<commit_before>(*  Title:      HOL/Auth/Public
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Theory of Public Keys (common to all symmetric-key protocols)

Server keys; initial states of agents; new nonces and keys; function "sees" 
*)


open Public;

(*Injectiveness of new nonces*)
AddIffs [inj_newN RS inj_eq];

(*Holds because Friend is injective: thus cannot prove for all f*)
goal thy "(Friend x : Friend``A) = (x:A)";
by (Auto_tac());
qed "Friend_image_eq";
Addsimps [Friend_image_eq];

Addsimps [Un_insert_left, Un_insert_right];

(*By default only o_apply is built-in.  But in the presence of eta-expansion
  this means that some terms displayed as (f o g) will be rewritten, and others
  will not!*)
Addsimps [o_def];

goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
by (agent.induct_tac "C" 1);
by (auto_tac (!claset addIs [range_eqI], !simpset));
qed "keysFor_parts_initState";
Addsimps [keysFor_parts_initState];

goalw thy [keysFor_def] "keysFor (Key``E) = {}";
by (Auto_tac ());
qed "keysFor_image_Key";
Addsimps [keysFor_image_Key];


(*** Function "sees" ***)

goal thy
    "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
by (list.induct_tac "evs" 1);
by (agent.induct_tac "A" 1);
by (event.induct_tac "a" 2);
by (Auto_tac ());
qed "sees_mono";

(*** Basic properties of pubK & priK ***)

AddIffs [inj_pubK RS inj_eq];
AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];

goalw thy [isSymKey_def] "~ isSymKey (pubK A)";
by (Simp_tac 1);
qed "not_isSymKey_pubK";

goalw thy [isSymKey_def] "~ isSymKey (priK A)";<commit_msg>New theorem priK_inj_eq, injectivity of priK<commit_after>(*  Title:      HOL/Auth/Public
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Theory of Public Keys (common to all symmetric-key protocols)

Server keys; initial states of agents; new nonces and keys; function "sees" 
*)


open Public;

(*Holds because Friend is injective: thus cannot prove for all f*)
goal thy "(Friend x : Friend``A) = (x:A)";
by (Auto_tac());
qed "Friend_image_eq";
Addsimps [Friend_image_eq];

Addsimps [Un_insert_left, Un_insert_right];

(*By default only o_apply is built-in.  But in the presence of eta-expansion
  this means that some terms displayed as (f o g) will be rewritten, and others
  will not!*)
Addsimps [o_def];

goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
by (agent.induct_tac "C" 1);
by (auto_tac (!claset addIs [range_eqI], !simpset));
qed "keysFor_parts_initState";
Addsimps [keysFor_parts_initState];

goalw thy [keysFor_def] "keysFor (Key``E) = {}";
by (Auto_tac ());
qed "keysFor_image_Key";
Addsimps [keysFor_image_Key];


(*** Function "sees" ***)

goal thy
    "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
by (list.induct_tac "evs" 1);
by (agent.induct_tac "A" 1);
by (event.induct_tac "a" 2);
by (Auto_tac ());
qed "sees_mono";

(*** Basic properties of pubK & priK ***)

AddIffs [inj_pubK RS inj_eq];

goal thy "!!A B. (priK A = priK B) = (A=B)";
by (Step_tac 1);
by (dres_inst_tac [("f","invKey")] arg_cong 1);
by (Full_simp_tac 1);
qed "priK_inj_eq";

AddIffs [priK_inj_eq];
AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];

goalw thy [isSymKey_def] "~ isSymKey (pubK A)";
by (Simp_tac 1);
qed "not_isSymKey_pubK";

goalw thy [isSymKey_def] "~ isSymKey (priK A)";
{'fraction_non_alphanumeric': 0.1388568129330254, 'fraction_numerical': 0.006062355658198615, 'mean_word_length': 4.755813953488372, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5411802', 'n_tokens_mistral': 1410, 'n_tokens_neox': 1344, 'n_words': 420}