--- a/src/HOL/SET_Protocol/Public_SET.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy Thu May 26 17:51:22 2016 +0200
@@ -4,24 +4,24 @@
Author: Lawrence C Paulson
*)
-section{*The Public-Key Theory, Modified for SET*}
+section\<open>The Public-Key Theory, Modified for SET\<close>
theory Public_SET
imports Event_SET
begin
-subsection{*Symmetric and Asymmetric Keys*}
+subsection\<open>Symmetric and Asymmetric Keys\<close>
-text{*definitions influenced by the wish to assign asymmetric keys
+text\<open>definitions influenced by the wish to assign asymmetric keys
- since the beginning - only to RCA and CAs, namely we need a partial
- function on type Agent*}
+ function on type Agent\<close>
-text{*The SET specs mention two signature keys for CAs - we only have one*}
+text\<open>The SET specs mention two signature keys for CAs - we only have one\<close>
consts
publicKey :: "[bool, agent] => key"
- --{*the boolean is TRUE if a signing key*}
+ \<comment>\<open>the boolean is TRUE if a signing key\<close>
abbreviation "pubEK == publicKey False"
abbreviation "pubSK == publicKey True"
@@ -30,8 +30,8 @@
abbreviation "priEK A == invKey (pubEK A)"
abbreviation "priSK A == invKey (pubSK A)"
-text{*By freeness of agents, no two agents have the same key. Since
- @{term "True\<noteq>False"}, no agent has the same 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 the same signing and encryption keys.\<close>
specification (publicKey)
injective_publicKey:
@@ -55,15 +55,15 @@
declare privateKey_neq_publicKey [THEN not_sym, iff]
-subsection{*Initial Knowledge*}
+subsection\<open>Initial Knowledge\<close>
-text{*This information is not necessary. Each protocol distributes any needed
+text\<open>This information is not necessary. Each protocol distributes any needed
certificates, and anyway our proofs require a formalization of the Spy's
knowledge only. However, the initial knowledge is as follows:
All agents know RCA's public keys;
RCA and CAs know their own respective keys;
RCA (has already certified and therefore) knows all CAs public keys;
- Spy knows all keys of all bad agents.*}
+ Spy knows all keys of all bad agents.\<close>
overloading initState \<equiv> "initState"
begin
@@ -104,13 +104,13 @@
end
-text{*Injective mapping from agents to PANs: an agent can have only one card*}
+text\<open>Injective mapping from agents to PANs: an agent can have only one card\<close>
consts pan :: "agent => nat"
specification (pan)
inj_pan: "inj pan"
- --{*No two agents have the same PAN*}
+ \<comment>\<open>No two agents have the same PAN\<close>
(*<*)
apply (rule exI [of _ "nat_of_agent"])
apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq])
@@ -120,10 +120,10 @@
declare inj_pan [THEN inj_eq, iff]
consts
- XOR :: "nat*nat => nat" --{*no properties are assumed of exclusive-or*}
+ XOR :: "nat*nat => nat" \<comment>\<open>no properties are assumed of exclusive-or\<close>
-subsection{*Signature Primitives*}
+subsection\<open>Signature Primitives\<close>
definition
(* Signature = Message + signed Digest *)
@@ -167,22 +167,22 @@
abbreviation "onlySig == Number (Suc 0)"
abbreviation "authCode == Number (Suc (Suc 0))"
-subsection{*Encryption Primitives*}
+subsection\<open>Encryption Primitives\<close>
definition EXcrypt :: "[key,key,msg,msg] => msg" where
- --{*Extra Encryption*}
+ \<comment>\<open>Extra Encryption\<close>
(*K: the symmetric key EK: the public encryption key*)
"EXcrypt K EK M m =
\<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m\<rbrace>\<rbrace>"
definition EXHcrypt :: "[key,key,msg,msg] => msg" where
- --{*Extra Encryption with Hashing*}
+ \<comment>\<open>Extra Encryption with Hashing\<close>
(*K: the symmetric key EK: the public encryption key*)
"EXHcrypt K EK M m =
\<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m, Hash M\<rbrace>\<rbrace>"
definition Enc :: "[key,key,key,msg] => msg" where
- --{*Simple Encapsulation with SIGNATURE*}
+ \<comment>\<open>Simple Encapsulation with SIGNATURE\<close>
(*SK: the sender's signing key
K: the symmetric key
EK: the public encryption key*)
@@ -190,12 +190,12 @@
\<lbrace>Crypt K (sign SK M), Crypt EK (Key K)\<rbrace>"
definition EncB :: "[key,key,key,msg,msg] => msg" where
- --{*Encapsulation with Baggage. Keys as above, and baggage b.*}
+ \<comment>\<open>Encapsulation with Baggage. Keys as above, and baggage b.\<close>
"EncB SK K EK M b =
\<lbrace>Enc SK K EK \<lbrace>M, Hash b\<rbrace>, b\<rbrace>"
-subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}
+subsection\<open>Basic Properties of pubEK, pubSK, priEK and priSK\<close>
lemma publicKey_eq_iff [iff]:
"(publicKey b A = publicKey b' A') = (b=b' & A=A')"
@@ -217,12 +217,12 @@
lemma symKeys_invKey_iff [simp]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
by (unfold symKeys_def, auto)
-text{*Can be slow (or even loop) as a simprule*}
+text\<open>Can be slow (or even loop) as a simprule\<close>
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
by blast
-text{*These alternatives to @{text symKeys_neq_imp_neq} don't seem any better
-in practice.*}
+text\<open>These alternatives to \<open>symKeys_neq_imp_neq\<close> don't seem any better
+in practice.\<close>
lemma publicKey_neq_symKey: "K \<in> symKeys ==> publicKey b A \<noteq> K"
by blast
@@ -241,12 +241,12 @@
by auto
-subsection{*"Image" Equations That Hold for Injective Functions *}
+subsection\<open>"Image" Equations That Hold for Injective Functions\<close>
lemma invKey_image_eq [iff]: "(invKey x \<in> invKey`A) = (x\<in>A)"
by auto
-text{*holds because invKey is injective*}
+text\<open>holds because invKey is injective\<close>
lemma publicKey_image_eq [iff]:
"(publicKey b A \<in> publicKey c ` AS) = (b=c & A\<in>AS)"
by auto
@@ -269,7 +269,7 @@
apply (auto intro: range_eqI)
done
-text{*for proving @{text new_keys_not_used}*}
+text\<open>for proving \<open>new_keys_not_used\<close>\<close>
lemma keysFor_parts_insert:
"[| K \<in> keysFor (parts (insert X H)); X \<in> synth (analz H) |]
==> K \<in> keysFor (parts H) | Key (invKey K) \<in> parts H"
@@ -282,22 +282,22 @@
"[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
by (drule Crypt_imp_invKey_keysFor, simp)
-text{*Agents see their own private keys!*}
+text\<open>Agents see their own private keys!\<close>
lemma privateKey_in_initStateCA [iff]:
"Key (invKey (publicKey b A)) \<in> initState A"
by (case_tac "A", auto)
-text{*Agents see their own public keys!*}
+text\<open>Agents see their own public keys!\<close>
lemma publicKey_in_initStateCA [iff]: "Key (publicKey b A) \<in> initState A"
by (case_tac "A", auto)
-text{*RCA sees CAs' public keys! *}
+text\<open>RCA sees CAs' public keys!\<close>
lemma pubK_CA_in_initState_RCA [iff]:
"Key (publicKey b (CA i)) \<in> initState RCA"
by auto
-text{*Spy knows all public keys*}
+text\<open>Spy knows all public keys\<close>
lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs"
apply (induct_tac "evs")
apply (simp_all add: imageI knows_Cons split add: event.split)
@@ -306,13 +306,13 @@
declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
(*needed????*)
-text{*Spy sees private keys of bad agents! [and obviously public keys too]*}
+text\<open>Spy sees private keys of bad agents! [and obviously public keys too]\<close>
lemma knows_Spy_bad_privateKey [intro!]:
"A \<in> bad ==> Key (invKey (publicKey b A)) \<in> knows Spy evs"
by (rule initState_subset_knows [THEN subsetD], simp)
-subsection{*Fresh Nonces for Possibility Theorems*}
+subsection\<open>Fresh Nonces for Possibility Theorems\<close>
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
by (induct_tac "B", auto)
@@ -320,7 +320,7 @@
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
by (simp add: used_Nil)
-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: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
@@ -337,10 +337,10 @@
done
-subsection{*Specialized Methods for Possibility Theorems*}
+subsection\<open>Specialized Methods for Possibility Theorems\<close>
ML
-{*
+\<open>
(*Tactic for possibility theorems*)
fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
@@ -356,18 +356,18 @@
(ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
-*}
+\<close>
-method_setup possibility = {*
- Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
+method_setup possibility = \<open>
+ Scan.succeed (SIMPLE_METHOD o possibility_tac)\<close>
"for proving possibility theorems"
-method_setup basic_possibility = {*
- Scan.succeed (SIMPLE_METHOD o basic_possibility_tac) *}
+method_setup basic_possibility = \<open>
+ Scan.succeed (SIMPLE_METHOD o basic_possibility_tac)\<close>
"for proving possibility theorems"
-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
@@ -376,17 +376,17 @@
"insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
by blast
-text{*Needed for @{text DK_fresh_not_KeyCryptKey}*}
+text\<open>Needed for \<open>DK_fresh_not_KeyCryptKey\<close>\<close>
lemma publicKey_in_used [iff]: "Key (publicKey b A) \<in> used evs"
by auto
lemma privateKey_in_used [iff]: "Key (invKey (publicKey b A)) \<in> used evs"
by (blast intro!: initState_into_used)
-text{*Reverse the normal simplification of "image" to build up (not break down)
- the set of keys. Based on @{text analz_image_freshK_ss}, but simpler.*}
+text\<open>Reverse the normal simplification of "image" to build up (not break down)
+ the set of keys. Based on \<open>analz_image_freshK_ss\<close>, but simpler.\<close>
lemmas analz_image_keys_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>
image_insert [THEN sym] image_Un [THEN sym]
rangeI symKeys_neq_imp_neq
insert_Key_singleton insert_Key_image Un_assoc [THEN sym]
@@ -394,16 +394,16 @@
(*General lemmas proved by Larry*)
-subsection{*Controlled Unfolding of Abbreviations*}
+subsection\<open>Controlled Unfolding of Abbreviations\<close>
-text{*A set is expanded only if a relation is applied to it*}
+text\<open>A set is expanded only if a relation is applied to it\<close>
lemma def_abbrev_simp_relation:
"A = B ==> (A \<in> X) = (B \<in> X) &
(u = A) = (u = B) &
(A = u) = (B = u)"
by auto
-text{*A set is expanded only if one of the given functions is applied to it*}
+text\<open>A set is expanded only if one of the given functions is applied to it\<close>
lemma def_abbrev_simp_function:
"A = B
==> parts (insert A X) = parts (insert B X) &
@@ -411,15 +411,15 @@
keysFor (insert A X) = keysFor (insert B X)"
by auto
-subsubsection{*Special Simplification Rules for @{term signCert}*}
+subsubsection\<open>Special Simplification Rules for @{term signCert}\<close>
-text{*Avoids duplicating X and its components!*}
+text\<open>Avoids duplicating X and its components!\<close>
lemma parts_insert_signCert:
"parts (insert (signCert K X) H) =
insert \<lbrace>X, Crypt K X\<rbrace> (parts (insert (Crypt K X) H))"
by (simp add: signCert_def insert_commute [of X])
-text{*Avoids a case split! [X is always available]*}
+text\<open>Avoids a case split! [X is always available]\<close>
lemma analz_insert_signCert:
"analz (insert (signCert K X) H) =
insert \<lbrace>X, Crypt K X\<rbrace> (insert (Crypt K X) (analz (insert X H)))"
@@ -428,9 +428,9 @@
lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H"
by (simp add: signCert_def)
-text{*Controlled rewrite rules for @{term signCert}, just the definitions
+text\<open>Controlled rewrite rules for @{term signCert}, just the definitions
of the others. Encryption primitives are just expanded, despite their huge
- redundancy!*}
+ redundancy!\<close>
lemmas abbrev_simps [simp] =
parts_insert_signCert analz_insert_signCert keysFor_insert_signCert
sign_def [THEN def_abbrev_simp_relation]
@@ -451,7 +451,7 @@
EncB_def [THEN def_abbrev_simp_function]
-subsubsection{*Elimination Rules for Controlled Rewriting *}
+subsubsection\<open>Elimination Rules for Controlled Rewriting\<close>
lemma Enc_partsE:
"!!R. [|Enc SK K EK M \<in> parts H;
@@ -477,7 +477,7 @@
by (unfold EXcrypt_def, blast)
-subsection{*Lemmas to Simplify Expressions Involving @{term analz} *}
+subsection\<open>Lemmas to Simplify Expressions Involving @{term analz}\<close>
lemma analz_knows_absorb:
"Key K \<in> analz (knows Spy evs)
@@ -505,13 +505,13 @@
subset_insertI [THEN [2] subset_trans]
-subsection{*Freshness Lemmas*}
+subsection\<open>Freshness Lemmas\<close>
lemma in_parts_Says_imp_used:
"[|Key K \<in> parts {X}; Says A B X \<in> set evs|] ==> Key K \<in> used evs"
by (blast intro: parts_trans dest!: Says_imp_knows_Spy [THEN parts.Inj])
-text{*A useful rewrite rule with @{term analz_image_keys_simps}*}
+text\<open>A useful rewrite rule with @{term analz_image_keys_simps}\<close>
lemma Crypt_notin_image_Key: "Crypt K X \<notin> Key ` KK"
by auto