<commit_before>(*  Title:      HOL/Auth/Guard/Guard_Public.thy
    Author:     <NAME>, University of Cambridge Computer Laboratory
    Copyright   2002  University of Cambridge

Lemmas on guarded messages for public protocols.
*)

theory Guard_Public imports Guard Public Extensions begin

subsection{*Extensions to Theory @{text Public}*}

declare initState.simps [simp del]

subsubsection{*signature*}

definition sign :: "agent => msg => msg" where
"sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}"

lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')"
by (auto simp: sign_def)

subsubsection{*agent associated to a key*}

definition agt :: "key => agent" where
"agt K == @A. K = priK A | K = pubK A"

lemma agt_priK [simp]: "agt (priK A) = A"
by (simp add: agt_def)

lemma agt_pubK [simp]: "agt (pubK A) = A"
by (simp add: agt_def)

subsubsection{*basic facts about @{term initState}*}

lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)"
by (cases A, auto simp: initState.simps)

lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)"<commit_msg>more precise imports;<commit_after>(*  Title:      HOL/Auth/Guard/Guard_Public.thy
    Author:     <NAME>, University of Cambridge Computer Laboratory
    Copyright   2002  University of Cambridge

Lemmas on guarded messages for public protocols.
*)

theory Guard_Public imports Guard "../Public" Extensions begin

subsection{*Extensions to Theory @{text Public}*}

declare initState.simps [simp del]

subsubsection{*signature*}

definition sign :: "agent => msg => msg" where
"sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}"

lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')"
by (auto simp: sign_def)

subsubsection{*agent associated to a key*}

definition agt :: "key => agent" where
"agt K == @A. K = priK A | K = pubK A"

lemma agt_priK [simp]: "agt (priK A) = A"
by (simp add: agt_def)

lemma agt_pubK [simp]: "agt (pubK A) = A"
by (simp add: agt_def)

subsubsection{*basic facts about @{term initState}*}

lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)"
by (cases A, auto simp: initState.simps)

lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)"
{'fraction_non_alphanumeric': 0.13363431151241534, 'fraction_numerical': 0.0036117381489841984, 'mean_word_length': 4.485148514851486, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 11, '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': '7468856', 'n_tokens_mistral': 818, 'n_tokens_neox': 788, 'n_words': 283}