author | paulson |
Sat, 26 Apr 2003 12:38:42 +0200 | |
changeset 13926 | 6e62e5357a10 |
parent 13507 | febb8e5d2a9d |
child 13956 | 8fe7e12290e1 |
permissions | -rw-r--r-- |
1995 | 1 |
(* Title: HOL/Auth/Yahalom |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
4 |
Copyright 1996 University of Cambridge |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
5 |
|
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
6 |
Inductive relation "yahalom" for the Yahalom protocol. |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
7 |
|
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
8 |
From page 257 of |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
9 |
Burrows, Abadi and Needham. A Logic of Authentication. |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
10 |
Proc. Royal Soc. 426 (1989) |
11251 | 11 |
|
12 |
This theory has the prototypical example of a secrecy relation, KeyCryptNonce. |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
13 |
*) |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
14 |
|
11251 | 15 |
theory Yahalom = Shared: |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
16 |
|
11251 | 17 |
consts yahalom :: "event list set" |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset
|
18 |
inductive "yahalom" |
11251 | 19 |
intros |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
20 |
(*Initial trace is empty*) |
11251 | 21 |
Nil: "[] \<in> yahalom" |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
22 |
|
2032 | 23 |
(*The spy MAY say anything he CAN say. We do not expect him to |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
24 |
invent new nonces here, but he can also use NS1. Common to |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
25 |
all similar protocols.*) |
11251 | 26 |
Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |] |
27 |
==> Says Spy B X # evsf \<in> yahalom" |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
28 |
|
6335 | 29 |
(*A message that has been sent can be received by the |
30 |
intended recipient.*) |
|
11251 | 31 |
Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |] |
32 |
==> Gets B X # evsr \<in> yahalom" |
|
6335 | 33 |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
34 |
(*Alice initiates a protocol run*) |
11251 | 35 |
YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |] |
36 |
==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom" |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
37 |
|
6335 | 38 |
(*Bob's response to Alice's message.*) |
11251 | 39 |
YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2; |
40 |
Gets B {|Agent A, Nonce NA|} \<in> set evs2 |] |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
41 |
==> Says B Server |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
42 |
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
11251 | 43 |
# evs2 \<in> yahalom" |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
44 |
|
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
45 |
(*The Server receives Bob's message. He responds by sending a |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
46 |
new session key to Alice, with a packet for forwarding to Bob.*) |
11251 | 47 |
YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; |
6335 | 48 |
Gets Server |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset
|
49 |
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
11251 | 50 |
\<in> set evs3 |] |
1995 | 51 |
==> Says Server A |
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset
|
52 |
{|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset
|
53 |
Crypt (shrK B) {|Agent A, Key KAB|}|} |
11251 | 54 |
# evs3 \<in> yahalom" |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
55 |
|
1995 | 56 |
(*Alice receives the Server's (?) message, checks her Nonce, and |
3961 | 57 |
uses the new session key to send Bob his Nonce. The premise |
11251 | 58 |
A \<noteq> Server is needed to prove Says_Server_not_range.*) |
59 |
YM4: "[| evs4 \<in> yahalom; A \<noteq> Server; |
|
6335 | 60 |
Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} |
11251 | 61 |
\<in> set evs4; |
62 |
Says A B {|Agent A, Nonce NA|} \<in> set evs4 |] |
|
63 |
==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom" |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
64 |
|
2110 | 65 |
(*This message models possible leaks of session keys. The Nonces |
2156 | 66 |
identify the protocol run. Quoting Server here ensures they are |
67 |
correct.*) |
|
11251 | 68 |
Oops: "[| evso \<in> yahalom; |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset
|
69 |
Says Server A {|Crypt (shrK A) |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset
|
70 |
{|Agent B, Key K, Nonce NA, Nonce NB|}, |
11251 | 71 |
X|} \<in> set evso |] |
72 |
==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom" |
|
2110 | 73 |
|
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset
|
74 |
|
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset
|
75 |
constdefs |
11251 | 76 |
KeyWithNonce :: "[key, nat, event list] => bool" |
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset
|
77 |
"KeyWithNonce K NB evs == |
11251 | 78 |
\<exists>A B na X. |
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset
|
79 |
Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} |
11251 | 80 |
\<in> set evs" |
81 |
||
82 |
||
83 |
declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
84 |
declare parts.Body [dest] |
|
85 |
declare Fake_parts_insert_in_Un [dest] |
|
86 |
declare analz_into_parts [dest] |
|
87 |
||
88 |
(*A "possibility property": there are traces that reach the end*) |
|
89 |
lemma "A \<noteq> Server |
|
90 |
==> \<exists>X NB K. \<exists>evs \<in> yahalom. |
|
91 |
Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs" |
|
92 |
apply (intro exI bexI) |
|
93 |
apply (rule_tac [2] yahalom.Nil |
|
94 |
[THEN yahalom.YM1, THEN yahalom.Reception, |
|
95 |
THEN yahalom.YM2, THEN yahalom.Reception, |
|
96 |
THEN yahalom.YM3, THEN yahalom.Reception, |
|
13507 | 97 |
THEN yahalom.YM4], possibility) |
11251 | 98 |
done |
99 |
||
100 |
lemma Gets_imp_Says: |
|
101 |
"[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" |
|
102 |
by (erule rev_mp, erule yahalom.induct, auto) |
|
103 |
||
104 |
(*Must be proved separately for each protocol*) |
|
105 |
lemma Gets_imp_knows_Spy: |
|
106 |
"[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs" |
|
107 |
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
|
108 |
||
109 |
declare Gets_imp_knows_Spy [THEN analz.Inj, dest] |
|
110 |
||
111 |
||
112 |
(**** Inductive proofs about yahalom ****) |
|
113 |
||
114 |
(*Lets us treat YM4 using a similar argument as for the Fake case.*) |
|
115 |
lemma YM4_analz_knows_Spy: |
|
116 |
"[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
|
117 |
==> X \<in> analz (knows Spy evs)" |
|
118 |
by blast |
|
119 |
||
120 |
lemmas YM4_parts_knows_Spy = |
|
121 |
YM4_analz_knows_Spy [THEN analz_into_parts, standard] |
|
122 |
||
123 |
(*For Oops*) |
|
124 |
lemma YM4_Key_parts_knows_Spy: |
|
125 |
"Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs |
|
126 |
==> K \<in> parts (knows Spy evs)" |
|
127 |
by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj]) |
|
128 |
||
129 |
||
130 |
(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
|
131 |
sends messages containing X! **) |
|
132 |
||
133 |
(*Spy never sees a good agent's shared key!*) |
|
134 |
lemma Spy_see_shrK [simp]: |
|
135 |
"evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
136 |
apply (erule yahalom.induct, force, |
|
13507 | 137 |
drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) |
11251 | 138 |
done |
139 |
||
140 |
lemma Spy_analz_shrK [simp]: |
|
141 |
"evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
142 |
by auto |
|
143 |
||
144 |
lemma Spy_see_shrK_D [dest!]: |
|
145 |
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" |
|
146 |
by (blast dest: Spy_see_shrK) |
|
147 |
||
148 |
(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) |
|
149 |
lemma new_keys_not_used [rule_format, simp]: |
|
150 |
"evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))" |
|
151 |
apply (erule yahalom.induct, force, |
|
152 |
frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
13926 | 153 |
txt{*Fake*} |
154 |
apply (force dest!: keysFor_parts_insert) |
|
155 |
txt{*YM3, YM4*} |
|
156 |
apply blast+ |
|
11251 | 157 |
done |
158 |
||
159 |
||
160 |
(*Earlier, all protocol proofs declared this theorem. |
|
161 |
But only a few proofs need it, e.g. Yahalom and Kerberos IV.*) |
|
162 |
lemma new_keys_not_analzd: |
|
163 |
"[|evs \<in> yahalom; Key K \<notin> used evs|] ==> K \<notin> keysFor (analz (knows Spy evs))" |
|
164 |
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) |
|
165 |
||
166 |
||
167 |
(*Describes the form of K when the Server sends this message. Useful for |
|
168 |
Oops as well as main secrecy property.*) |
|
169 |
lemma Says_Server_not_range [simp]: |
|
170 |
"[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} |
|
171 |
\<in> set evs; evs \<in> yahalom |] |
|
172 |
==> K \<notin> range shrK" |
|
13507 | 173 |
apply (erule rev_mp, erule yahalom.induct, simp_all, blast) |
11251 | 174 |
done |
175 |
||
176 |
||
177 |
(*For proofs involving analz. |
|
178 |
val analz_knows_Spy_tac = |
|
179 |
ftac YM4_analz_knows_Spy 7 THEN assume_tac 7 |
|
180 |
*) |
|
181 |
||
182 |
(**** |
|
183 |
The following is to prove theorems of the form |
|
184 |
||
185 |
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
|
186 |
Key K \<in> analz (knows Spy evs) |
|
187 |
||
188 |
A more general formula must be proved inductively. |
|
189 |
****) |
|
190 |
||
191 |
(** Session keys are not used to encrypt other session keys **) |
|
192 |
||
193 |
lemma analz_image_freshK [rule_format]: |
|
194 |
"evs \<in> yahalom ==> |
|
195 |
\<forall>K KK. KK <= - (range shrK) --> |
|
196 |
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
197 |
(K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
198 |
apply (erule yahalom.induct, force, |
|
13507 | 199 |
drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz) |
11251 | 200 |
apply (simp only: Says_Server_not_range analz_image_freshK_simps) |
201 |
done |
|
202 |
||
203 |
lemma analz_insert_freshK: |
|
204 |
"[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> |
|
11655 | 205 |
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
11251 | 206 |
(K = KAB | Key K \<in> analz (knows Spy evs))" |
207 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
208 |
||
209 |
||
210 |
(*** The Key K uniquely identifies the Server's message. **) |
|
211 |
||
212 |
lemma unique_session_keys: |
|
213 |
"[| Says Server A |
|
214 |
{|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs; |
|
215 |
Says Server A' |
|
216 |
{|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs; |
|
217 |
evs \<in> yahalom |] |
|
218 |
==> A=A' & B=B' & na=na' & nb=nb'" |
|
219 |
apply (erule rev_mp, erule rev_mp) |
|
220 |
apply (erule yahalom.induct, simp_all) |
|
221 |
(*YM3, by freshness, and YM4*) |
|
222 |
apply blast+ |
|
223 |
done |
|
224 |
||
225 |
||
226 |
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) |
|
227 |
||
228 |
lemma secrecy_lemma: |
|
229 |
"[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
230 |
==> Says Server A |
|
231 |
{|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
232 |
Crypt (shrK B) {|Agent A, Key K|}|} |
|
233 |
\<in> set evs --> |
|
234 |
Notes Spy {|na, nb, Key K|} \<notin> set evs --> |
|
235 |
Key K \<notin> analz (knows Spy evs)" |
|
236 |
apply (erule yahalom.induct, force, |
|
237 |
drule_tac [6] YM4_analz_knows_Spy) |
|
13507 | 238 |
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*) |
11251 | 239 |
apply (blast dest: unique_session_keys)+ (*YM3, Oops*) |
240 |
done |
|
241 |
||
242 |
(*Final version*) |
|
243 |
lemma Spy_not_see_encrypted_key: |
|
244 |
"[| Says Server A |
|
245 |
{|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
246 |
Crypt (shrK B) {|Agent A, Key K|}|} |
|
247 |
\<in> set evs; |
|
248 |
Notes Spy {|na, nb, Key K|} \<notin> set evs; |
|
249 |
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
250 |
==> Key K \<notin> analz (knows Spy evs)" |
|
251 |
by (blast dest: secrecy_lemma) |
|
252 |
||
253 |
||
254 |
(** Security Guarantee for A upon receiving YM3 **) |
|
255 |
||
256 |
(*If the encrypted message appears then it originated with the Server*) |
|
257 |
lemma A_trusts_YM3: |
|
258 |
"[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
|
259 |
A \<notin> bad; evs \<in> yahalom |] |
|
260 |
==> Says Server A |
|
261 |
{|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
262 |
Crypt (shrK B) {|Agent A, Key K|}|} |
|
263 |
\<in> set evs" |
|
264 |
apply (erule rev_mp) |
|
265 |
apply (erule yahalom.induct, force, |
|
266 |
frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
267 |
(*Fake, YM3*) |
|
268 |
apply blast+ |
|
269 |
done |
|
270 |
||
271 |
(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) |
|
272 |
lemma A_gets_good_key: |
|
273 |
"[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
|
274 |
Notes Spy {|na, nb, Key K|} \<notin> set evs; |
|
275 |
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
276 |
==> Key K \<notin> analz (knows Spy evs)" |
|
277 |
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) |
|
278 |
||
279 |
(** Security Guarantees for B upon receiving YM4 **) |
|
280 |
||
281 |
(*B knows, by the first part of A's message, that the Server distributed |
|
282 |
the key for A and B. But this part says nothing about nonces.*) |
|
283 |
lemma B_trusts_YM4_shrK: |
|
284 |
"[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs); |
|
285 |
B \<notin> bad; evs \<in> yahalom |] |
|
286 |
==> \<exists>NA NB. Says Server A |
|
287 |
{|Crypt (shrK A) {|Agent B, Key K, |
|
288 |
Nonce NA, Nonce NB|}, |
|
289 |
Crypt (shrK B) {|Agent A, Key K|}|} |
|
290 |
\<in> set evs" |
|
291 |
apply (erule rev_mp) |
|
292 |
apply (erule yahalom.induct, force, |
|
293 |
frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
294 |
(*Fake, YM3*) |
|
295 |
apply blast+ |
|
296 |
done |
|
297 |
||
298 |
(*B knows, by the second part of A's message, that the Server distributed |
|
299 |
the key quoting nonce NB. This part says nothing about agent names. |
|
300 |
Secrecy of NB is crucial. Note that Nonce NB \<notin> analz(knows Spy evs) must |
|
301 |
be the FIRST antecedent of the induction formula.*) |
|
302 |
lemma B_trusts_YM4_newK[rule_format]: |
|
303 |
"[|Crypt K (Nonce NB) \<in> parts (knows Spy evs); |
|
304 |
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
|
305 |
==> \<exists>A B NA. Says Server A |
|
306 |
{|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
|
307 |
Crypt (shrK B) {|Agent A, Key K|}|} |
|
308 |
\<in> set evs" |
|
309 |
apply (erule rev_mp, erule rev_mp) |
|
310 |
apply (erule yahalom.induct, force, |
|
311 |
frule_tac [6] YM4_parts_knows_Spy) |
|
312 |
apply (analz_mono_contra, simp_all) |
|
313 |
(*Fake, YM3*) |
|
314 |
apply blast |
|
315 |
apply blast |
|
316 |
(*YM4*) |
|
317 |
(*A is uncompromised because NB is secure |
|
318 |
A's certificate guarantees the existence of the Server message*) |
|
319 |
apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
|
320 |
dest: Says_imp_spies |
|
321 |
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) |
|
322 |
done |
|
323 |
||
324 |
||
325 |
(**** Towards proving secrecy of Nonce NB ****) |
|
326 |
||
327 |
(** Lemmas about the predicate KeyWithNonce **) |
|
328 |
||
329 |
lemma KeyWithNonceI: |
|
330 |
"Says Server A |
|
331 |
{|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} |
|
332 |
\<in> set evs ==> KeyWithNonce K NB evs" |
|
333 |
by (unfold KeyWithNonce_def, blast) |
|
334 |
||
335 |
lemma KeyWithNonce_Says [simp]: |
|
336 |
"KeyWithNonce K NB (Says S A X # evs) = |
|
337 |
(Server = S & |
|
338 |
(\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) |
|
339 |
| KeyWithNonce K NB evs)" |
|
340 |
by (simp add: KeyWithNonce_def, blast) |
|
341 |
||
342 |
||
343 |
lemma KeyWithNonce_Notes [simp]: |
|
344 |
"KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs" |
|
345 |
by (simp add: KeyWithNonce_def) |
|
346 |
||
347 |
lemma KeyWithNonce_Gets [simp]: |
|
348 |
"KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs" |
|
349 |
by (simp add: KeyWithNonce_def) |
|
350 |
||
351 |
(*A fresh key cannot be associated with any nonce |
|
352 |
(with respect to a given trace). *) |
|
353 |
lemma fresh_not_KeyWithNonce: |
|
354 |
"Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs" |
|
355 |
by (unfold KeyWithNonce_def, blast) |
|
356 |
||
357 |
(*The Server message associates K with NB' and therefore not with any |
|
358 |
other nonce NB.*) |
|
359 |
lemma Says_Server_KeyWithNonce: |
|
360 |
"[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} |
|
361 |
\<in> set evs; |
|
362 |
NB \<noteq> NB'; evs \<in> yahalom |] |
|
363 |
==> ~ KeyWithNonce K NB evs" |
|
364 |
by (unfold KeyWithNonce_def, blast dest: unique_session_keys) |
|
365 |
||
366 |
||
367 |
(*The only nonces that can be found with the help of session keys are |
|
368 |
those distributed as nonce NB by the Server. The form of the theorem |
|
369 |
recalls analz_image_freshK, but it is much more complicated.*) |
|
370 |
||
371 |
||
372 |
(*As with analz_image_freshK, we take some pains to express the property |
|
373 |
as a logical equivalence so that the simplifier can apply it.*) |
|
374 |
lemma Nonce_secrecy_lemma: |
|
375 |
"P --> (X \<in> analz (G Un H)) --> (X \<in> analz H) ==> |
|
376 |
P --> (X \<in> analz (G Un H)) = (X \<in> analz H)" |
|
377 |
by (blast intro: analz_mono [THEN subsetD]) |
|
378 |
||
379 |
lemma Nonce_secrecy: |
|
380 |
"evs \<in> yahalom ==> |
|
381 |
(\<forall>KK. KK <= - (range shrK) --> |
|
382 |
(\<forall>K \<in> KK. ~ KeyWithNonce K NB evs) --> |
|
383 |
(Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) = |
|
384 |
(Nonce NB \<in> analz (knows Spy evs)))" |
|
385 |
apply (erule yahalom.induct, force, |
|
386 |
frule_tac [6] YM4_analz_knows_Spy) |
|
387 |
apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI]) |
|
388 |
apply (simp_all del: image_insert image_Un |
|
389 |
add: analz_image_freshK_simps split_ifs |
|
390 |
all_conj_distrib ball_conj_distrib |
|
391 |
analz_image_freshK fresh_not_KeyWithNonce |
|
392 |
imp_disj_not1 (*Moves NBa\<noteq>NB to the front*) |
|
393 |
Says_Server_KeyWithNonce) |
|
394 |
(*For Oops, simplification proves NBa\<noteq>NB. By Says_Server_KeyWithNonce, |
|
395 |
we get (~ KeyWithNonce K NB evs); then simplification can apply the |
|
396 |
induction hypothesis with KK = {K}.*) |
|
397 |
(*Fake*) |
|
398 |
apply spy_analz |
|
399 |
(*YM4*) (** LEVEL 6 **) |
|
13507 | 400 |
apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify) |
11251 | 401 |
(*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB. Previous two steps make |
402 |
the next step faster.*) |
|
403 |
apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad |
|
404 |
dest: analz.Inj |
|
405 |
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI]) |
|
406 |
done |
|
407 |
||
408 |
||
409 |
(*Version required below: if NB can be decrypted using a session key then it |
|
410 |
was distributed with that key. The more general form above is required |
|
411 |
for the induction to carry through.*) |
|
412 |
lemma single_Nonce_secrecy: |
|
413 |
"[| Says Server A |
|
414 |
{|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} |
|
415 |
\<in> set evs; |
|
416 |
NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom |] |
|
417 |
==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) = |
|
418 |
(Nonce NB \<in> analz (knows Spy evs))" |
|
419 |
by (simp_all del: image_insert image_Un imp_disjL |
|
420 |
add: analz_image_freshK_simps split_ifs |
|
13507 | 421 |
Nonce_secrecy Says_Server_KeyWithNonce) |
11251 | 422 |
|
423 |
||
424 |
(*** The Nonce NB uniquely identifies B's message. ***) |
|
425 |
||
426 |
lemma unique_NB: |
|
427 |
"[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs); |
|
428 |
Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs); |
|
429 |
evs \<in> yahalom; B \<notin> bad; B' \<notin> bad |] |
|
430 |
==> NA' = NA & A' = A & B' = B" |
|
431 |
apply (erule rev_mp, erule rev_mp) |
|
432 |
apply (erule yahalom.induct, force, |
|
433 |
frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
434 |
(*Fake, and YM2 by freshness*) |
|
435 |
apply blast+ |
|
436 |
done |
|
437 |
||
438 |
||
439 |
(*Variant useful for proving secrecy of NB. Because nb is assumed to be |
|
440 |
secret, we no longer must assume B, B' not bad.*) |
|
441 |
lemma Says_unique_NB: |
|
442 |
"[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} |
|
443 |
\<in> set evs; |
|
444 |
Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} |
|
445 |
\<in> set evs; |
|
446 |
nb \<notin> analz (knows Spy evs); evs \<in> yahalom |] |
|
447 |
==> NA' = NA & A' = A & B' = B" |
|
448 |
by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
|
449 |
dest: Says_imp_spies unique_NB parts.Inj analz.Inj) |
|
450 |
||
451 |
||
452 |
(** A nonce value is never used both as NA and as NB **) |
|
453 |
||
454 |
lemma no_nonce_YM1_YM2: |
|
455 |
"[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \<in> parts(knows Spy evs); |
|
456 |
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
|
457 |
==> Crypt (shrK B) {|Agent A, na, Nonce NB|} \<notin> parts(knows Spy evs)" |
|
458 |
apply (erule rev_mp, erule rev_mp) |
|
459 |
apply (erule yahalom.induct, force, |
|
460 |
frule_tac [6] YM4_parts_knows_Spy) |
|
461 |
apply (analz_mono_contra, simp_all) |
|
462 |
(*Fake, YM2*) |
|
463 |
apply blast+ |
|
464 |
done |
|
465 |
||
466 |
(*The Server sends YM3 only in response to YM2.*) |
|
467 |
lemma Says_Server_imp_YM2: |
|
468 |
"[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \<in> set evs; |
|
469 |
evs \<in> yahalom |] |
|
470 |
==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} |
|
471 |
\<in> set evs" |
|
13507 | 472 |
apply (erule rev_mp, erule yahalom.induct, auto) |
11251 | 473 |
done |
474 |
||
475 |
||
476 |
(*A vital theorem for B, that nonce NB remains secure from the Spy.*) |
|
477 |
lemma Spy_not_see_NB : |
|
478 |
"[| Says B Server |
|
479 |
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
|
480 |
\<in> set evs; |
|
481 |
(\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs); |
|
482 |
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
483 |
==> Nonce NB \<notin> analz (knows Spy evs)" |
|
484 |
apply (erule rev_mp, erule rev_mp) |
|
485 |
apply (erule yahalom.induct, force, |
|
486 |
frule_tac [6] YM4_analz_knows_Spy) |
|
487 |
apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq |
|
488 |
analz_insert_freshK) |
|
489 |
(*Fake*) |
|
490 |
apply spy_analz |
|
491 |
(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) |
|
492 |
apply blast |
|
493 |
(*YM2*) |
|
494 |
apply blast |
|
495 |
(*Prove YM3 by showing that no NB can also be an NA*) |
|
496 |
apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) |
|
497 |
(** LEVEL 7: YM4 and Oops remain **) |
|
498 |
apply (clarify, simp add: all_conj_distrib) |
|
499 |
(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) |
|
500 |
(*Case analysis on Aa:bad; PROOF FAILED problems |
|
501 |
use Says_unique_NB to identify message components: Aa=A, Ba=B*) |
|
502 |
apply (blast dest!: Says_unique_NB |
|
503 |
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] |
|
504 |
dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 |
|
505 |
Spy_not_see_encrypted_key) |
|
506 |
(*Oops case: if the nonce is betrayed now, show that the Oops event is |
|
507 |
covered by the quantified Oops assumption.*) |
|
508 |
apply (clarify, simp add: all_conj_distrib) |
|
509 |
apply (frule Says_Server_imp_YM2, assumption) |
|
510 |
apply (case_tac "NB = NBa") |
|
511 |
(*If NB=NBa then all other components of the Oops message agree*) |
|
512 |
apply (blast dest: Says_unique_NB) |
|
513 |
(*case NB \<noteq> NBa*) |
|
514 |
apply (simp add: single_Nonce_secrecy) |
|
515 |
apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*)) |
|
516 |
done |
|
517 |
||
518 |
||
519 |
(*B's session key guarantee from YM4. The two certificates contribute to a |
|
520 |
single conclusion about the Server's message. Note that the "Notes Spy" |
|
521 |
assumption must quantify over \<forall>POSSIBLE keys instead of our particular K. |
|
522 |
If this run is broken and the spy substitutes a certificate containing an |
|
523 |
old key, B has no means of telling.*) |
|
524 |
lemma B_trusts_YM4: |
|
525 |
"[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
526 |
Crypt K (Nonce NB)|} \<in> set evs; |
|
527 |
Says B Server |
|
528 |
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
|
529 |
\<in> set evs; |
|
530 |
\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs; |
|
531 |
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
532 |
==> Says Server A |
|
533 |
{|Crypt (shrK A) {|Agent B, Key K, |
|
534 |
Nonce NA, Nonce NB|}, |
|
535 |
Crypt (shrK B) {|Agent A, Key K|}|} |
|
536 |
\<in> set evs" |
|
537 |
by (blast dest: Spy_not_see_NB Says_unique_NB |
|
538 |
Says_Server_imp_YM2 B_trusts_YM4_newK) |
|
539 |
||
540 |
||
541 |
||
542 |
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) |
|
543 |
lemma B_gets_good_key: |
|
544 |
"[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
545 |
Crypt K (Nonce NB)|} \<in> set evs; |
|
546 |
Says B Server |
|
547 |
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
|
548 |
\<in> set evs; |
|
549 |
\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs; |
|
550 |
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
551 |
==> Key K \<notin> analz (knows Spy evs)" |
|
552 |
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) |
|
553 |
||
554 |
||
555 |
(*** Authenticating B to A ***) |
|
556 |
||
557 |
(*The encryption in message YM2 tells us it cannot be faked.*) |
|
558 |
lemma B_Said_YM2 [rule_format]: |
|
559 |
"[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs); |
|
560 |
evs \<in> yahalom|] |
|
561 |
==> B \<notin> bad --> |
|
562 |
Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} |
|
563 |
\<in> set evs" |
|
564 |
apply (erule rev_mp, erule yahalom.induct, force, |
|
565 |
frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
566 |
(*Fake*) |
|
567 |
apply blast |
|
568 |
done |
|
569 |
||
570 |
(*If the server sends YM3 then B sent YM2*) |
|
571 |
lemma YM3_auth_B_to_A_lemma: |
|
572 |
"[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} |
|
573 |
\<in> set evs; evs \<in> yahalom|] |
|
574 |
==> B \<notin> bad --> |
|
575 |
Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} |
|
576 |
\<in> set evs" |
|
577 |
apply (erule rev_mp, erule yahalom.induct, simp_all) |
|
578 |
(*YM3, YM4*) |
|
579 |
apply (blast dest!: B_Said_YM2)+ |
|
580 |
done |
|
581 |
||
582 |
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) |
|
583 |
lemma YM3_auth_B_to_A: |
|
584 |
"[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} |
|
585 |
\<in> set evs; |
|
586 |
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
587 |
==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} |
|
588 |
\<in> set evs" |
|
589 |
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs) |
|
590 |
||
591 |
||
592 |
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) |
|
593 |
||
594 |
(*Assuming the session key is secure, if both certificates are present then |
|
595 |
A has said NB. We can't be sure about the rest of A's message, but only |
|
596 |
NB matters for freshness.*) |
|
597 |
lemma A_Said_YM3_lemma [rule_format]: |
|
598 |
"evs \<in> yahalom |
|
599 |
==> Key K \<notin> analz (knows Spy evs) --> |
|
600 |
Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
|
601 |
Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) --> |
|
602 |
B \<notin> bad --> |
|
603 |
(\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)" |
|
604 |
apply (erule yahalom.induct, force, |
|
605 |
frule_tac [6] YM4_parts_knows_Spy) |
|
606 |
apply (analz_mono_contra, simp_all) |
|
607 |
(*Fake*) |
|
608 |
apply blast |
|
609 |
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) |
|
610 |
apply (force dest!: Crypt_imp_keysFor) |
|
611 |
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) |
|
612 |
apply (simp add: ex_disj_distrib) |
|
613 |
(*yes: apply unicity of session keys*) |
|
614 |
apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK |
|
615 |
Crypt_Spy_analz_bad |
|
616 |
dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) |
|
617 |
done |
|
618 |
||
619 |
(*If B receives YM4 then A has used nonce NB (and therefore is alive). |
|
620 |
Moreover, A associates K with NB (thus is talking about the same run). |
|
621 |
Other premises guarantee secrecy of K.*) |
|
622 |
lemma YM4_imp_A_Said_YM3 [rule_format]: |
|
623 |
"[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
624 |
Crypt K (Nonce NB)|} \<in> set evs; |
|
625 |
Says B Server |
|
626 |
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
|
627 |
\<in> set evs; |
|
628 |
(\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs); |
|
629 |
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
630 |
==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs" |
|
631 |
by (blast intro!: A_Said_YM3_lemma |
|
632 |
dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says) |
|
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset
|
633 |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset
|
634 |
end |