author | paulson <lp15@cam.ac.uk> |
Thu, 13 Oct 2022 17:19:50 +0100 | |
changeset 76291 | 616405057951 |
parent 76290 | 64d29ebb7d3d |
child 76299 | 0ad6f6508274 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/Auth/Message.thy |
1839 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1996 University of Cambridge |
|
4 |
||
5 |
Datatypes of agents and messages; |
|
1913 | 6 |
Inductive relations "parts", "analz" and "synth" |
1839 | 7 |
*) |
8 |
||
61830 | 9 |
section\<open>Theory of Agents and Messages for Security Protocols\<close> |
13956 | 10 |
|
27105
5f139027c365
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26807
diff
changeset
|
11 |
theory Message |
5f139027c365
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26807
diff
changeset
|
12 |
imports Main |
5f139027c365
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26807
diff
changeset
|
13 |
begin |
11189 | 14 |
|
15 |
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
|
13926 | 16 |
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
76288
b82ac7ef65ec
Removal of the "unfold" method in favour of "unfolding"
paulson <lp15@cam.ac.uk>
parents:
76287
diff
changeset
|
17 |
by blast |
1839 | 18 |
|
41774 | 19 |
type_synonym |
1839 | 20 |
key = nat |
21 |
||
22 |
consts |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
23 |
all_symmetric :: bool \<comment> \<open>true if all keys are symmetric\<close> |
67613 | 24 |
invKey :: "key\<Rightarrow>key" \<comment> \<open>inverse of a symmetric key\<close> |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
25 |
|
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
26 |
specification (invKey) |
14181 | 27 |
invKey [simp]: "invKey (invKey K) = K" |
67613 | 28 |
invKey_symmetric: "all_symmetric \<longrightarrow> invKey = id" |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
29 |
by (rule exI [of _ id], auto) |
1839 | 30 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
31 |
|
61830 | 32 |
text\<open>The inverse of a symmetric key is itself; that of a public key |
33 |
is the private key and vice versa\<close> |
|
1839 | 34 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35109
diff
changeset
|
35 |
definition symKeys :: "key set" where |
11230
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11192
diff
changeset
|
36 |
"symKeys == {K. invKey K = K}" |
1839 | 37 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
38 |
datatype \<comment> \<open>We allow any number of friendly agents\<close> |
2032 | 39 |
agent = Server | Friend nat | Spy |
1839 | 40 |
|
58310 | 41 |
datatype |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
42 |
msg = Agent agent \<comment> \<open>Agent names\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
43 |
| Number nat \<comment> \<open>Ordinary integers, timestamps, ...\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
44 |
| Nonce nat \<comment> \<open>Unguessable nonces\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
45 |
| Key key \<comment> \<open>Crypto keys\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
46 |
| Hash msg \<comment> \<open>Hashing\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
47 |
| MPair msg msg \<comment> \<open>Compound messages\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
48 |
| Crypt key msg \<comment> \<open>Encryption, public- or shared-key\<close> |
1839 | 49 |
|
5234 | 50 |
|
61956 | 51 |
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
5234 | 52 |
syntax |
61956 | 53 |
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
1839 | 54 |
translations |
61956 | 55 |
"\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
56 |
"\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
|
1839 | 57 |
|
58 |
||
67613 | 59 |
definition HPair :: "[msg,msg] \<Rightarrow> msg" ("(4Hash[_] /_)" [0, 1000]) where |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
60 |
\<comment> \<open>Message Y paired with a MAC computed with the help of X\<close> |
61956 | 61 |
"Hash[X] Y == \<lbrace>Hash\<lbrace>X,Y\<rbrace>, Y\<rbrace>" |
2484 | 62 |
|
67613 | 63 |
definition keysFor :: "msg set \<Rightarrow> key set" where |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62390
diff
changeset
|
64 |
\<comment> \<open>Keys useful to decrypt elements of a message set\<close> |
11192 | 65 |
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" |
1839 | 66 |
|
16818 | 67 |
|
61830 | 68 |
subsubsection\<open>Inductive Definition of All Parts" of a Message\<close> |
1839 | 69 |
|
23746 | 70 |
inductive_set |
67613 | 71 |
parts :: "msg set \<Rightarrow> msg set" |
23746 | 72 |
for H :: "msg set" |
73 |
where |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
74 |
Inj [intro]: "X \<in> H \<Longrightarrow> X \<in> parts H" |
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
75 |
| Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H \<Longrightarrow> X \<in> parts H" |
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
76 |
| Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H \<Longrightarrow> Y \<in> parts H" |
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
77 |
| Body: "Crypt K X \<in> parts H \<Longrightarrow> X \<in> parts H" |
11189 | 78 |
|
79 |
||
61830 | 80 |
text\<open>Monotonicity\<close> |
76289 | 81 |
lemma parts_mono_aux: "\<lbrakk>G \<subseteq> H; X \<in> parts G\<rbrakk> \<Longrightarrow> X \<in> parts H" |
76288
b82ac7ef65ec
Removal of the "unfold" method in favour of "unfolding"
paulson <lp15@cam.ac.uk>
parents:
76287
diff
changeset
|
82 |
by (erule parts.induct) (auto dest: parts.Fst parts.Snd parts.Body) |
b82ac7ef65ec
Removal of the "unfold" method in favour of "unfolding"
paulson <lp15@cam.ac.uk>
parents:
76287
diff
changeset
|
83 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
84 |
lemma parts_mono: "G \<subseteq> H \<Longrightarrow> parts(G) \<subseteq> parts(H)" |
76288
b82ac7ef65ec
Removal of the "unfold" method in favour of "unfolding"
paulson <lp15@cam.ac.uk>
parents:
76287
diff
changeset
|
85 |
using parts_mono_aux by blast |
1839 | 86 |
|
87 |
||
61830 | 88 |
text\<open>Equations hold because constructors are injective.\<close> |
67613 | 89 |
lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x\<in>A)" |
76288
b82ac7ef65ec
Removal of the "unfold" method in favour of "unfolding"
paulson <lp15@cam.ac.uk>
parents:
76287
diff
changeset
|
90 |
by auto |
13926 | 91 |
|
92 |
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)" |
|
76288
b82ac7ef65ec
Removal of the "unfold" method in favour of "unfolding"
paulson <lp15@cam.ac.uk>
parents:
76287
diff
changeset
|
93 |
by auto |
13926 | 94 |
|
95 |
lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)" |
|
76288
b82ac7ef65ec
Removal of the "unfold" method in favour of "unfolding"
paulson <lp15@cam.ac.uk>
parents:
76287
diff
changeset
|
96 |
by auto |
13926 | 97 |
|
98 |
||
61830 | 99 |
subsubsection\<open>Inverse of keys\<close> |
13926 | 100 |
|
101 |
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')" |
|
76288
b82ac7ef65ec
Removal of the "unfold" method in favour of "unfolding"
paulson <lp15@cam.ac.uk>
parents:
76287
diff
changeset
|
102 |
by (metis invKey) |
13926 | 103 |
|
104 |
||
61830 | 105 |
subsection\<open>keysFor operator\<close> |
13926 | 106 |
|
107 |
lemma keysFor_empty [simp]: "keysFor {} = {}" |
|
76289 | 108 |
unfolding keysFor_def by blast |
13926 | 109 |
|
110 |
lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'" |
|
76289 | 111 |
unfolding keysFor_def by blast |
13926 | 112 |
|
113 |
lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))" |
|
76289 | 114 |
unfolding keysFor_def by blast |
13926 | 115 |
|
61830 | 116 |
text\<open>Monotonicity\<close> |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
117 |
lemma keysFor_mono: "G \<subseteq> H \<Longrightarrow> keysFor(G) \<subseteq> keysFor(H)" |
76289 | 118 |
unfolding keysFor_def by blast |
13926 | 119 |
|
120 |
lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H" |
|
76289 | 121 |
unfolding keysFor_def by auto |
13926 | 122 |
|
123 |
lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H" |
|
76289 | 124 |
unfolding keysFor_def by auto |
13926 | 125 |
|
126 |
lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H" |
|
76289 | 127 |
unfolding keysFor_def by auto |
13926 | 128 |
|
129 |
lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H" |
|
76289 | 130 |
unfolding keysFor_def by auto |
13926 | 131 |
|
132 |
lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H" |
|
76289 | 133 |
unfolding keysFor_def by auto |
13926 | 134 |
|
61956 | 135 |
lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H" |
76289 | 136 |
unfolding keysFor_def by auto |
13926 | 137 |
|
138 |
lemma keysFor_insert_Crypt [simp]: |
|
139 |
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)" |
|
76289 | 140 |
unfolding keysFor_def by auto |
13926 | 141 |
|
142 |
lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}" |
|
76289 | 143 |
unfolding keysFor_def by auto |
13926 | 144 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
145 |
lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H \<Longrightarrow> invKey K \<in> keysFor H" |
76289 | 146 |
unfolding keysFor_def by blast |
13926 | 147 |
|
148 |
||
61830 | 149 |
subsection\<open>Inductive relation "parts"\<close> |
13926 | 150 |
|
151 |
lemma MPair_parts: |
|
76289 | 152 |
"\<lbrakk>\<lbrace>X,Y\<rbrace> \<in> parts H; |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
153 |
\<lbrakk>X \<in> parts H; Y \<in> parts H\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
76289 | 154 |
by (blast dest: parts.Fst parts.Snd) |
13926 | 155 |
|
156 |
declare MPair_parts [elim!] parts.Body [dest!] |
|
61830 | 157 |
text\<open>NB These two rules are UNSAFE in the formal sense, as they discard the |
13926 | 158 |
compound message. They work well on THIS FILE. |
61830 | 159 |
\<open>MPair_parts\<close> is left as SAFE because it speeds up proofs. |
160 |
The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.\<close> |
|
13926 | 161 |
|
162 |
lemma parts_increasing: "H \<subseteq> parts(H)" |
|
76289 | 163 |
by blast |
13926 | 164 |
|
45605 | 165 |
lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD] |
13926 | 166 |
|
76289 | 167 |
lemma parts_empty_aux: "X \<in> parts{} \<Longrightarrow> False" |
168 |
by (induction rule: parts.induct) (blast+) |
|
169 |
||
13926 | 170 |
lemma parts_empty [simp]: "parts{} = {}" |
76289 | 171 |
using parts_empty_aux by blast |
13926 | 172 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
173 |
lemma parts_emptyE [elim!]: "X\<in> parts{} \<Longrightarrow> P" |
76289 | 174 |
by simp |
13926 | 175 |
|
61830 | 176 |
text\<open>WARNING: loops if H = {Y}, therefore must not be repeated!\<close> |
76289 | 177 |
lemma parts_singleton: "X \<in> parts H \<Longrightarrow> \<exists>Y\<in>H. X \<in> parts {Y}" |
178 |
by (erule parts.induct, fast+) |
|
13926 | 179 |
|
180 |
||
61830 | 181 |
subsubsection\<open>Unions\<close> |
13926 | 182 |
|
183 |
lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)" |
|
76289 | 184 |
by (intro Un_least parts_mono Un_upper1 Un_upper2) |
13926 | 185 |
|
186 |
lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)" |
|
76289 | 187 |
apply (rule subsetI) |
188 |
apply (erule parts.induct, blast+) |
|
189 |
done |
|
13926 | 190 |
|
191 |
lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)" |
|
76289 | 192 |
by (intro equalityI parts_Un_subset1 parts_Un_subset2) |
13926 | 193 |
|
194 |
lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H" |
|
76289 | 195 |
by (metis insert_is_Un parts_Un) |
13926 | 196 |
|
61830 | 197 |
text\<open>TWO inserts to avoid looping. This rewrite is better than nothing. |
198 |
But its behaviour can be strange.\<close> |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
199 |
lemma parts_insert2: |
76289 | 200 |
"parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H" |
201 |
by (metis Un_commute Un_empty_right Un_insert_right insert_is_Un parts_Un) |
|
13926 | 202 |
|
203 |
lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)" |
|
76289 | 204 |
by (intro UN_least parts_mono UN_upper) |
13926 | 205 |
|
206 |
lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))" |
|
76289 | 207 |
apply (rule subsetI) |
208 |
apply (erule parts.induct, blast+) |
|
209 |
done |
|
13926 | 210 |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
211 |
lemma parts_UN [simp]: |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
212 |
"parts (\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts (H x))" |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
213 |
by (intro equalityI parts_UN_subset1 parts_UN_subset2) |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
214 |
|
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
215 |
lemma parts_image [simp]: |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
216 |
"parts (f ` A) = (\<Union>x\<in>A. parts {f x})" |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
217 |
apply auto |
76289 | 218 |
apply (metis (mono_tags, opaque_lifting) image_iff parts_singleton) |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
219 |
apply (metis empty_subsetI image_eqI insert_absorb insert_subset parts_mono) |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
220 |
done |
13926 | 221 |
|
61830 | 222 |
text\<open>Added to simplify arguments to parts, analz and synth. |
223 |
NOTE: the UN versions are no longer used!\<close> |
|
13926 | 224 |
|
225 |
||
61830 | 226 |
text\<open>This allows \<open>blast\<close> to simplify occurrences of |
69597 | 227 |
\<^term>\<open>parts(G\<union>H)\<close> in the assumption.\<close> |
17729 | 228 |
lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] |
229 |
declare in_parts_UnE [elim!] |
|
13926 | 230 |
|
231 |
||
232 |
lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)" |
|
76289 | 233 |
by (blast intro: parts_mono [THEN [2] rev_subsetD]) |
13926 | 234 |
|
61830 | 235 |
subsubsection\<open>Idempotence and transitivity\<close> |
13926 | 236 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
237 |
lemma parts_partsD [dest!]: "X\<in> parts (parts H) \<Longrightarrow> X\<in> parts H" |
76289 | 238 |
by (erule parts.induct, blast+) |
13926 | 239 |
|
240 |
lemma parts_idem [simp]: "parts (parts H) = parts H" |
|
76289 | 241 |
by blast |
13926 | 242 |
|
17689
a04b5b43625e
streamlined theory; conformance to recent publication
paulson
parents:
16818
diff
changeset
|
243 |
lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)" |
76289 | 244 |
by (metis parts_idem parts_increasing parts_mono subset_trans) |
17689
a04b5b43625e
streamlined theory; conformance to recent publication
paulson
parents:
16818
diff
changeset
|
245 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
246 |
lemma parts_trans: "\<lbrakk>X\<in> parts G; G \<subseteq> parts H\<rbrakk> \<Longrightarrow> X\<in> parts H" |
76289 | 247 |
by (metis parts_subset_iff subsetD) |
13926 | 248 |
|
61830 | 249 |
text\<open>Cut\<close> |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
250 |
lemma parts_cut: |
76289 | 251 |
"\<lbrakk>Y\<in> parts (insert X G); X\<in> parts H\<rbrakk> \<Longrightarrow> Y\<in> parts (G \<union> H)" |
252 |
by (blast intro: parts_trans) |
|
18492 | 253 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
254 |
lemma parts_cut_eq [simp]: "X\<in> parts H \<Longrightarrow> parts (insert X H) = parts H" |
76289 | 255 |
by (metis insert_absorb parts_idem parts_insert) |
13926 | 256 |
|
257 |
||
61830 | 258 |
subsubsection\<open>Rewrite rules for pulling out atomic messages\<close> |
13926 | 259 |
|
260 |
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset] |
|
261 |
||
262 |
||
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
263 |
lemma parts_insert_Agent [simp]: |
76289 | 264 |
"parts (insert (Agent agt) H) = insert (Agent agt) (parts H)" |
265 |
apply (rule parts_insert_eq_I) |
|
266 |
apply (erule parts.induct, auto) |
|
267 |
done |
|
13926 | 268 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
269 |
lemma parts_insert_Nonce [simp]: |
76289 | 270 |
"parts (insert (Nonce N) H) = insert (Nonce N) (parts H)" |
271 |
apply (rule parts_insert_eq_I) |
|
272 |
apply (erule parts.induct, auto) |
|
273 |
done |
|
13926 | 274 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
275 |
lemma parts_insert_Number [simp]: |
76289 | 276 |
"parts (insert (Number N) H) = insert (Number N) (parts H)" |
277 |
apply (rule parts_insert_eq_I) |
|
278 |
apply (erule parts.induct, auto) |
|
279 |
done |
|
13926 | 280 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
281 |
lemma parts_insert_Key [simp]: |
76289 | 282 |
"parts (insert (Key K) H) = insert (Key K) (parts H)" |
283 |
apply (rule parts_insert_eq_I) |
|
284 |
apply (erule parts.induct, auto) |
|
285 |
done |
|
13926 | 286 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
287 |
lemma parts_insert_Hash [simp]: |
76289 | 288 |
"parts (insert (Hash X) H) = insert (Hash X) (parts H)" |
289 |
apply (rule parts_insert_eq_I) |
|
290 |
apply (erule parts.induct, auto) |
|
291 |
done |
|
13926 | 292 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
293 |
lemma parts_insert_Crypt [simp]: |
76289 | 294 |
"parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))" |
295 |
apply (rule equalityI) |
|
296 |
apply (rule subsetI) |
|
297 |
apply (erule parts.induct, auto) |
|
298 |
apply (blast intro: parts.Body) |
|
299 |
done |
|
13926 | 300 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
301 |
lemma parts_insert_MPair [simp]: |
76289 | 302 |
"parts (insert \<lbrace>X,Y\<rbrace> H) = |
61956 | 303 |
insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))" |
76289 | 304 |
apply (rule equalityI) |
305 |
apply (rule subsetI) |
|
306 |
apply (erule parts.induct, auto) |
|
307 |
apply (blast intro: parts.Fst parts.Snd)+ |
|
308 |
done |
|
13926 | 309 |
|
310 |
lemma parts_image_Key [simp]: "parts (Key`N) = Key`N" |
|
76289 | 311 |
by auto |
13926 | 312 |
|
61830 | 313 |
text\<open>In any message, there is an upper bound N on its greatest nonce.\<close> |
67613 | 314 |
lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> parts {msg}" |
57394 | 315 |
proof (induct msg) |
316 |
case (Nonce n) |
|
76289 | 317 |
show ?case |
318 |
by simp (metis Suc_n_not_le_n) |
|
57394 | 319 |
next |
320 |
case (MPair X Y) |
|
76289 | 321 |
then show ?case \<comment> \<open>metis works out the necessary sum itself!\<close> |
322 |
by (simp add: parts_insert2) (metis le_trans nat_le_linear) |
|
57394 | 323 |
qed auto |
13926 | 324 |
|
61830 | 325 |
subsection\<open>Inductive relation "analz"\<close> |
13926 | 326 |
|
61830 | 327 |
text\<open>Inductive definition of "analz" -- what can be broken down from a set of |
1839 | 328 |
messages, including keys. A form of downward closure. Pairs can |
61830 | 329 |
be taken apart; messages decrypted with known keys.\<close> |
1839 | 330 |
|
23746 | 331 |
inductive_set |
67613 | 332 |
analz :: "msg set \<Rightarrow> msg set" |
23746 | 333 |
for H :: "msg set" |
334 |
where |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
335 |
Inj [intro,simp]: "X \<in> H \<Longrightarrow> X \<in> analz H" |
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
336 |
| Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> X \<in> analz H" |
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
337 |
| Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> Y \<in> analz H" |
23746 | 338 |
| Decrypt [dest]: |
76289 | 339 |
"\<lbrakk>Crypt K X \<in> analz H; Key(invKey K) \<in> analz H\<rbrakk> \<Longrightarrow> X \<in> analz H" |
1839 | 340 |
|
341 |
||
61830 | 342 |
text\<open>Monotonicity; Lemma 1 of Lowe's paper\<close> |
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
343 |
lemma analz_mono_aux: "\<lbrakk>G \<subseteq> H; X \<in> analz G\<rbrakk> \<Longrightarrow> X \<in> analz H" |
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
344 |
by (erule analz.induct) (auto dest: analz.Fst analz.Snd) |
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
345 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
346 |
lemma analz_mono: "G\<subseteq>H \<Longrightarrow> analz(G) \<subseteq> analz(H)" |
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
347 |
using analz_mono_aux by blast |
11189 | 348 |
|
61830 | 349 |
text\<open>Making it safe speeds up proofs\<close> |
13926 | 350 |
lemma MPair_analz [elim!]: |
76289 | 351 |
"\<lbrakk>\<lbrace>X,Y\<rbrace> \<in> analz H; |
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
352 |
\<lbrakk>X \<in> analz H; Y \<in> analz H\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
76289 | 353 |
by (blast dest: analz.Fst analz.Snd) |
13926 | 354 |
|
355 |
lemma analz_increasing: "H \<subseteq> analz(H)" |
|
76289 | 356 |
by blast |
13926 | 357 |
|
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
358 |
lemma analz_into_parts: "X \<in> analz H \<Longrightarrow> X \<in> parts H" |
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
359 |
by (erule analz.induct) auto |
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
360 |
|
13926 | 361 |
lemma analz_subset_parts: "analz H \<subseteq> parts H" |
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
362 |
using analz_into_parts by blast |
13926 | 363 |
|
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
364 |
lemma analz_parts [simp]: "analz (parts H) = parts H" |
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
365 |
using analz_subset_parts by blast |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
366 |
|
45605 | 367 |
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD] |
13926 | 368 |
|
369 |
||
370 |
lemma parts_analz [simp]: "parts (analz H) = parts H" |
|
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
371 |
by (metis analz_increasing analz_subset_parts parts_idem parts_mono subset_antisym) |
13926 | 372 |
|
45605 | 373 |
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD] |
13926 | 374 |
|
61830 | 375 |
subsubsection\<open>General equational properties\<close> |
13926 | 376 |
|
377 |
lemma analz_empty [simp]: "analz{} = {}" |
|
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
378 |
using analz_parts by fastforce |
13926 | 379 |
|
61830 | 380 |
text\<open>Converse fails: we can analz more from the union than from the |
381 |
separate parts, as a key in one might decrypt a message in the other\<close> |
|
13926 | 382 |
lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)" |
76289 | 383 |
by (intro Un_least analz_mono Un_upper1 Un_upper2) |
13926 | 384 |
|
385 |
lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)" |
|
76289 | 386 |
by (blast intro: analz_mono [THEN [2] rev_subsetD]) |
13926 | 387 |
|
61830 | 388 |
subsubsection\<open>Rewrite rules for pulling out atomic messages\<close> |
13926 | 389 |
|
390 |
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert] |
|
391 |
||
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
392 |
lemma analz_insert_Agent [simp]: |
76289 | 393 |
"analz (insert (Agent agt) H) = insert (Agent agt) (analz H)" |
394 |
apply (rule analz_insert_eq_I) |
|
395 |
apply (erule analz.induct, auto) |
|
396 |
done |
|
13926 | 397 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
398 |
lemma analz_insert_Nonce [simp]: |
76289 | 399 |
"analz (insert (Nonce N) H) = insert (Nonce N) (analz H)" |
400 |
apply (rule analz_insert_eq_I) |
|
401 |
apply (erule analz.induct, auto) |
|
402 |
done |
|
13926 | 403 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
404 |
lemma analz_insert_Number [simp]: |
76289 | 405 |
"analz (insert (Number N) H) = insert (Number N) (analz H)" |
406 |
apply (rule analz_insert_eq_I) |
|
407 |
apply (erule analz.induct, auto) |
|
408 |
done |
|
13926 | 409 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
410 |
lemma analz_insert_Hash [simp]: |
76289 | 411 |
"analz (insert (Hash X) H) = insert (Hash X) (analz H)" |
412 |
apply (rule analz_insert_eq_I) |
|
413 |
apply (erule analz.induct, auto) |
|
414 |
done |
|
13926 | 415 |
|
61830 | 416 |
text\<open>Can only pull out Keys if they are not needed to decrypt the rest\<close> |
13926 | 417 |
lemma analz_insert_Key [simp]: |
76289 | 418 |
"K \<notin> keysFor (analz H) \<Longrightarrow> |
13926 | 419 |
analz (insert (Key K) H) = insert (Key K) (analz H)" |
76290
64d29ebb7d3d
Mostly, removing the unfold method
paulson <lp15@cam.ac.uk>
parents:
76289
diff
changeset
|
420 |
unfolding keysFor_def |
76289 | 421 |
apply (rule analz_insert_eq_I) |
422 |
apply (erule analz.induct, auto) |
|
423 |
done |
|
13926 | 424 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
425 |
lemma analz_insert_MPair [simp]: |
76289 | 426 |
"analz (insert \<lbrace>X,Y\<rbrace> H) = |
61956 | 427 |
insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))" |
76289 | 428 |
apply (rule equalityI) |
429 |
apply (rule subsetI) |
|
430 |
apply (erule analz.induct, auto) |
|
431 |
apply (erule analz.induct) |
|
432 |
apply (blast intro: analz.Fst analz.Snd)+ |
|
433 |
done |
|
13926 | 434 |
|
61830 | 435 |
text\<open>Can pull out enCrypted message if the Key is not known\<close> |
13926 | 436 |
lemma analz_insert_Crypt: |
76289 | 437 |
"Key (invKey K) \<notin> analz H |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
438 |
\<Longrightarrow> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)" |
76289 | 439 |
apply (rule analz_insert_eq_I) |
440 |
apply (erule analz.induct, auto) |
|
13926 | 441 |
|
76289 | 442 |
done |
13926 | 443 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
444 |
lemma lemma1: "Key (invKey K) \<in> analz H \<Longrightarrow> |
13926 | 445 |
analz (insert (Crypt K X) H) \<subseteq> |
446 |
insert (Crypt K X) (analz (insert X H))" |
|
76289 | 447 |
apply (rule subsetI) |
448 |
apply (erule_tac x = x in analz.induct, auto) |
|
449 |
done |
|
13926 | 450 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
451 |
lemma lemma2: "Key (invKey K) \<in> analz H \<Longrightarrow> |
13926 | 452 |
insert (Crypt K X) (analz (insert X H)) \<subseteq> |
453 |
analz (insert (Crypt K X) H)" |
|
76289 | 454 |
apply auto |
455 |
apply (erule_tac x = x in analz.induct, auto) |
|
456 |
apply (blast intro: analz_insertI analz.Decrypt) |
|
457 |
done |
|
13926 | 458 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
459 |
lemma analz_insert_Decrypt: |
76289 | 460 |
"Key (invKey K) \<in> analz H \<Longrightarrow> |
13926 | 461 |
analz (insert (Crypt K X) H) = |
462 |
insert (Crypt K X) (analz (insert X H))" |
|
76289 | 463 |
by (intro equalityI lemma1 lemma2) |
13926 | 464 |
|
61830 | 465 |
text\<open>Case analysis: either the message is secure, or it is not! Effective, |
62390 | 466 |
but can cause subgoals to blow up! Use with \<open>if_split\<close>; apparently |
69597 | 467 |
\<open>split_tac\<close> does not cope with patterns such as \<^term>\<open>analz (insert |
468 |
(Crypt K X) H)\<close>\<close> |
|
13926 | 469 |
lemma analz_Crypt_if [simp]: |
76289 | 470 |
"analz (insert (Crypt K X) H) = |
13926 | 471 |
(if (Key (invKey K) \<in> analz H) |
472 |
then insert (Crypt K X) (analz (insert X H)) |
|
473 |
else insert (Crypt K X) (analz H))" |
|
76289 | 474 |
by (simp add: analz_insert_Crypt analz_insert_Decrypt) |
13926 | 475 |
|
476 |
||
61830 | 477 |
text\<open>This rule supposes "for the sake of argument" that we have the key.\<close> |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
478 |
lemma analz_insert_Crypt_subset: |
76289 | 479 |
"analz (insert (Crypt K X) H) \<subseteq> |
13926 | 480 |
insert (Crypt K X) (analz (insert X H))" |
76289 | 481 |
apply (rule subsetI) |
482 |
apply (erule analz.induct, auto) |
|
483 |
done |
|
13926 | 484 |
|
485 |
||
486 |
lemma analz_image_Key [simp]: "analz (Key`N) = Key`N" |
|
76289 | 487 |
apply auto |
488 |
apply (erule analz.induct, auto) |
|
489 |
done |
|
13926 | 490 |
|
491 |
||
61830 | 492 |
subsubsection\<open>Idempotence and transitivity\<close> |
13926 | 493 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
494 |
lemma analz_analzD [dest!]: "X\<in> analz (analz H) \<Longrightarrow> X\<in> analz H" |
76289 | 495 |
by (erule analz.induct, blast+) |
13926 | 496 |
|
497 |
lemma analz_idem [simp]: "analz (analz H) = analz H" |
|
76289 | 498 |
by blast |
13926 | 499 |
|
17689
a04b5b43625e
streamlined theory; conformance to recent publication
paulson
parents:
16818
diff
changeset
|
500 |
lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)" |
76289 | 501 |
by (metis analz_idem analz_increasing analz_mono subset_trans) |
17689
a04b5b43625e
streamlined theory; conformance to recent publication
paulson
parents:
16818
diff
changeset
|
502 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
503 |
lemma analz_trans: "\<lbrakk>X\<in> analz G; G \<subseteq> analz H\<rbrakk> \<Longrightarrow> X\<in> analz H" |
76289 | 504 |
by (drule analz_mono, blast) |
13926 | 505 |
|
61830 | 506 |
text\<open>Cut; Lemma 2 of Lowe\<close> |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
507 |
lemma analz_cut: "\<lbrakk>Y\<in> analz (insert X H); X\<in> analz H\<rbrakk> \<Longrightarrow> Y\<in> analz H" |
76289 | 508 |
by (erule analz_trans, blast) |
13926 | 509 |
|
510 |
(*Cut can be proved easily by induction on |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
511 |
"Y: analz (insert X H) \<Longrightarrow> X: analz H \<longrightarrow> Y: analz H" |
13926 | 512 |
*) |
513 |
||
61830 | 514 |
text\<open>This rewrite rule helps in the simplification of messages that involve |
13926 | 515 |
the forwarding of unknown components (X). Without it, removing occurrences |
61830 | 516 |
of X can be very complicated.\<close> |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
517 |
lemma analz_insert_eq: "X\<in> analz H \<Longrightarrow> analz (insert X H) = analz H" |
76289 | 518 |
by (metis analz_cut analz_insert_eq_I insert_absorb) |
13926 | 519 |
|
520 |
||
61830 | 521 |
text\<open>A congruence rule for "analz"\<close> |
13926 | 522 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
523 |
lemma analz_subset_cong: |
76289 | 524 |
"\<lbrakk>analz G \<subseteq> analz G'; analz H \<subseteq> analz H'\<rbrakk> |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
525 |
\<Longrightarrow> analz (G \<union> H) \<subseteq> analz (G' \<union> H')" |
76289 | 526 |
by (metis Un_mono analz_Un analz_subset_iff subset_trans) |
13926 | 527 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
528 |
lemma analz_cong: |
76289 | 529 |
"\<lbrakk>analz G = analz G'; analz H = analz H'\<rbrakk> |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
530 |
\<Longrightarrow> analz (G \<union> H) = analz (G' \<union> H')" |
76289 | 531 |
by (intro equalityI analz_subset_cong, simp_all) |
13926 | 532 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
533 |
lemma analz_insert_cong: |
76289 | 534 |
"analz H = analz H' \<Longrightarrow> analz(insert X H) = analz(insert X H')" |
535 |
by (force simp only: insert_def intro!: analz_cong) |
|
13926 | 536 |
|
61830 | 537 |
text\<open>If there are no pairs or encryptions then analz does nothing\<close> |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
538 |
lemma analz_trivial: |
76289 | 539 |
"\<lbrakk>\<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H; \<forall>X K. Crypt K X \<notin> H\<rbrakk> \<Longrightarrow> analz H = H" |
540 |
apply safe |
|
541 |
apply (erule analz.induct, blast+) |
|
542 |
done |
|
13926 | 543 |
|
61830 | 544 |
text\<open>These two are obsolete (with a single Spy) but cost little to prove...\<close> |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
545 |
lemma analz_UN_analz_lemma: |
76289 | 546 |
"X\<in> analz (\<Union>i\<in>A. analz (H i)) \<Longrightarrow> X\<in> analz (\<Union>i\<in>A. H i)" |
547 |
apply (erule analz.induct) |
|
548 |
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+ |
|
549 |
done |
|
13926 | 550 |
|
551 |
lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)" |
|
76289 | 552 |
by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD]) |
13926 | 553 |
|
554 |
||
61830 | 555 |
subsection\<open>Inductive relation "synth"\<close> |
13926 | 556 |
|
61830 | 557 |
text\<open>Inductive definition of "synth" -- what can be built up from a set of |
1839 | 558 |
messages. A form of upward closure. Pairs can be built, messages |
3668 | 559 |
encrypted with known keys. Agent names are public domain. |
61830 | 560 |
Numbers can be guessed, but Nonces cannot be.\<close> |
1839 | 561 |
|
23746 | 562 |
inductive_set |
563 |
synth :: "msg set => msg set" |
|
564 |
for H :: "msg set" |
|
565 |
where |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
566 |
Inj [intro]: "X \<in> H \<Longrightarrow> X \<in> synth H" |
23746 | 567 |
| Agent [intro]: "Agent agt \<in> synth H" |
568 |
| Number [intro]: "Number n \<in> synth H" |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
569 |
| Hash [intro]: "X \<in> synth H \<Longrightarrow> Hash X \<in> synth H" |
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
570 |
| MPair [intro]: "\<lbrakk>X \<in> synth H; Y \<in> synth H\<rbrakk> \<Longrightarrow> \<lbrace>X,Y\<rbrace> \<in> synth H" |
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
571 |
| Crypt [intro]: "\<lbrakk>X \<in> synth H; Key(K) \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H" |
11189 | 572 |
|
61830 | 573 |
text\<open>Monotonicity\<close> |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
574 |
lemma synth_mono: "G\<subseteq>H \<Longrightarrow> synth(G) \<subseteq> synth(H)" |
16818 | 575 |
by (auto, erule synth.induct, auto) |
11189 | 576 |
|
61830 | 577 |
text\<open>NO \<open>Agent_synth\<close>, as any Agent name can be synthesized. |
69597 | 578 |
The same holds for \<^term>\<open>Number\<close>\<close> |
11189 | 579 |
|
39216 | 580 |
inductive_simps synth_simps [iff]: |
76289 | 581 |
"Nonce n \<in> synth H" |
582 |
"Key K \<in> synth H" |
|
583 |
"Hash X \<in> synth H" |
|
584 |
"\<lbrace>X,Y\<rbrace> \<in> synth H" |
|
585 |
"Crypt K X \<in> synth H" |
|
13926 | 586 |
|
587 |
lemma synth_increasing: "H \<subseteq> synth(H)" |
|
76289 | 588 |
by blast |
13926 | 589 |
|
61830 | 590 |
subsubsection\<open>Unions\<close> |
13926 | 591 |
|
61830 | 592 |
text\<open>Converse fails: we can synth more from the union than from the |
593 |
separate parts, building a compound message using elements of each.\<close> |
|
13926 | 594 |
lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)" |
76289 | 595 |
by (intro Un_least synth_mono Un_upper1 Un_upper2) |
13926 | 596 |
|
597 |
lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)" |
|
76289 | 598 |
by (blast intro: synth_mono [THEN [2] rev_subsetD]) |
13926 | 599 |
|
61830 | 600 |
subsubsection\<open>Idempotence and transitivity\<close> |
13926 | 601 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
602 |
lemma synth_synthD [dest!]: "X\<in> synth (synth H) \<Longrightarrow> X\<in> synth H" |
76289 | 603 |
by (erule synth.induct, auto) |
13926 | 604 |
|
605 |
lemma synth_idem: "synth (synth H) = synth H" |
|
76289 | 606 |
by blast |
13926 | 607 |
|
17689
a04b5b43625e
streamlined theory; conformance to recent publication
paulson
parents:
16818
diff
changeset
|
608 |
lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)" |
76289 | 609 |
by (metis subset_trans synth_idem synth_increasing synth_mono) |
17689
a04b5b43625e
streamlined theory; conformance to recent publication
paulson
parents:
16818
diff
changeset
|
610 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
611 |
lemma synth_trans: "\<lbrakk>X\<in> synth G; G \<subseteq> synth H\<rbrakk> \<Longrightarrow> X\<in> synth H" |
76289 | 612 |
by (drule synth_mono, blast) |
13926 | 613 |
|
61830 | 614 |
text\<open>Cut; Lemma 2 of Lowe\<close> |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
615 |
lemma synth_cut: "\<lbrakk>Y\<in> synth (insert X H); X\<in> synth H\<rbrakk> \<Longrightarrow> Y\<in> synth H" |
76289 | 616 |
by (erule synth_trans, blast) |
13926 | 617 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
618 |
lemma Crypt_synth_eq [simp]: |
76289 | 619 |
"Key K \<notin> H \<Longrightarrow> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)" |
620 |
by blast |
|
13926 | 621 |
|
622 |
||
623 |
lemma keysFor_synth [simp]: |
|
76289 | 624 |
"keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}" |
625 |
unfolding keysFor_def by blast |
|
13926 | 626 |
|
627 |
||
61830 | 628 |
subsubsection\<open>Combinations of parts, analz and synth\<close> |
13926 | 629 |
|
630 |
lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H" |
|
76289 | 631 |
apply (rule equalityI) |
632 |
apply (rule subsetI) |
|
633 |
apply (erule parts.induct) |
|
634 |
apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] |
|
635 |
parts.Fst parts.Snd parts.Body)+ |
|
636 |
done |
|
13926 | 637 |
|
638 |
lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)" |
|
76289 | 639 |
apply (intro equalityI analz_subset_cong)+ |
640 |
apply simp_all |
|
641 |
done |
|
13926 | 642 |
|
643 |
lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G" |
|
76289 | 644 |
apply (rule equalityI) |
645 |
apply (rule subsetI) |
|
646 |
apply (erule analz.induct) |
|
647 |
prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD]) |
|
648 |
apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+ |
|
649 |
done |
|
13926 | 650 |
|
651 |
lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H" |
|
76289 | 652 |
by (metis Un_empty_right analz_synth_Un) |
13926 | 653 |
|
654 |
||
61830 | 655 |
subsubsection\<open>For reasoning about the Fake rule in traces\<close> |
13926 | 656 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
657 |
lemma parts_insert_subset_Un: "X\<in> G \<Longrightarrow> parts(insert X H) \<subseteq> parts G \<union> parts H" |
76289 | 658 |
by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono) |
13926 | 659 |
|
61830 | 660 |
text\<open>More specifically for Fake. See also \<open>Fake_parts_sing\<close> below\<close> |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
661 |
lemma Fake_parts_insert: |
76289 | 662 |
"X \<in> synth (analz H) \<Longrightarrow> |
13926 | 663 |
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H" |
76289 | 664 |
by (metis Un_commute analz_increasing insert_subset parts_analz parts_mono |
665 |
parts_synth synth_mono synth_subset_iff) |
|
13926 | 666 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
667 |
lemma Fake_parts_insert_in_Un: |
76289 | 668 |
"\<lbrakk>Z \<in> parts (insert X H); X \<in> synth (analz H)\<rbrakk> |
67613 | 669 |
\<Longrightarrow> Z \<in> synth (analz H) \<union> parts H" |
76289 | 670 |
by (metis Fake_parts_insert subsetD) |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
671 |
|
69597 | 672 |
text\<open>\<^term>\<open>H\<close> is sometimes \<^term>\<open>Key ` KK \<union> spies evs\<close>, so can't put |
673 |
\<^term>\<open>G=H\<close>.\<close> |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
674 |
lemma Fake_analz_insert: |
76289 | 675 |
"X\<in> synth (analz G) \<Longrightarrow> |
13926 | 676 |
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)" |
76289 | 677 |
by (metis UnCI Un_commute Un_upper1 analz_analz_Un analz_mono analz_synth_Un insert_subset) |
13926 | 678 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
679 |
lemma analz_conj_parts [simp]: |
76289 | 680 |
"(X \<in> analz H \<and> X \<in> parts H) = (X \<in> analz H)" |
681 |
by (blast intro: analz_subset_parts [THEN subsetD]) |
|
13926 | 682 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
683 |
lemma analz_disj_parts [simp]: |
76289 | 684 |
"(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)" |
685 |
by (blast intro: analz_subset_parts [THEN subsetD]) |
|
13926 | 686 |
|
61830 | 687 |
text\<open>Without this equation, other rules for synth and analz would yield |
688 |
redundant cases\<close> |
|
13926 | 689 |
lemma MPair_synth_analz [iff]: |
76289 | 690 |
"\<lbrace>X,Y\<rbrace> \<in> synth (analz H) \<longleftrightarrow> X \<in> synth (analz H) \<and> Y \<in> synth (analz H)" |
691 |
by blast |
|
13926 | 692 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
693 |
lemma Crypt_synth_analz: |
76289 | 694 |
"\<lbrakk>Key K \<in> analz H; Key (invKey K) \<in> analz H\<rbrakk> |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
695 |
\<Longrightarrow> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))" |
76289 | 696 |
by blast |
13926 | 697 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
698 |
lemma Hash_synth_analz [simp]: |
76289 | 699 |
"X \<notin> synth (analz H) |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
700 |
\<Longrightarrow> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)" |
76289 | 701 |
by blast |
13926 | 702 |
|
703 |
||
61830 | 704 |
subsection\<open>HPair: a combination of Hash and MPair\<close> |
13926 | 705 |
|
61830 | 706 |
subsubsection\<open>Freeness\<close> |
13926 | 707 |
|
67613 | 708 |
lemma Agent_neq_HPair: "Agent A \<noteq> Hash[X] Y" |
57394 | 709 |
unfolding HPair_def by simp |
13926 | 710 |
|
67613 | 711 |
lemma Nonce_neq_HPair: "Nonce N \<noteq> Hash[X] Y" |
57394 | 712 |
unfolding HPair_def by simp |
13926 | 713 |
|
67613 | 714 |
lemma Number_neq_HPair: "Number N \<noteq> Hash[X] Y" |
57394 | 715 |
unfolding HPair_def by simp |
13926 | 716 |
|
67613 | 717 |
lemma Key_neq_HPair: "Key K \<noteq> Hash[X] Y" |
57394 | 718 |
unfolding HPair_def by simp |
13926 | 719 |
|
67613 | 720 |
lemma Hash_neq_HPair: "Hash Z \<noteq> Hash[X] Y" |
57394 | 721 |
unfolding HPair_def by simp |
13926 | 722 |
|
67613 | 723 |
lemma Crypt_neq_HPair: "Crypt K X' \<noteq> Hash[X] Y" |
57394 | 724 |
unfolding HPair_def by simp |
13926 | 725 |
|
726 |
lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair |
|
76289 | 727 |
Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair |
13926 | 728 |
|
729 |
declare HPair_neqs [iff] |
|
730 |
declare HPair_neqs [symmetric, iff] |
|
731 |
||
67613 | 732 |
lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X \<and> Y'=Y)" |
76289 | 733 |
by (simp add: HPair_def) |
13926 | 734 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
735 |
lemma MPair_eq_HPair [iff]: |
76289 | 736 |
"(\<lbrace>X',Y'\<rbrace> = Hash[X] Y) = (X' = Hash\<lbrace>X,Y\<rbrace> \<and> Y'=Y)" |
737 |
by (simp add: HPair_def) |
|
13926 | 738 |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
739 |
lemma HPair_eq_MPair [iff]: |
76289 | 740 |
"(Hash[X] Y = \<lbrace>X',Y'\<rbrace>) = (X' = Hash\<lbrace>X,Y\<rbrace> \<and> Y'=Y)" |
741 |
by (auto simp add: HPair_def) |
|
13926 | 742 |
|
743 |
||
61830 | 744 |
subsubsection\<open>Specialized laws, proved in terms of those for Hash and MPair\<close> |
13926 | 745 |
|
746 |
lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H" |
|
76289 | 747 |
by (simp add: HPair_def) |
13926 | 748 |
|
749 |
lemma parts_insert_HPair [simp]: |
|
76289 | 750 |
"parts (insert (Hash[X] Y) H) = |
61956 | 751 |
insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (parts (insert Y H)))" |
76289 | 752 |
by (simp add: HPair_def) |
13926 | 753 |
|
754 |
lemma analz_insert_HPair [simp]: |
|
76289 | 755 |
"analz (insert (Hash[X] Y) H) = |
61956 | 756 |
insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (analz (insert Y H)))" |
76289 | 757 |
by (simp add: HPair_def) |
13926 | 758 |
|
759 |
lemma HPair_synth_analz [simp]: |
|
76289 | 760 |
"X \<notin> synth (analz H) |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
761 |
\<Longrightarrow> (Hash[X] Y \<in> synth (analz H)) = |
67613 | 762 |
(Hash \<lbrace>X, Y\<rbrace> \<in> analz H \<and> Y \<in> synth (analz H))" |
76289 | 763 |
by (auto simp add: HPair_def) |
13926 | 764 |
|
765 |
||
61830 | 766 |
text\<open>We do NOT want Crypt... messages broken up in protocols!!\<close> |
13926 | 767 |
declare parts.Body [rule del] |
768 |
||
769 |
||
61830 | 770 |
text\<open>Rewrites to push in Key and Crypt messages, so that other messages can |
771 |
be pulled out using the \<open>analz_insert\<close> rules\<close> |
|
13926 | 772 |
|
45605 | 773 |
lemmas pushKeys = |
27225 | 774 |
insert_commute [of "Key K" "Agent C"] |
775 |
insert_commute [of "Key K" "Nonce N"] |
|
776 |
insert_commute [of "Key K" "Number N"] |
|
777 |
insert_commute [of "Key K" "Hash X"] |
|
778 |
insert_commute [of "Key K" "MPair X Y"] |
|
779 |
insert_commute [of "Key K" "Crypt X K'"] |
|
45605 | 780 |
for K C N X Y K' |
13926 | 781 |
|
45605 | 782 |
lemmas pushCrypts = |
27225 | 783 |
insert_commute [of "Crypt X K" "Agent C"] |
784 |
insert_commute [of "Crypt X K" "Agent C"] |
|
785 |
insert_commute [of "Crypt X K" "Nonce N"] |
|
786 |
insert_commute [of "Crypt X K" "Number N"] |
|
787 |
insert_commute [of "Crypt X K" "Hash X'"] |
|
788 |
insert_commute [of "Crypt X K" "MPair X' Y"] |
|
45605 | 789 |
for X K C N X' Y |
13926 | 790 |
|
61830 | 791 |
text\<open>Cannot be added with \<open>[simp]\<close> -- messages should not always be |
792 |
re-ordered.\<close> |
|
13926 | 793 |
lemmas pushes = pushKeys pushCrypts |
794 |
||
795 |
||
61830 | 796 |
subsection\<open>The set of key-free messages\<close> |
43582
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
797 |
|
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
798 |
(*Note that even the encryption of a key-free message remains key-free. |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
799 |
This concept is valuable because of the theorem analz_keyfree_into_Un, proved below. *) |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
800 |
|
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
801 |
inductive_set |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
802 |
keyfree :: "msg set" |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
803 |
where |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
804 |
Agent: "Agent A \<in> keyfree" |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
805 |
| Number: "Number N \<in> keyfree" |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
806 |
| Nonce: "Nonce N \<in> keyfree" |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
807 |
| Hash: "Hash X \<in> keyfree" |
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
808 |
| MPair: "\<lbrakk>X \<in> keyfree; Y \<in> keyfree\<rbrakk> \<Longrightarrow> \<lbrace>X,Y\<rbrace> \<in> keyfree" |
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
809 |
| Crypt: "\<lbrakk>X \<in> keyfree\<rbrakk> \<Longrightarrow> Crypt K X \<in> keyfree" |
43582
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
810 |
|
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
811 |
|
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
812 |
declare keyfree.intros [intro] |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
813 |
|
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
814 |
inductive_cases keyfree_KeyE: "Key K \<in> keyfree" |
61956 | 815 |
inductive_cases keyfree_MPairE: "\<lbrace>X,Y\<rbrace> \<in> keyfree" |
43582
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
816 |
inductive_cases keyfree_CryptE: "Crypt K X \<in> keyfree" |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
817 |
|
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
818 |
lemma parts_keyfree: "parts (keyfree) \<subseteq> keyfree" |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
819 |
by (clarify, erule parts.induct, auto elim!: keyfree_KeyE keyfree_MPairE keyfree_CryptE) |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
820 |
|
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
821 |
(*The key-free part of a set of messages can be removed from the scope of the analz operator.*) |
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
822 |
lemma analz_keyfree_into_Un: "\<lbrakk>X \<in> analz (G \<union> H); G \<subseteq> keyfree\<rbrakk> \<Longrightarrow> X \<in> parts G \<union> analz H" |
76291
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
823 |
proof (induction rule: analz.induct) |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
824 |
case (Decrypt K X) |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
825 |
then show ?case |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
826 |
by (metis Un_iff analz.Decrypt in_mono keyfree_KeyE parts.Body parts_keyfree parts_mono) |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
827 |
qed (auto dest: parts.Body) |
43582
ddca453102ab
keyfree: The set of key-free messages (and associated theorems)
paulson
parents:
42793
diff
changeset
|
828 |
|
61830 | 829 |
subsection\<open>Tactics useful for many protocol proofs\<close> |
13926 | 830 |
ML |
76289 | 831 |
\<open> |
13926 | 832 |
(*Analysis of Fake cases. Also works for messages that forward unknown parts, |
833 |
but this application is no longer necessary if analz_insert_eq is used. |
|
834 |
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) |
|
835 |
||
32117
0762b9ad83df
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
haftmann
parents:
30607
diff
changeset
|
836 |
fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) |
0762b9ad83df
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
haftmann
parents:
30607
diff
changeset
|
837 |
|
13926 | 838 |
(*Apply rules to break down assumptions of the form |
839 |
Y \<in> parts(insert X H) and Y \<in> analz(insert X H) |
|
840 |
*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
841 |
fun Fake_insert_tac ctxt = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
842 |
dresolve_tac ctxt [impOfSubs @{thm Fake_analz_insert}, |
24122 | 843 |
impOfSubs @{thm Fake_parts_insert}] THEN' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
844 |
eresolve_tac ctxt [asm_rl, @{thm synth.Inj}]; |
13926 | 845 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51702
diff
changeset
|
846 |
fun Fake_insert_simp_tac ctxt i = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
847 |
REPEAT (Fake_insert_tac ctxt i) THEN asm_full_simp_tac ctxt i; |
13926 | 848 |
|
42474 | 849 |
fun atomic_spy_analz_tac ctxt = |
42793 | 850 |
SELECT_GOAL |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51702
diff
changeset
|
851 |
(Fake_insert_simp_tac ctxt 1 THEN |
42793 | 852 |
IF_UNSOLVED |
853 |
(Blast.depth_tac |
|
854 |
(ctxt addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1)); |
|
13926 | 855 |
|
42474 | 856 |
fun spy_analz_tac ctxt i = |
42793 | 857 |
DETERM |
858 |
(SELECT_GOAL |
|
859 |
(EVERY |
|
860 |
[ (*push in occurrences of X...*) |
|
861 |
(REPEAT o CHANGED) |
|
59780 | 862 |
(Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] [] |
863 |
(insert_commute RS ssubst) 1), |
|
42793 | 864 |
(*...allowing further simplifications*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51702
diff
changeset
|
865 |
simp_tac ctxt 1, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
866 |
REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), |
42793 | 867 |
DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
61830 | 868 |
\<close> |
13926 | 869 |
|
61830 | 870 |
text\<open>By default only \<open>o_apply\<close> is built-in. But in the presence of |
69597 | 871 |
eta-expansion this means that some terms displayed as \<^term>\<open>f o g\<close> will be |
61830 | 872 |
rewritten, and others will not!\<close> |
13926 | 873 |
declare o_def [simp] |
874 |
||
11189 | 875 |
|
13922 | 876 |
lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A" |
76289 | 877 |
by auto |
13922 | 878 |
|
879 |
lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A" |
|
76289 | 880 |
by auto |
13922 | 881 |
|
76287
cdc14f94c754
Elimination of the archaic ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
73932
diff
changeset
|
882 |
lemma synth_analz_mono: "G\<subseteq>H \<Longrightarrow> synth (analz(G)) \<subseteq> synth (analz(H))" |
76289 | 883 |
by (iprover intro: synth_mono analz_mono) |
13922 | 884 |
|
885 |
lemma Fake_analz_eq [simp]: |
|
76289 | 886 |
"X \<in> synth(analz H) \<Longrightarrow> synth (analz (insert X H)) = synth (analz H)" |
887 |
by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute |
|
888 |
subset_insertI synth_analz_mono synth_increasing synth_subset_iff) |
|
13922 | 889 |
|
61830 | 890 |
text\<open>Two generalizations of \<open>analz_insert_eq\<close>\<close> |
13922 | 891 |
lemma gen_analz_insert_eq [rule_format]: |
76289 | 892 |
"X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> analz (insert X G) = analz G" |
893 |
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD]) |
|
13922 | 894 |
|
76291
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
895 |
lemma synth_analz_insert_eq: |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
896 |
"\<lbrakk>X \<in> synth (analz H); H \<subseteq> G\<rbrakk> |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
897 |
\<Longrightarrow> (Key K \<in> analz (insert X G)) \<longleftrightarrow> (Key K \<in> analz G)" |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
898 |
proof (induction arbitrary: G rule: synth.induct) |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
899 |
case (Inj X) |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
900 |
then show ?case |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
901 |
using gen_analz_insert_eq by presburger |
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
76290
diff
changeset
|
902 |
qed (simp_all add: subset_eq) |
13922 | 903 |
|
904 |
lemma Fake_parts_sing: |
|
76289 | 905 |
"X \<in> synth (analz H) \<Longrightarrow> parts{X} \<subseteq> synth (analz H) \<union> parts H" |
906 |
by (metis Fake_parts_insert empty_subsetI insert_mono parts_mono subset_trans) |
|
13922 | 907 |
|
14145
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
14126
diff
changeset
|
908 |
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
14126
diff
changeset
|
909 |
|
61830 | 910 |
method_setup spy_analz = \<open> |
911 |
Scan.succeed (SIMPLE_METHOD' o spy_analz_tac)\<close> |
|
76289 | 912 |
"for proving the Fake case when analz is involved" |
1839 | 913 |
|
61830 | 914 |
method_setup atomic_spy_analz = \<open> |
915 |
Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac)\<close> |
|
76289 | 916 |
"for debugging spy_analz" |
11264 | 917 |
|
61830 | 918 |
method_setup Fake_insert_simp = \<open> |
919 |
Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac)\<close> |
|
76289 | 920 |
"for debugging spy_analz" |
11264 | 921 |
|
1839 | 922 |
end |