--- a/src/HOL/Auth/Public.thy Thu Dec 10 21:31:24 2015 +0100
+++ b/src/HOL/Auth/Public.thy Thu Dec 10 21:39:33 2015 +0100
@@ -14,7 +14,7 @@
lemma invKey_K: "K \<in> symKeys ==> invKey K = K"
by (simp add: symKeys_def)
-subsection{*Asymmetric Keys*}
+subsection\<open>Asymmetric Keys\<close>
datatype keymode = Signature | Encryption
@@ -43,8 +43,8 @@
"priSK A == privateKey Signature A"
-text{*These abbreviations give backward compatibility. They represent the
-simple situation where the signature and encryption keys are the same.*}
+text\<open>These abbreviations give backward compatibility. They represent the
+simple situation where the signature and encryption keys are the same.\<close>
abbreviation
pubK :: "agent => key" where
@@ -55,8 +55,8 @@
"priK A == invKey (pubEK A)"
-text{*By freeness of agents, no two agents have the same key. Since
- @{term "True\<noteq>False"}, no agent has identical signing and encryption keys*}
+text\<open>By freeness of agents, no two agents have the same key. Since
+ @{term "True\<noteq>False"}, no agent has identical signing and encryption keys\<close>
specification (publicKey)
injective_publicKey:
"publicKey b A = publicKey c A' ==> b=c & A=A'"
@@ -77,7 +77,7 @@
declare publicKey_neq_privateKey [iff]
-subsection{*Basic properties of @{term pubK} and @{term priK}*}
+subsection\<open>Basic properties of @{term pubK} and @{term priK}\<close>
lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
by (blast dest!: injective_publicKey)
@@ -104,7 +104,7 @@
-subsection{*"Image" equations that hold for injective functions*}
+subsection\<open>"Image" equations that hold for injective functions\<close>
lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)"
by auto
@@ -125,26 +125,26 @@
by auto
-subsection{*Symmetric Keys*}
+subsection\<open>Symmetric Keys\<close>
-text{*For some protocols, it is convenient to equip agents with symmetric as
-well as asymmetric keys. The theory @{text Shared} assumes that all keys
-are symmetric.*}
+text\<open>For some protocols, it is convenient to equip agents with symmetric as
+well as asymmetric keys. The theory \<open>Shared\<close> assumes that all keys
+are symmetric.\<close>
consts
- shrK :: "agent => key" --{*long-term shared keys*}
+ shrK :: "agent => key" \<comment>\<open>long-term shared keys\<close>
specification (shrK)
inj_shrK: "inj shrK"
- --{*No two agents have the same long-term key*}
+ \<comment>\<open>No two agents have the same long-term key\<close>
apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"])
apply (simp add: inj_on_def split: agent.split)
done
axiomatization where
- sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
+ sym_shrK [iff]: "shrK X \<in> symKeys" \<comment>\<open>All shared keys are symmetric\<close>
-text{*Injectiveness: Agents' long-term keys are distinct.*}
+text\<open>Injectiveness: Agents' long-term keys are distinct.\<close>
lemmas shrK_injective = inj_shrK [THEN inj_eq]
declare shrK_injective [iff]
@@ -189,15 +189,15 @@
lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)"
by auto
-text{*For some reason, moving this up can make some proofs loop!*}
+text\<open>For some reason, moving this up can make some proofs loop!\<close>
declare invKey_K [simp]
-subsection{*Initial States of Agents*}
+subsection\<open>Initial States of Agents\<close>
-text{*Note: for all practical purposes, all that matters is the initial
+text\<open>Note: for all practical purposes, all that matters is the initial
knowledge of the Spy. All other agents are automata, merely following the
-protocol.*}
+protocol.\<close>
overloading
initState \<equiv> initState
@@ -224,10 +224,10 @@
end
-text{*These lemmas allow reasoning about @{term "used evs"} rather than
+text\<open>These lemmas allow reasoning about @{term "used evs"} rather than
@{term "knows Spy evs"}, which is useful when there are private Notes.
Because they depend upon the definition of @{term initState}, they cannot
- be moved up.*}
+ be moved up.\<close>
lemma used_parts_subset_parts [rule_format]:
"\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
@@ -235,15 +235,15 @@
prefer 2
apply (simp add: used_Cons split: event.split)
apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff)
-txt{*Base case*}
+txt\<open>Base case\<close>
apply (auto dest!: parts_cut simp add: used_Nil)
done
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
by (drule used_parts_subset_parts, simp, blast)
-text{*There was a similar theorem in Event.thy, so perhaps this one can
- be moved up if proved directly by induction.*}
+text\<open>There was a similar theorem in Event.thy, so perhaps this one can
+ be moved up if proved directly by induction.\<close>
lemma MPair_used [elim!]:
"[| {|X,Y|} \<in> used H;
[| X \<in> used H; Y \<in> used H |] ==> P |]
@@ -251,8 +251,8 @@
by (blast dest: MPair_used_D)
-text{*Rewrites should not refer to @{term "initState(Friend i)"} because
- that expression is not in normal form.*}
+text\<open>Rewrites should not refer to @{term "initState(Friend i)"} because
+ that expression is not in normal form.\<close>
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
apply (unfold keysFor_def)
@@ -293,20 +293,20 @@
declare neq_shrK [simp]
-subsection{*Function @{term spies} *}
+subsection\<open>Function @{term spies}\<close>
lemma not_SignatureE [elim!]: "b \<noteq> Signature \<Longrightarrow> b = Encryption"
by (cases b, auto)
-text{*Agents see their own private keys!*}
+text\<open>Agents see their own private keys!\<close>
lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A"
by (cases A, auto)
-text{*Agents see all public keys!*}
+text\<open>Agents see all public keys!\<close>
lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B"
by (cases B, auto)
-text{*All public keys are visible*}
+text\<open>All public keys are visible\<close>
lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
apply (induct_tac "evs")
apply (auto simp add: imageI knows_Cons split add: event.split)
@@ -315,14 +315,14 @@
lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
declare analz_spies_pubK [iff]
-text{*Spy sees private keys of bad agents!*}
+text\<open>Spy sees private keys of bad agents!\<close>
lemma Spy_spies_bad_privateKey [intro!]:
"A \<in> bad ==> Key (privateKey b A) \<in> spies evs"
apply (induct_tac "evs")
apply (auto simp add: imageI knows_Cons split add: event.split)
done
-text{*Spy sees long-term shared keys of bad agents!*}
+text\<open>Spy sees long-term shared keys of bad agents!\<close>
lemma Spy_spies_bad_shrK [intro!]:
"A \<in> bad ==> Key (shrK A) \<in> spies evs"
apply (induct_tac "evs")
@@ -346,7 +346,7 @@
by force
-subsection{*Fresh Nonces*}
+subsection\<open>Fresh Nonces\<close>
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
by (induct_tac "B", auto)
@@ -355,9 +355,9 @@
by (simp add: used_Nil)
-subsection{*Supply fresh nonces for possibility theorems*}
+subsection\<open>Supply fresh nonces for possibility theorems\<close>
-text{*In any trace, there is an upper bound N on the greatest nonce in use*}
+text\<open>In any trace, there is an upper bound N on the greatest nonce in use\<close>
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
@@ -374,7 +374,7 @@
apply (rule someI, fast)
done
-subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
+subsection\<open>Specialized Rewriting for Theorems About @{term analz} and Image\<close>
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
by blast
@@ -386,22 +386,22 @@
lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H"
by (drule Crypt_imp_invKey_keysFor, simp)
-text{*Lemma for the trivial direction of the if-and-only-if of the
-Session Key Compromise Theorem*}
+text\<open>Lemma for the trivial direction of the if-and-only-if of the
+Session Key Compromise Theorem\<close>
lemma analz_image_freshK_lemma:
"(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H) ==>
(Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])
lemmas analz_image_freshK_simps =
- simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
+ simp_thms mem_simps \<comment>\<open>these two allow its use with \<open>only:\<close>\<close>
disj_comms
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
insert_Key_singleton
Key_not_used insert_Key_image Un_assoc [THEN sym]
-ML {*
+ML \<open>
structure Public =
struct
@@ -428,25 +428,25 @@
REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
end
-*}
+\<close>
-method_setup analz_freshK = {*
+method_setup analz_freshK = \<open>
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
- ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))]))) *}
+ ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))])))\<close>
"for proving the Session Key Compromise theorem"
-subsection{*Specialized Methods for Possibility Theorems*}
+subsection\<open>Specialized Methods for Possibility Theorems\<close>
-method_setup possibility = {*
- Scan.succeed (SIMPLE_METHOD o Public.possibility_tac) *}
+method_setup possibility = \<open>
+ Scan.succeed (SIMPLE_METHOD o Public.possibility_tac)\<close>
"for proving possibility theorems"
-method_setup basic_possibility = {*
- Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac) *}
+method_setup basic_possibility = \<open>
+ Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac)\<close>
"for proving possibility theorems"
end