--- a/src/HOL/SET_Protocol/Message_SET.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu May 26 17:51:22 2016 +0200
@@ -4,29 +4,29 @@
Author: Lawrence C Paulson
*)
-section{*The Message Theory, Modified for SET*}
+section\<open>The Message Theory, Modified for SET\<close>
theory Message_SET
imports Main "~~/src/HOL/Library/Nat_Bijection"
begin
-subsection{*General Lemmas*}
+subsection\<open>General Lemmas\<close>
-text{*Needed occasionally with @{text spy_analz_tac}, e.g. in
- @{text analz_insert_Key_newK}*}
+text\<open>Needed occasionally with \<open>spy_analz_tac\<close>, e.g. in
+ \<open>analz_insert_Key_newK\<close>\<close>
lemma Un_absorb3 [simp] : "A \<union> (B \<union> A) = B \<union> A"
by blast
-text{*Collapses redundant cases in the huge protocol proofs*}
+text\<open>Collapses redundant cases in the huge protocol proofs\<close>
lemmas disj_simps = disj_comms disj_left_absorb disj_assoc
-text{*Effective with assumptions like @{term "K \<notin> range pubK"} and
- @{term "K \<notin> invKey`range pubK"}*}
+text\<open>Effective with assumptions like @{term "K \<notin> range pubK"} and
+ @{term "K \<notin> invKey`range pubK"}\<close>
lemma notin_image_iff: "(y \<notin> f`I) = (\<forall>i\<in>I. f i \<noteq> y)"
by blast
-text{*Effective with the assumption @{term "KK \<subseteq> - (range(invKey o pubK))"} *}
+text\<open>Effective with the assumption @{term "KK \<subseteq> - (range(invKey o pubK))"}\<close>
lemma disjoint_image_iff: "(A <= - (f`I)) = (\<forall>i\<in>I. f i \<notin> A)"
by blast
@@ -35,8 +35,8 @@
type_synonym key = nat
consts
- all_symmetric :: bool --{*true if all keys are symmetric*}
- invKey :: "key=>key" --{*inverse of a symmetric key*}
+ all_symmetric :: bool \<comment>\<open>true if all keys are symmetric\<close>
+ invKey :: "key=>key" \<comment>\<open>inverse of a symmetric key\<close>
specification (invKey)
invKey [simp]: "invKey (invKey K) = K"
@@ -44,27 +44,27 @@
by (rule exI [of _ id], auto)
-text{*The inverse of a symmetric key is itself; that of a public key
- is the private key and vice versa*}
+text\<open>The inverse of a symmetric key is itself; that of a public key
+ is the private key and vice versa\<close>
definition symKeys :: "key set" where
"symKeys == {K. invKey K = K}"
-text{*Agents. We allow any number of certification authorities, cardholders
- merchants, and payment gateways.*}
+text\<open>Agents. We allow any number of certification authorities, cardholders
+ merchants, and payment gateways.\<close>
datatype
agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy
-text{*Messages*}
+text\<open>Messages\<close>
datatype
- msg = Agent agent --{*Agent names*}
- | Number nat --{*Ordinary integers, timestamps, ...*}
- | Nonce nat --{*Unguessable nonces*}
- | Pan nat --{*Unguessable Primary Account Numbers (??)*}
- | Key key --{*Crypto keys*}
- | Hash msg --{*Hashing*}
- | MPair msg msg --{*Compound messages*}
- | Crypt key msg --{*Encryption, public- or shared-key*}
+ msg = Agent agent \<comment>\<open>Agent names\<close>
+ | Number nat \<comment>\<open>Ordinary integers, timestamps, ...\<close>
+ | Nonce nat \<comment>\<open>Unguessable nonces\<close>
+ | Pan nat \<comment>\<open>Unguessable Primary Account Numbers (??)\<close>
+ | Key key \<comment>\<open>Crypto keys\<close>
+ | Hash msg \<comment>\<open>Hashing\<close>
+ | MPair msg msg \<comment>\<open>Compound messages\<close>
+ | Crypt key msg \<comment>\<open>Encryption, public- or shared-key\<close>
(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
@@ -81,9 +81,9 @@
(curry prod_encode 2)
(curry prod_encode 3)
(prod_encode (4,0))"
- --{*maps each agent to a unique natural number, for specifications*}
+ \<comment>\<open>maps each agent to a unique natural number, for specifications\<close>
-text{*The function is indeed injective*}
+text\<open>The function is indeed injective\<close>
lemma inj_nat_of_agent: "inj nat_of_agent"
by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split)
@@ -93,7 +93,7 @@
keysFor :: "msg set => key set"
where "keysFor H = invKey ` {K. \<exists>X. Crypt K X \<in> H}"
-subsubsection{*Inductive definition of all "parts" of a message.*}
+subsubsection\<open>Inductive definition of all "parts" of a message.\<close>
inductive_set
parts :: "msg set => msg set"
@@ -113,7 +113,7 @@
done
-subsubsection{*Inverse of keys*}
+subsubsection\<open>Inverse of keys\<close>
(*Equations hold because constructors are injective; cannot prove for all f*)
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
@@ -143,7 +143,7 @@
done
-subsection{*keysFor operator*}
+subsection\<open>keysFor operator\<close>
lemma keysFor_empty [simp]: "keysFor {} = {}"
by (unfold keysFor_def, blast)
@@ -190,7 +190,7 @@
by (unfold keysFor_def, blast)
-subsection{*Inductive relation "parts"*}
+subsection\<open>Inductive relation "parts"\<close>
lemma MPair_parts:
"[| \<lbrace>X,Y\<rbrace> \<in> parts H;
@@ -198,10 +198,10 @@
by (blast dest: parts.Fst parts.Snd)
declare MPair_parts [elim!] parts.Body [dest!]
-text{*NB These two rules are UNSAFE in the formal sense, as they discard the
+text\<open>NB These two rules are UNSAFE in the formal sense, as they discard the
compound message. They work well on THIS FILE.
- @{text MPair_parts} is left as SAFE because it speeds up proofs.
- The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
+ \<open>MPair_parts\<close> is left as SAFE because it speeds up proofs.
+ The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.\<close>
lemma parts_increasing: "H \<subseteq> parts(H)"
by blast
@@ -221,7 +221,7 @@
by (erule parts.induct, fast+)
-subsubsection{*Unions*}
+subsubsection\<open>Unions\<close>
lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
by (intro Un_least parts_mono Un_upper1 Un_upper2)
@@ -262,15 +262,15 @@
NOTE: the UN versions are no longer used!*)
-text{*This allows @{text blast} to simplify occurrences of
- @{term "parts(G\<union>H)"} in the assumption.*}
+text\<open>This allows \<open>blast\<close> to simplify occurrences of
+ @{term "parts(G\<union>H)"} in the assumption.\<close>
declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!]
lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
by (blast intro: parts_mono [THEN [2] rev_subsetD])
-subsubsection{*Idempotence and transitivity*}
+subsubsection\<open>Idempotence and transitivity\<close>
lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
by (erule parts.induct, blast+)
@@ -290,7 +290,7 @@
by (force dest!: parts_cut intro: parts_insertI)
-subsubsection{*Rewrite rules for pulling out atomic messages*}
+subsubsection\<open>Rewrite rules for pulling out atomic messages\<close>
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
@@ -383,11 +383,11 @@
apply (rule_tac x = "N + Suc nat" in exI, auto)
done
-subsection{*Inductive relation "analz"*}
+subsection\<open>Inductive relation "analz"\<close>
-text{*Inductive definition of "analz" -- what can be broken down from a set of
+text\<open>Inductive definition of "analz" -- what can be broken down from a set of
messages, including keys. A form of downward closure. Pairs can
- be taken apart; messages decrypted with known keys.*}
+ be taken apart; messages decrypted with known keys.\<close>
inductive_set
analz :: "msg set => msg set"
@@ -407,7 +407,7 @@
apply (auto dest: Fst Snd)
done
-text{*Making it safe speeds up proofs*}
+text\<open>Making it safe speeds up proofs\<close>
lemma MPair_analz [elim!]:
"[| \<lbrace>X,Y\<rbrace> \<in> analz H;
[| X \<in> analz H; Y \<in> analz H |] ==> P
@@ -440,7 +440,7 @@
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
-subsubsection{*General equational properties*}
+subsubsection\<open>General equational properties\<close>
lemma analz_empty [simp]: "analz{} = {}"
apply safe
@@ -455,7 +455,7 @@
lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])
-subsubsection{*Rewrite rules for pulling out atomic messages*}
+subsubsection\<open>Rewrite rules for pulling out atomic messages\<close>
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
@@ -568,7 +568,7 @@
done
-subsubsection{*Idempotence and transitivity*}
+subsubsection\<open>Idempotence and transitivity\<close>
lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
by (erule analz.induct, blast+)
@@ -594,7 +594,7 @@
by (blast intro: analz_cut analz_insertI)
-text{*A congruence rule for "analz"*}
+text\<open>A congruence rule for "analz"\<close>
lemma analz_subset_cong:
"[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'
@@ -631,12 +631,12 @@
by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
-subsection{*Inductive relation "synth"*}
+subsection\<open>Inductive relation "synth"\<close>
-text{*Inductive definition of "synth" -- what can be built up from a set of
+text\<open>Inductive definition of "synth" -- what can be built up from a set of
messages. A form of upward closure. Pairs can be built, messages
encrypted with known keys. Agent names are public domain.
- Numbers can be guessed, but Nonces cannot be.*}
+ Numbers can be guessed, but Nonces cannot be.\<close>
inductive_set
synth :: "msg set => msg set"
@@ -668,7 +668,7 @@
lemma synth_increasing: "H \<subseteq> synth(H)"
by blast
-subsubsection{*Unions*}
+subsubsection\<open>Unions\<close>
(*Converse fails: we can synth more from the union than from the
separate parts, building a compound message using elements of each.*)
@@ -678,7 +678,7 @@
lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
by (blast intro: synth_mono [THEN [2] rev_subsetD])
-subsubsection{*Idempotence and transitivity*}
+subsubsection\<open>Idempotence and transitivity\<close>
lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
by (erule synth.induct, blast+)
@@ -716,7 +716,7 @@
by (unfold keysFor_def, blast)
-subsubsection{*Combinations of parts, analz and synth*}
+subsubsection\<open>Combinations of parts, analz and synth\<close>
lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
apply (rule equalityI)
@@ -745,7 +745,7 @@
done
-subsubsection{*For reasoning about the Fake rule in traces*}
+subsubsection\<open>For reasoning about the Fake rule in traces\<close>
lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
@@ -806,8 +806,8 @@
declare parts.Body [rule del]
-text{*Rewrites to push in Key and Crypt messages, so that other messages can
- be pulled out using the @{text analz_insert} rules*}
+text\<open>Rewrites to push in Key and Crypt messages, so that other messages can
+ be pulled out using the \<open>analz_insert\<close> rules\<close>
lemmas pushKeys =
insert_commute [of "Key K" "Agent C"]
@@ -828,15 +828,15 @@
insert_commute [of "Crypt X K" "MPair X' Y"]
for X K C N PAN X' Y
-text{*Cannot be added with @{text "[simp]"} -- messages should not always be
- re-ordered.*}
+text\<open>Cannot be added with \<open>[simp]\<close> -- messages should not always be
+ re-ordered.\<close>
lemmas pushes = pushKeys pushCrypts
-subsection{*Tactics useful for many protocol proofs*}
+subsection\<open>Tactics useful for many protocol proofs\<close>
(*<*)
ML
-{*
+\<open>
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
but this application is no longer necessary if analz_insert_eq is used.
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
@@ -873,7 +873,7 @@
simp_tac ctxt 1,
REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
-*}
+\<close>
(*>*)
@@ -901,7 +901,7 @@
apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD])
done
-text{*Two generalizations of @{text analz_insert_eq}*}
+text\<open>Two generalizations of \<open>analz_insert_eq\<close>\<close>
lemma gen_analz_insert_eq [rule_format]:
"X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
@@ -922,16 +922,16 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
-method_setup spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o spy_analz_tac) *}
+method_setup spy_analz = \<open>
+ Scan.succeed (SIMPLE_METHOD' o spy_analz_tac)\<close>
"for proving the Fake case when analz is involved"
-method_setup atomic_spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac) *}
+method_setup atomic_spy_analz = \<open>
+ Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac)\<close>
"for debugging spy_analz"
-method_setup Fake_insert_simp = {*
- Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac) *}
+method_setup Fake_insert_simp = \<open>
+ Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac)\<close>
"for debugging spy_analz"
end