4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 Inductive relation "recur" for the Recursive Authentication protocol. |
6 Inductive relation "recur" for the Recursive Authentication protocol. |
7 *) |
7 *) |
8 |
8 |
9 Recur = Shared + |
9 theory Recur = Shared: |
10 |
10 |
11 (*End marker for message bundles*) |
11 (*End marker for message bundles*) |
12 syntax END :: msg |
12 syntax END :: "msg" |
13 translations "END" == "Number 0" |
13 translations "END" == "Number 0" |
14 |
14 |
15 (*Two session keys are distributed to each agent except for the initiator, |
15 (*Two session keys are distributed to each agent except for the initiator, |
16 who receives one. |
16 who receives one. |
17 Perhaps the two session keys could be bundled into a single message. |
17 Perhaps the two session keys could be bundled into a single message. |
18 *) |
18 *) |
19 consts respond :: "event list => (msg*msg*key)set" |
19 consts respond :: "event list => (msg*msg*key)set" |
20 inductive "respond evs" (*Server's response to the nested message*) |
20 inductive "respond evs" (*Server's response to the nested message*) |
21 intrs |
21 intros |
22 One "Key KAB \\<notin> used evs |
22 One: "Key KAB \<notin> used evs |
23 ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, |
23 ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, |
24 {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|}, |
24 {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|}, |
25 KAB) \\<in> respond evs" |
25 KAB) \<in> respond evs" |
26 |
26 |
27 (*The most recent session key is passed up to the caller*) |
27 (*The most recent session key is passed up to the caller*) |
28 Cons "[| (PA, RA, KAB) \\<in> respond evs; |
28 Cons: "[| (PA, RA, KAB) \<in> respond evs; |
29 Key KBC \\<notin> used evs; Key KBC \\<notin> parts {RA}; |
29 Key KBC \<notin> used evs; Key KBC \<notin> parts {RA}; |
30 PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |] |
30 PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |] |
31 ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, |
31 ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, |
32 {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
32 {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
33 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
33 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
34 RA|}, |
34 RA|}, |
35 KBC) |
35 KBC) |
36 \\<in> respond evs" |
36 \<in> respond evs" |
37 |
37 |
38 |
38 |
39 (*Induction over "respond" can be difficult due to the complexity of the |
39 (*Induction over "respond" can be difficult due to the complexity of the |
40 subgoals. Set "responses" captures the general form of certificates. |
40 subgoals. Set "responses" captures the general form of certificates. |
41 *) |
41 *) |
42 consts responses :: event list => msg set |
42 consts responses :: "event list => msg set" |
43 inductive "responses evs" |
43 inductive "responses evs" |
44 intrs |
44 intros |
45 (*Server terminates lists*) |
45 (*Server terminates lists*) |
46 Nil "END \\<in> responses evs" |
46 Nil: "END \<in> responses evs" |
47 |
47 |
48 Cons "[| RA \\<in> responses evs; Key KAB \\<notin> used evs |] |
48 Cons: "[| RA \<in> responses evs; Key KAB \<notin> used evs |] |
49 ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
49 ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
50 RA|} \\<in> responses evs" |
50 RA|} \<in> responses evs" |
51 |
51 |
52 |
52 |
53 consts recur :: event list set |
53 consts recur :: "event list set" |
54 inductive "recur" |
54 inductive "recur" |
55 intrs |
55 intros |
56 (*Initial trace is empty*) |
56 (*Initial trace is empty*) |
57 Nil "[] \\<in> recur" |
57 Nil: "[] \<in> recur" |
58 |
58 |
59 (*The spy MAY say anything he CAN say. Common to |
59 (*The spy MAY say anything he CAN say. Common to |
60 all similar protocols.*) |
60 all similar protocols.*) |
61 Fake "[| evs: recur; X: synth (analz (spies evs)) |] |
61 Fake: "[| evsf \<in> recur; X \<in> synth (analz (knows Spy evsf)) |] |
62 ==> Says Spy B X # evs \\<in> recur" |
62 ==> Says Spy B X # evsf \<in> recur" |
63 |
63 |
64 (*Alice initiates a protocol run. |
64 (*Alice initiates a protocol run. |
65 END is a placeholder to terminate the nesting.*) |
65 END is a placeholder to terminate the nesting.*) |
66 RA1 "[| evs1: recur; Nonce NA \\<notin> used evs1 |] |
66 RA1: "[| evs1: recur; Nonce NA \<notin> used evs1 |] |
67 ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}) |
67 ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}) |
68 # evs1 \\<in> recur" |
68 # evs1 \<in> recur" |
69 |
69 |
70 (*Bob's response to Alice's message. C might be the Server. |
70 (*Bob's response to Alice's message. C might be the Server. |
71 We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because |
71 We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because |
72 it complicates proofs, so B may respond to any message at all!*) |
72 it complicates proofs, so B may respond to any message at all!*) |
73 RA2 "[| evs2: recur; Nonce NB \\<notin> used evs2; |
73 RA2: "[| evs2: recur; Nonce NB \<notin> used evs2; |
74 Says A' B PA \\<in> set evs2 |] |
74 Says A' B PA \<in> set evs2 |] |
75 ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) |
75 ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) |
76 # evs2 \\<in> recur" |
76 # evs2 \<in> recur" |
77 |
77 |
78 (*The Server receives Bob's message and prepares a response.*) |
78 (*The Server receives Bob's message and prepares a response.*) |
79 RA3 "[| evs3: recur; Says B' Server PB \\<in> set evs3; |
79 RA3: "[| evs3: recur; Says B' Server PB \<in> set evs3; |
80 (PB,RB,K) \\<in> respond evs3 |] |
80 (PB,RB,K) \<in> respond evs3 |] |
81 ==> Says Server B RB # evs3 \\<in> recur" |
81 ==> Says Server B RB # evs3 \<in> recur" |
82 |
82 |
83 (*Bob receives the returned message and compares the Nonces with |
83 (*Bob receives the returned message and compares the Nonces with |
84 those in the message he previously sent the Server.*) |
84 those in the message he previously sent the Server.*) |
85 RA4 "[| evs4: recur; |
85 RA4: "[| evs4: recur; |
86 Says B C {|XH, Agent B, Agent C, Nonce NB, |
86 Says B C {|XH, Agent B, Agent C, Nonce NB, |
87 XA, Agent A, Agent B, Nonce NA, P|} \\<in> set evs4; |
87 XA, Agent A, Agent B, Nonce NA, P|} \<in> set evs4; |
88 Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
88 Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
89 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
89 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
90 RA|} \\<in> set evs4 |] |
90 RA|} \<in> set evs4 |] |
91 ==> Says B A RA # evs4 \\<in> recur" |
91 ==> Says B A RA # evs4 \<in> recur" |
92 |
|
93 end |
|
94 |
92 |
95 (*No "oops" message can easily be expressed. Each session key is |
93 (*No "oops" message can easily be expressed. Each session key is |
96 associated--in two separate messages--with two nonces. This is |
94 associated--in two separate messages--with two nonces. This is |
97 one try, but it isn't that useful. Re domino attack, note that |
95 one try, but it isn't that useful. Re domino attack, note that |
98 Recur.ML proves that each session key is secure provided the two |
96 Recur.ML proves that each session key is secure provided the two |
99 peers are, even if there are compromised agents elsewhere in |
97 peers are, even if there are compromised agents elsewhere in |
100 the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts, |
98 the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts, |
101 etc. |
99 etc. |
102 |
100 |
103 Oops "[| evso: recur; Says Server B RB \\<in> set evso; |
101 Oops: "[| evso: recur; Says Server B RB \<in> set evso; |
104 RB \\<in> responses evs'; Key K \\<in> parts {RB} |] |
102 RB \<in> responses evs'; Key K \<in> parts {RB} |] |
105 ==> Notes Spy {|Key K, RB|} # evso \\<in> recur" |
103 ==> Notes Spy {|Key K, RB|} # evso \<in> recur" |
106 *) |
104 *) |
|
105 |
|
106 |
|
107 declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
108 declare parts.Body [dest] |
|
109 declare analz_into_parts [dest] |
|
110 declare Fake_parts_insert_in_Un [dest] |
|
111 |
|
112 |
|
113 (** Possibility properties: traces that reach the end |
|
114 ONE theorem would be more elegant and faster! |
|
115 By induction on a list of agents (no repetitions) |
|
116 **) |
|
117 |
|
118 |
|
119 (*Simplest case: Alice goes directly to the server*) |
|
120 lemma "\<exists>K NA. \<exists>evs \<in> recur. |
|
121 Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, |
|
122 END|} \<in> set evs" |
|
123 apply (intro exI bexI) |
|
124 apply (rule_tac [2] recur.Nil [THEN recur.RA1, |
|
125 THEN recur.RA3 [OF _ _ respond.One]]) |
|
126 apply possibility |
|
127 done |
|
128 |
|
129 |
|
130 (*Case two: Alice, Bob and the server |
|
131 WHY WON'T INSERT LET VARS REMAIN??? |
|
132 lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur. |
|
133 Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, |
|
134 END|} \<in> set evs" |
|
135 apply (insert Nonce_supply2 Key_supply2) |
|
136 apply clarify |
|
137 apply (intro exI bexI) |
|
138 apply (rule_tac [2] recur.Nil [THEN recur.RA1, THEN recur.RA2, |
|
139 THEN recur.RA3 [OF _ _ respond.One]]) |
|
140 apply possibility |
|
141 apply (DEPTH_SOLVE (erule asm_rl less_not_refl2 less_not_refl3)) |
|
142 done |
|
143 *) |
|
144 |
|
145 (*Case three: Alice, Bob, Charlie and the server |
|
146 TOO SLOW to run every time! |
|
147 Goal "\<exists>K. \<exists>NA. \<exists>evs \<in> recur. |
|
148 Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, |
|
149 END|} \<in> set evs" |
|
150 by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); |
|
151 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
|
152 by (REPEAT (resolve_tac [exI,bexI] 1)); |
|
153 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS |
|
154 (respond.One RS respond.Cons RS respond.Cons RSN |
|
155 (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); |
|
156 by basic_possibility_tac; |
|
157 by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 |
|
158 ORELSE |
|
159 eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)); |
|
160 result(); |
|
161 ****) |
|
162 |
|
163 (**** Inductive proofs about recur ****) |
|
164 |
|
165 lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs" |
|
166 by (erule respond.induct, simp_all) |
|
167 |
|
168 lemma Key_in_parts_respond [rule_format]: |
|
169 "[| Key K \<in> parts {RB}; (PB,RB,K') \<in> respond evs |] ==> Key K \<notin> used evs" |
|
170 apply (erule rev_mp, erule respond.induct) |
|
171 apply (auto dest: Key_not_used respond_imp_not_used) |
|
172 done |
|
173 |
|
174 (*Simple inductive reasoning about responses*) |
|
175 lemma respond_imp_responses: |
|
176 "(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs" |
|
177 apply (erule respond.induct) |
|
178 apply (blast intro!: respond_imp_not_used responses.intros)+ |
|
179 done |
|
180 |
|
181 |
|
182 (** For reasoning about the encrypted portion of messages **) |
|
183 |
|
184 lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj] |
|
185 |
|
186 lemma RA4_analz_spies: |
|
187 "Says C' B {|Crypt K X, X', RA|} \<in> set evs ==> RA \<in> analz (spies evs)" |
|
188 by blast |
|
189 |
|
190 |
|
191 (*RA2_analz... and RA4_analz... let us treat those cases using the same |
|
192 argument as for the Fake case. This is possible for most, but not all, |
|
193 proofs: Fake does not invent new nonces (as in RA2), and of course Fake |
|
194 messages originate from the Spy. *) |
|
195 |
|
196 lemmas RA2_parts_spies = RA2_analz_spies [THEN analz_into_parts] |
|
197 lemmas RA4_parts_spies = RA4_analz_spies [THEN analz_into_parts] |
|
198 |
|
199 |
|
200 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY |
|
201 sends messages containing X! **) |
|
202 |
|
203 (** Spy never sees another agent's shared key! (unless it's bad at start) **) |
|
204 |
|
205 lemma Spy_see_shrK [simp]: |
|
206 "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" |
|
207 apply (erule recur.induct) |
|
208 apply auto |
|
209 (*RA3. It's ugly to call auto twice, but it seems necessary.*) |
|
210 apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies) |
|
211 done |
|
212 |
|
213 lemma Spy_analz_shrK [simp]: |
|
214 "evs \<in> recur ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" |
|
215 by auto |
|
216 |
|
217 lemma Spy_see_shrK_D [dest!]: |
|
218 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> recur|] ==> A \<in> bad" |
|
219 by (blast dest: Spy_see_shrK) |
|
220 |
|
221 |
|
222 (*** Proofs involving analz ***) |
|
223 |
|
224 (** Session keys are not used to encrypt other session keys **) |
|
225 |
|
226 (*Version for "responses" relation. Handles case RA3 in the theorem below. |
|
227 Note that it holds for *any* set H (not just "spies evs") |
|
228 satisfying the inductive hypothesis.*) |
|
229 lemma resp_analz_image_freshK_lemma: |
|
230 "[| RB \<in> responses evs; |
|
231 \<forall>K KK. KK \<subseteq> - (range shrK) --> |
|
232 (Key K \<in> analz (Key`KK Un H)) = |
|
233 (K \<in> KK | Key K \<in> analz H) |] |
|
234 ==> \<forall>K KK. KK \<subseteq> - (range shrK) --> |
|
235 (Key K \<in> analz (insert RB (Key`KK Un H))) = |
|
236 (K \<in> KK | Key K \<in> analz (insert RB H))" |
|
237 by (erule responses.induct, |
|
238 simp_all del: image_insert |
|
239 add: analz_image_freshK_simps) |
|
240 |
|
241 |
|
242 (*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) |
|
243 lemma raw_analz_image_freshK: |
|
244 "evs \<in> recur ==> |
|
245 \<forall>K KK. KK \<subseteq> - (range shrK) --> |
|
246 (Key K \<in> analz (Key`KK Un (spies evs))) = |
|
247 (K \<in> KK | Key K \<in> analz (spies evs))" |
|
248 apply (erule recur.induct) |
|
249 apply (drule_tac [4] RA2_analz_spies, |
|
250 frule_tac [5] respond_imp_responses, |
|
251 drule_tac [6] RA4_analz_spies) |
|
252 apply analz_freshK |
|
253 apply spy_analz |
|
254 (*RA3*) |
|
255 apply (simp_all add: resp_analz_image_freshK_lemma) |
|
256 done |
|
257 |
|
258 |
|
259 (*Instance of the lemma with H replaced by (spies evs): |
|
260 [| RB \<in> responses evs; evs \<in> recur; |] |
|
261 ==> KK \<subseteq> - (range shrK) --> |
|
262 Key K \<in> analz (insert RB (Key`KK Un spies evs)) = |
|
263 (K \<in> KK | Key K \<in> analz (insert RB (spies evs))) |
|
264 *) |
|
265 lemmas resp_analz_image_freshK = |
|
266 resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK] |
|
267 |
|
268 lemma analz_insert_freshK: |
|
269 "[| evs \<in> recur; KAB \<notin> range shrK |] |
|
270 ==> Key K \<in> analz (insert (Key KAB) (spies evs)) = |
|
271 (K = KAB | Key K \<in> analz (spies evs))" |
|
272 by (simp del: image_insert |
|
273 add: analz_image_freshK_simps raw_analz_image_freshK) |
|
274 |
|
275 |
|
276 (*Everything that's hashed is already in past traffic. *) |
|
277 lemma Hash_imp_body: "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs); |
|
278 evs \<in> recur; A \<notin> bad |] ==> X \<in> parts (spies evs)" |
|
279 apply (erule rev_mp) |
|
280 apply (erule recur.induct, |
|
281 frule_tac [6] RA4_parts_spies, |
|
282 frule_tac [5] respond_imp_responses, |
|
283 frule_tac [4] RA2_parts_spies) |
|
284 (*RA3 requires a further induction*) |
|
285 apply (erule_tac [5] responses.induct) |
|
286 apply simp_all |
|
287 (*Nil*) |
|
288 apply force |
|
289 (*Fake*) |
|
290 apply (blast intro: parts_insertI) |
|
291 done |
|
292 |
|
293 |
|
294 (** The Nonce NA uniquely identifies A's message. |
|
295 This theorem applies to steps RA1 and RA2! |
|
296 |
|
297 Unicity is not used in other proofs but is desirable in its own right. |
|
298 **) |
|
299 |
|
300 lemma unique_NA: |
|
301 "[| Hash {|Key(shrK A), Agent A, B, NA, P|} \<in> parts (spies evs); |
|
302 Hash {|Key(shrK A), Agent A, B',NA, P'|} \<in> parts (spies evs); |
|
303 evs \<in> recur; A \<notin> bad |] |
|
304 ==> B=B' & P=P'" |
|
305 apply (erule rev_mp, erule rev_mp) |
|
306 apply (erule recur.induct, |
|
307 frule_tac [5] respond_imp_responses) |
|
308 apply (force, simp_all) |
|
309 (*Fake*) |
|
310 apply blast |
|
311 apply (erule_tac [3] responses.induct) |
|
312 (*RA1,2: creation of new Nonce*) |
|
313 apply simp_all |
|
314 apply (blast dest!: Hash_imp_body)+ |
|
315 done |
|
316 |
|
317 |
|
318 (*** Lemmas concerning the Server's response |
|
319 (relations "respond" and "responses") |
|
320 ***) |
|
321 |
|
322 lemma shrK_in_analz_respond [simp]: |
|
323 "[| RB \<in> responses evs; evs \<in> recur |] |
|
324 ==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B:bad)" |
|
325 by (erule responses.induct, |
|
326 simp_all del: image_insert |
|
327 add: analz_image_freshK_simps resp_analz_image_freshK) |
|
328 |
|
329 |
|
330 lemma resp_analz_insert_lemma: |
|
331 "[| Key K \<in> analz (insert RB H); |
|
332 \<forall>K KK. KK \<subseteq> - (range shrK) --> |
|
333 (Key K \<in> analz (Key`KK Un H)) = |
|
334 (K \<in> KK | Key K \<in> analz H); |
|
335 RB \<in> responses evs |] |
|
336 ==> (Key K \<in> parts{RB} | Key K \<in> analz H)" |
|
337 apply (erule rev_mp, erule responses.induct) |
|
338 apply (simp_all del: image_insert |
|
339 add: analz_image_freshK_simps resp_analz_image_freshK_lemma) |
|
340 (*Simplification using two distinct treatments of "image"*) |
|
341 apply (simp add: parts_insert2) |
|
342 apply blast |
|
343 done |
|
344 |
|
345 lemmas resp_analz_insert = |
|
346 resp_analz_insert_lemma [OF _ raw_analz_image_freshK] |
|
347 |
|
348 (*The last key returned by respond indeed appears in a certificate*) |
|
349 lemma respond_certificate: |
|
350 "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs |
|
351 ==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}" |
|
352 apply (ind_cases "(X, RA, K) \<in> respond evs") |
|
353 apply simp_all |
|
354 done |
|
355 |
|
356 (*This unicity proof differs from all the others in the HOL/Auth directory. |
|
357 The conclusion isn't quite unicity but duplicity, in that there are two |
|
358 possibilities. Also, the presence of two different matching messages in |
|
359 the inductive step complicates the case analysis. Unusually for such proofs, |
|
360 the quantifiers appear to be necessary.*) |
|
361 lemma unique_lemma [rule_format]: |
|
362 "(PB,RB,KXY) \<in> respond evs ==> |
|
363 \<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB} --> |
|
364 (\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB} --> |
|
365 (A'=A & B'=B) | (A'=B & B'=A))" |
|
366 apply (erule respond.induct) |
|
367 apply (simp_all add: all_conj_distrib) |
|
368 apply (blast dest: respond_certificate) |
|
369 done |
|
370 |
|
371 lemma unique_session_keys: |
|
372 "[| Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB}; |
|
373 Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB}; |
|
374 (PB,RB,KXY) \<in> respond evs |] |
|
375 ==> (A'=A & B'=B) | (A'=B & B'=A)" |
|
376 by (rule unique_lemma, auto) |
|
377 |
|
378 |
|
379 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3 |
|
380 Does not in itself guarantee security: an attack could violate |
|
381 the premises, e.g. by having A=Spy **) |
|
382 |
|
383 lemma respond_Spy_not_see_session_key [rule_format]: |
|
384 "[| (PB,RB,KAB) \<in> respond evs; evs \<in> recur |] |
|
385 ==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad --> |
|
386 Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts{RB} --> |
|
387 Key K \<notin> analz (insert RB (spies evs))" |
|
388 apply (erule respond.induct) |
|
389 apply (frule_tac [2] respond_imp_responses) |
|
390 apply (frule_tac [2] respond_imp_not_used) |
|
391 apply (simp_all del: image_insert |
|
392 add: analz_image_freshK_simps split_ifs shrK_in_analz_respond |
|
393 resp_analz_image_freshK parts_insert2) |
|
394 apply (simp_all add: ex_disj_distrib) |
|
395 (** LEVEL 5 **) |
|
396 (*Base case of respond*) |
|
397 apply blast |
|
398 (*Inductive step of respond*) |
|
399 apply (intro allI conjI impI) |
|
400 apply simp_all |
|
401 (*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*) |
|
402 apply (blast dest: unique_session_keys [OF _ respond_certificate]) |
|
403 apply (blast dest!: respond_certificate) |
|
404 apply (blast dest!: resp_analz_insert) |
|
405 done |
|
406 |
|
407 |
|
408 (*WHAT'S GOING ON??*) |
|
409 method_setup newbla = {* |
|
410 Method.no_args (Method.METHOD (fn facts => Blast_tac 1)) *} |
|
411 "for debugging spy_analz" |
|
412 |
|
413 lemma Spy_not_see_session_key: |
|
414 "[| Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts (spies evs); |
|
415 A \<notin> bad; A' \<notin> bad; evs \<in> recur |] |
|
416 ==> Key K \<notin> analz (spies evs)" |
|
417 apply (erule rev_mp) |
|
418 apply (erule recur.induct) |
|
419 apply (drule_tac [4] RA2_analz_spies, |
|
420 frule_tac [5] respond_imp_responses, |
|
421 drule_tac [6] RA4_analz_spies, |
|
422 simp_all add: split_ifs analz_insert_eq analz_insert_freshK) |
|
423 (*Base*) |
|
424 apply force |
|
425 (*Fake*) |
|
426 apply (intro allI impI notI conjI iffI) |
|
427 apply Fake_insert_simp |
|
428 apply (blast ); |
|
429 (*???ASK MARKUS WHY METHOD_SETUP DOESN'T WORK. Should be just |
|
430 apply spy_analz |
|
431 *) |
|
432 (*RA2*) |
|
433 apply blast |
|
434 (*RA3 remains*) |
|
435 apply (simp add: parts_insert_spies) |
|
436 (*Now we split into two cases. A single blast could do it, but it would take |
|
437 a CPU minute.*) |
|
438 apply (safe del: impCE) |
|
439 (*RA3, case 1: use lemma previously proved by induction*) |
|
440 apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key]) |
|
441 (*RA3, case 2: K is an old key*) |
|
442 apply (blast dest: resp_analz_insert dest: Key_in_parts_respond) |
|
443 (*RA4*) |
|
444 apply blast |
|
445 done |
|
446 |
|
447 (**** Authenticity properties for Agents ****) |
|
448 |
|
449 (*The response never contains Hashes*) |
|
450 lemma Hash_in_parts_respond: |
|
451 "[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H); |
|
452 (PB,RB,K) \<in> respond evs |] |
|
453 ==> Hash {|Key (shrK B), M|} \<in> parts H" |
|
454 apply (erule rev_mp) |
|
455 apply (erule respond_imp_responses [THEN responses.induct]) |
|
456 apply auto |
|
457 done |
|
458 |
|
459 (*Only RA1 or RA2 can have caused such a part of a message to appear. |
|
460 This result is of no use to B, who cannot verify the Hash. Moreover, |
|
461 it can say nothing about how recent A's message is. It might later be |
|
462 used to prove B's presence to A at the run's conclusion.*) |
|
463 lemma Hash_auth_sender [rule_format]: |
|
464 "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \<in> parts(spies evs); |
|
465 A \<notin> bad; evs \<in> recur |] |
|
466 ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \<in> set evs" |
|
467 apply (unfold HPair_def) |
|
468 apply (erule rev_mp) |
|
469 apply (erule recur.induct, |
|
470 frule_tac [6] RA4_parts_spies, |
|
471 frule_tac [4] RA2_parts_spies, |
|
472 simp_all) |
|
473 (*Nil*) |
|
474 apply force |
|
475 (*Fake, RA3*) |
|
476 apply (blast dest: Hash_in_parts_respond)+; |
|
477 done |
|
478 |
|
479 (** These two results subsume (for all agents) the guarantees proved |
|
480 separately for A and B in the Otway-Rees protocol. |
|
481 **) |
|
482 |
|
483 |
|
484 (*Certificates can only originate with the Server.*) |
|
485 lemma Cert_imp_Server_msg: |
|
486 "[| Crypt (shrK A) Y \<in> parts (spies evs); |
|
487 A \<notin> bad; evs \<in> recur |] |
|
488 ==> \<exists>C RC. Says Server C RC \<in> set evs & |
|
489 Crypt (shrK A) Y \<in> parts {RC}" |
|
490 apply (erule rev_mp, erule recur.induct, simp_all) |
|
491 (*Nil*) |
|
492 apply force |
|
493 (*Fake*) |
|
494 apply blast |
|
495 (*RA1*) |
|
496 apply blast |
|
497 (*RA2: it cannot be a new Nonce, contradiction.*) |
|
498 apply blast |
|
499 (*RA3*) |
|
500 apply (simp add: parts_insert_spies, blast) |
|
501 (*RA4*) |
|
502 apply blast |
|
503 done |
|
504 |
|
505 end |