|
1 (* Title: HOL/Auth/CertifiedEmail |
|
2 ID: $Id$ |
|
3 Author: Giampaolo Bella, Christiano Longo and Lawrence C Paulson |
|
4 |
|
5 The certified electronic mail protocol by Abadi et al. |
|
6 *) |
|
7 |
|
8 theory CertifiedEmail = Public: |
|
9 |
|
10 syntax |
|
11 TTP :: agent |
|
12 RPwd :: "agent => key" |
|
13 TTPDecKey :: key |
|
14 TTPEncKey :: key |
|
15 TTPSigKey :: key |
|
16 TTPVerKey :: key |
|
17 |
|
18 translations |
|
19 "TTP" == "Server" |
|
20 "RPwd" == "shrK" |
|
21 "TTPDecKey" == "priEK Server" |
|
22 "TTPEncKey" == "pubEK Server" |
|
23 "TTPSigKey" == "priSK Server" |
|
24 "TTPVerKey" == "pubSK Server" |
|
25 |
|
26 |
|
27 (*FIXME: the four options should be represented by pairs of 0 or 1. |
|
28 Right now only BothAuth is modelled.*) |
|
29 consts |
|
30 NoAuth :: nat |
|
31 TTPAuth :: nat |
|
32 SAuth :: nat |
|
33 BothAuth :: nat |
|
34 |
|
35 text{*We formalize a fixed way of computing responses. Could be better.*} |
|
36 constdefs |
|
37 "response" :: "agent => agent => nat => msg" |
|
38 "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}" |
|
39 |
|
40 |
|
41 consts certified_mail :: "event list set" |
|
42 inductive "certified_mail" |
|
43 intros |
|
44 |
|
45 Nil: --{*The empty trace*} |
|
46 "[] \<in> certified_mail" |
|
47 |
|
48 Fake: --{*The Spy may say anything he can say. The sender field is correct, |
|
49 but agents don't use that information.*} |
|
50 "[| evsf \<in> certified_mail; X \<in> synth(analz(knows Spy evsf))|] |
|
51 ==> Says Spy B X #evsf \<in> certified_mail" |
|
52 |
|
53 FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent |
|
54 equipped with the necessary credentials to serve as an SSL server.*} |
|
55 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(knows Spy evsfssl))|] |
|
56 ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail" |
|
57 |
|
58 CM1: --{*The sender approaches the recipient. The message is a number.*} |
|
59 "[|evs1 \<in> certified_mail; |
|
60 Key K \<notin> used evs1; |
|
61 K \<in> symKeys; |
|
62 Nonce q \<notin> used evs1; |
|
63 hs = Hash {|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|}; |
|
64 S2TTP = Crypt TTPEncKey {|Agent S, Number BothAuth, Key K, Agent R, hs|}|] |
|
65 ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, |
|
66 Number cleartext, Nonce q, S2TTP|} # evs1 |
|
67 \<in> certified_mail" |
|
68 |
|
69 CM2: --{*The recipient records @{term S2TTP'} while transmitting it and her |
|
70 password to @{term TTP} over an SSL channel.*} |
|
71 "[|evs2 \<in> certified_mail; |
|
72 Gets R {|Agent S, Agent TTP, em', Number BothAuth, Number cleartext', |
|
73 Nonce q', S2TTP'|} \<in> set evs2; |
|
74 TTP \<noteq> R; |
|
75 hr = Hash {|Number cleartext', Nonce q', response S R q', em'|} |] |
|
76 ==> |
|
77 Notes TTP {|Agent R, Agent TTP, S2TTP', Key(RPwd R), hr|} # evs2 |
|
78 \<in> certified_mail" |
|
79 |
|
80 CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives |
|
81 a receipt to the sender. The SSL channel does not authenticate |
|
82 the client (@{term R'}), but @{term TTP} accepts the message only |
|
83 if the given password is that of the claimed sender, @{term R'}. |
|
84 He replies over the established SSL channel.*} |
|
85 "[|evs3 \<in> certified_mail; |
|
86 Notes TTP {|Agent R', Agent TTP, S2TTP'', Key(RPwd R'), hr'|} \<in> set evs3; |
|
87 S2TTP'' = Crypt TTPEncKey |
|
88 {|Agent S, Number BothAuth, Key k', Agent R', hs'|}; |
|
89 TTP \<noteq> R'; hs' = hr'; k' \<in> symKeys|] |
|
90 ==> |
|
91 Notes R' {|Agent TTP, Agent R', Key k', hr'|} # |
|
92 Says TTP S (Crypt TTPSigKey S2TTP'') # evs3 \<in> certified_mail" |
|
93 |
|
94 Reception: |
|
95 "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|] |
|
96 ==> Gets B X#evsr \<in> certified_mail" |
|
97 |
|
98 |
|
99 axioms |
|
100 (*Unlike the corresponding property of nonces, this cannot be proved. |
|
101 We have infinitely many agents and there is nothing to stop their |
|
102 long-term keys from exhausting all the natural numbers. The axiom |
|
103 assumes that their keys are dispersed so as to leave room for infinitely |
|
104 many fresh session keys. We could, alternatively, restrict agents to |
|
105 an unspecified finite number. TOO STRONG. REPLACE "used evs" BY |
|
106 used []*) |
|
107 Key_supply_ax: "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs" |
|
108 |
|
109 |
|
110 lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs" |
|
111 by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast) |
|
112 |
|
113 (*A "possibility property": there are traces that reach the end*) |
|
114 lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail. |
|
115 Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs" |
|
116 apply (rule bexE [OF Key_supply1]) |
|
117 apply (intro exI bexI) |
|
118 apply (rule_tac [2] certified_mail.Nil |
|
119 [THEN certified_mail.CM1, THEN certified_mail.Reception, |
|
120 THEN certified_mail.CM2, |
|
121 THEN certified_mail.CM3], possibility, possibility) |
|
122 apply auto |
|
123 done |
|
124 |
|
125 |
|
126 lemma Gets_imp_Says: |
|
127 "[| Gets B X \<in> set evs; evs \<in> certified_mail |] ==> \<exists>A. Says A B X \<in> set evs" |
|
128 apply (erule rev_mp) |
|
129 apply (erule certified_mail.induct, auto) |
|
130 done |
|
131 |
|
132 |
|
133 lemma Gets_imp_parts_knows_Spy: |
|
134 "[|Gets A X \<in> set evs; evs \<in> certified_mail|] ==> X \<in> parts(spies evs)" |
|
135 apply (drule Gets_imp_Says, simp) |
|
136 apply (blast dest: Says_imp_knows_Spy parts.Inj) |
|
137 done |
|
138 |
|
139 lemma CM2_S2TTP_analz_knows_Spy: |
|
140 "[|Gets R {|Agent A, Agent B, em, Number AO, Number cleartext, |
|
141 Nonce q, S2TTP|} \<in> set evs; |
|
142 evs \<in> certified_mail|] |
|
143 ==> S2TTP \<in> analz(knows Spy evs)" |
|
144 apply (drule Gets_imp_Says, simp) |
|
145 apply (blast dest: Says_imp_knows_Spy analz.Inj) |
|
146 done |
|
147 |
|
148 lemmas CM2_S2TTP_parts_knows_Spy = |
|
149 CM2_S2TTP_analz_knows_Spy [THEN analz_subset_parts [THEN subsetD]] |
|
150 |
|
151 lemma hr_form_lemma [rule_format]: |
|
152 "evs \<in> certified_mail |
|
153 ==> hr \<notin> synth (analz (knows Spy evs)) --> |
|
154 (\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} |
|
155 \<in> set evs --> |
|
156 (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|}))" |
|
157 apply (erule certified_mail.induct) |
|
158 apply (synth_analz_mono_contra, simp_all, blast+) |
|
159 done |
|
160 |
|
161 text{*Cannot strengthen the first disjunct to @{term "R\<noteq>Spy"} because |
|
162 the fakessl rule allows Spy to spoof the sender's name. Maybe can |
|
163 strengthen the second disjunct with @{term "R\<noteq>Spy"}.*} |
|
164 lemma hr_form: |
|
165 "[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs; |
|
166 evs \<in> certified_mail|] |
|
167 ==> hr \<in> synth (analz (knows Spy evs)) | |
|
168 (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})" |
|
169 by (blast intro: hr_form_lemma) |
|
170 |
|
171 lemma Spy_dont_know_private_keys [rule_format]: |
|
172 "evs \<in> certified_mail |
|
173 ==> Key (privateKey b A) \<in> parts (spies evs) --> A \<in> bad" |
|
174 apply (erule certified_mail.induct, simp_all) |
|
175 txt{*Fake*} |
|
176 apply (blast dest: Fake_parts_insert[THEN subsetD] |
|
177 analz_subset_parts[THEN subsetD]) |
|
178 txt{*Message 1*} |
|
179 apply blast |
|
180 txt{*Message 3*} |
|
181 apply (frule_tac hr_form, assumption) |
|
182 apply (elim disjE exE) |
|
183 apply (simp_all add: parts_insert2) |
|
184 apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD] |
|
185 analz_subset_parts[THEN subsetD], blast) |
|
186 done |
|
187 |
|
188 lemma Spy_know_private_keys_iff [simp]: |
|
189 "evs \<in> certified_mail |
|
190 ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)" |
|
191 by (blast intro: Spy_dont_know_private_keys parts.Inj) |
|
192 |
|
193 |
|
194 lemma CM3_k_parts_knows_Spy: |
|
195 "[| evs \<in> certified_mail; |
|
196 Notes TTP {|Agent A, Agent TTP, |
|
197 Crypt TTPEncKey {|Agent S, Number AO, Key K, |
|
198 Agent R, hs|}, Key (RPwd R), hs|} \<in> set evs|] |
|
199 ==> Key K \<in> parts(spies evs)" |
|
200 apply (rotate_tac 1) |
|
201 apply (erule rev_mp) |
|
202 apply (erule certified_mail.induct, simp_all) |
|
203 apply (blast intro:parts_insertI) |
|
204 txt{*Fake SSL*} |
|
205 apply (blast dest: analz_subset_parts[THEN subsetD] parts.Body) |
|
206 txt{*Message 2*} |
|
207 apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] Gets_imp_Says |
|
208 elim!: knows_Spy_partsEs) |
|
209 txt{*Message 3*} |
|
210 apply (frule_tac hr_form, assumption) |
|
211 apply (elim disjE exE) |
|
212 apply (simp_all add: parts_insert2) |
|
213 apply (blast intro: subsetD [OF parts_mono [OF Set.subset_insertI]]) |
|
214 done |
|
215 |
|
216 lemma Spy_dont_know_RPwd [rule_format]: |
|
217 "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad" |
|
218 apply (erule certified_mail.induct, simp_all) |
|
219 txt{*Fake*} |
|
220 apply (blast dest: Fake_parts_insert[THEN subsetD] |
|
221 analz_subset_parts[THEN subsetD]) |
|
222 txt{*Message 1*} |
|
223 apply blast |
|
224 txt{*Message 3*} |
|
225 apply (frule CM3_k_parts_knows_Spy, assumption) |
|
226 apply (frule_tac hr_form, assumption) |
|
227 apply (elim disjE exE) |
|
228 apply (simp_all add: parts_insert2) |
|
229 apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD] |
|
230 analz_subset_parts[THEN subsetD]) |
|
231 done |
|
232 |
|
233 |
|
234 lemma Spy_know_RPwd_iff [simp]: |
|
235 "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(knows Spy evs)) = (A\<in>bad)" |
|
236 by (auto simp add: Spy_dont_know_RPwd) |
|
237 |
|
238 lemma Spy_analz_RPwd_iff [simp]: |
|
239 "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(knows Spy evs)) = (A\<in>bad)" |
|
240 by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts[THEN subsetD]]) |
|
241 |
|
242 |
|
243 text{*Unused, but a guarantee of sorts*} |
|
244 theorem CertAutenticity: |
|
245 "[|Crypt TTPSigKey X \<in> parts (spies evs); evs \<in> certified_mail|] |
|
246 ==> \<exists>A. Says TTP A (Crypt TTPSigKey X) \<in> set evs" |
|
247 apply (erule rev_mp) |
|
248 apply (erule certified_mail.induct, simp_all) |
|
249 txt{*Fake*} |
|
250 apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert[THEN subsetD] |
|
251 analz_subset_parts[THEN subsetD]) |
|
252 txt{*Message 1*} |
|
253 apply blast |
|
254 txt{*Message 3*} |
|
255 apply (frule_tac hr_form, assumption) |
|
256 apply (elim disjE exE) |
|
257 apply (simp_all add: parts_insert2) |
|
258 apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD] |
|
259 analz_subset_parts[THEN subsetD], blast) |
|
260 done |
|
261 |
|
262 |
|
263 lemma Spy_dont_know_TTPDecKey [simp]: |
|
264 "evs \<in> certified_mail ==> Key TTPDecKey \<notin> parts(knows Spy evs)" |
|
265 by auto |
|
266 |
|
267 lemma Spy_dont_know_TTPDecKey_analz [simp]: |
|
268 "evs \<in> certified_mail ==> Key TTPDecKey \<notin> analz(knows Spy evs)" |
|
269 by (force dest!: analz_subset_parts[THEN subsetD]) |
|
270 |
|
271 |
|
272 lemma Spy_knows_TTPVerKey [simp]: |
|
273 "Key (invKey TTPSigKey) \<in> analz(knows Spy evs)" |
|
274 by simp |
|
275 |
|
276 |
|
277 subsection{*Proving Confidentiality Results*} |
|
278 |
|
279 lemma analz_image_freshK [rule_format]: |
|
280 "evs \<in> certified_mail ==> |
|
281 \<forall>K KK. invKey TTPEncKey \<notin> KK --> |
|
282 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
283 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
284 apply (erule certified_mail.induct) |
|
285 apply (drule_tac [6] A=TTP in symKey_neq_priEK) |
|
286 apply (erule_tac [6] disjE [OF hr_form]) |
|
287 apply (drule_tac [5] CM2_S2TTP_analz_knows_Spy) |
|
288 prefer 9 |
|
289 apply (elim exE) |
|
290 apply (simp_all add: synth_analz_insert_eq |
|
291 subset_trans [OF _ subset_insertI] |
|
292 subset_trans [OF _ Un_upper2] |
|
293 del: image_insert image_Un add: analz_image_freshK_simps) |
|
294 done |
|
295 |
|
296 |
|
297 lemma analz_insert_freshK: |
|
298 "[| evs \<in> certified_mail; KAB \<noteq> invKey TTPEncKey |] ==> |
|
299 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
|
300 (K = KAB | Key K \<in> analz (knows Spy evs))" |
|
301 by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
302 |
|
303 text{*@{term S2TTP} must have originated from a valid sender |
|
304 provided @{term K} is secure. Proof is surprisingly hard.*} |
|
305 |
|
306 lemma Notes_SSL_imp_used: |
|
307 "[|Notes B {|Agent A, Agent B, X|} \<in> set evs|] ==> X \<in> used evs" |
|
308 by (blast dest!: Notes_imp_used) |
|
309 |
|
310 |
|
311 (*The weaker version, replacing "used evs" by "parts (knows Spy evs)", |
|
312 isn't inductive: message 3 case can't be proved *) |
|
313 lemma S2TTP_sender_lemma [rule_format]: |
|
314 "evs \<in> certified_mail ==> |
|
315 Key K \<notin> analz (knows Spy evs) --> |
|
316 (\<forall>AO. Crypt TTPEncKey |
|
317 {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs --> |
|
318 (\<exists>m ctxt q. |
|
319 hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} & |
|
320 Says S R |
|
321 {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
|
322 Number ctxt, Nonce q, |
|
323 Crypt TTPEncKey |
|
324 {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))" |
|
325 apply (erule certified_mail.induct, analz_mono_contra) |
|
326 apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp) |
|
327 apply (simp add: used_Nil Crypt_notin_initState, simp_all) |
|
328 txt{*Fake*} |
|
329 apply (blast dest: Fake_parts_sing[THEN subsetD] |
|
330 dest!: analz_subset_parts[THEN subsetD]) |
|
331 txt{*Fake SSL*} |
|
332 apply (blast dest: Fake_parts_sing[THEN subsetD] |
|
333 dest: analz_subset_parts[THEN subsetD]) |
|
334 txt{*Message 1*} |
|
335 apply clarsimp |
|
336 apply blast |
|
337 txt{*Message 2*} |
|
338 apply (simp add: parts_insert2, clarify) |
|
339 apply (drule parts_cut, assumption, simp) |
|
340 apply (blast dest: parts_knows_Spy_subset_used [THEN subsetD]) |
|
341 txt{*Message 3*} |
|
342 apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts) |
|
343 done |
|
344 |
|
345 lemma S2TTP_sender: |
|
346 "[|Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs; |
|
347 Key K \<notin> analz (knows Spy evs); |
|
348 evs \<in> certified_mail|] |
|
349 ==> \<exists>m ctxt q. |
|
350 hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} & |
|
351 Says S R |
|
352 {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
|
353 Number ctxt, Nonce q, |
|
354 Crypt TTPEncKey |
|
355 {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs" |
|
356 by (blast intro: S2TTP_sender_lemma) |
|
357 |
|
358 |
|
359 text{*Nobody can have used non-existent keys!*} |
|
360 lemma new_keys_not_used [rule_format, simp]: |
|
361 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> certified_mail|] |
|
362 ==> K \<notin> keysFor (parts (spies evs))" |
|
363 apply (erule rev_mp) |
|
364 apply (erule certified_mail.induct, simp_all) |
|
365 txt{*Fake*} |
|
366 apply (force dest!: keysFor_parts_insert) |
|
367 txt{*Message 1*} |
|
368 apply blast |
|
369 txt{*Message 3*} |
|
370 apply (frule CM3_k_parts_knows_Spy, assumption) |
|
371 apply (frule_tac hr_form, assumption) |
|
372 apply (force dest!: keysFor_parts_insert) |
|
373 done |
|
374 |
|
375 |
|
376 text{*Less easy to prove @{term "m'=m"}. Maybe needs a separate unicity |
|
377 theorem fror ciphertexts of the form @{term "Crypt K (Number m)"}, |
|
378 where @{term K} is secure.*} |
|
379 lemma Key_unique_lemma [rule_format]: |
|
380 "evs \<in> certified_mail ==> |
|
381 Key K \<notin> analz (knows Spy evs) --> |
|
382 (\<forall>m cleartext q hs. |
|
383 Says S R |
|
384 {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
|
385 Number cleartext, Nonce q, |
|
386 Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|} |
|
387 \<in> set evs --> |
|
388 (\<forall>m' cleartext' q' hs'. |
|
389 Says S' R' |
|
390 {|Agent S', Agent TTP, Crypt K (Number m'), Number AO', |
|
391 Number cleartext', Nonce q', |
|
392 Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|} |
|
393 \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))" |
|
394 apply (erule certified_mail.induct, analz_mono_contra, simp_all) |
|
395 txt{*Fake*} |
|
396 apply (blast dest!: usedI S2TTP_sender analz_subset_parts[THEN subsetD]) |
|
397 txt{*Message 1*} |
|
398 apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor) |
|
399 done |
|
400 |
|
401 text{*The key determines the sender, recipient and protocol options.*} |
|
402 theorem Key_unique: |
|
403 "[|Says S R |
|
404 {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
|
405 Number cleartext, Nonce q, |
|
406 Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|} |
|
407 \<in> set evs; |
|
408 Says S' R' |
|
409 {|Agent S', Agent TTP, Crypt K (Number m'), Number AO', |
|
410 Number cleartext', Nonce q', |
|
411 Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|} |
|
412 \<in> set evs; |
|
413 Key K \<notin> analz (knows Spy evs); |
|
414 evs \<in> certified_mail|] |
|
415 ==> R' = R & S' = S & AO' = AO & hs' = hs" |
|
416 by (rule Key_unique_lemma, assumption+) |
|
417 |
|
418 text{*If Spy gets the key then @{term R} is bad and also @{term S} at least |
|
419 gets his return receipt (and therefore has no grounds for complaint).*} |
|
420 lemma Spy_see_encrypted_key_imp: |
|
421 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
|
422 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
|
423 Key K \<in> analz(knows Spy evs); |
|
424 S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}; |
|
425 evs \<in> certified_mail; |
|
426 S\<noteq>Spy|] |
|
427 ==> R \<in> bad & Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs" |
|
428 apply (erule rev_mp) |
|
429 apply (erule rev_mp) |
|
430 apply (erule ssubst) |
|
431 apply (erule certified_mail.induct, simp_all) |
|
432 txt{*Fake*} |
|
433 apply spy_analz |
|
434 txt{*Fake SSL*} |
|
435 apply spy_analz |
|
436 txt{*Message 3*} |
|
437 apply (frule_tac hr_form, assumption) |
|
438 apply (elim disjE exE) |
|
439 apply (simp_all add: synth_analz_insert_eq |
|
440 subset_trans [OF _ subset_insertI] |
|
441 subset_trans [OF _ Un_upper2] |
|
442 del: image_insert image_Un add: analz_image_freshK_simps) |
|
443 apply (simp_all add: symKey_neq_priEK analz_insert_freshK) |
|
444 apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique)+ |
|
445 done |
|
446 |
|
447 text{*Confidentially for the symmetric key*} |
|
448 theorem Spy_not_see_encrypted_key: |
|
449 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
|
450 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
|
451 S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}; |
|
452 evs \<in> certified_mail; |
|
453 S\<noteq>Spy; R \<notin> bad|] |
|
454 ==> Key K \<notin> analz(knows Spy evs)" |
|
455 by (blast dest: Spy_see_encrypted_key_imp) |
|
456 |
|
457 |
|
458 subsection{*The Guarantees for Sender and Recipient*} |
|
459 |
|
460 text{*Agent @{term R}, who may be the Spy, doesn't receive the key |
|
461 until @{term S} has access to the return receipt.*} |
|
462 theorem S_guarantee: |
|
463 "[|Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs; |
|
464 Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
|
465 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
|
466 S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}; |
|
467 hs = Hash {|Number cleartext, Nonce q, response S R q, |
|
468 Crypt K (Number m)|}; |
|
469 S\<noteq>Spy; evs \<in> certified_mail|] |
|
470 ==> Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs" |
|
471 apply (erule rev_mp) |
|
472 apply (erule rev_mp) |
|
473 apply (erule ssubst) |
|
474 apply (erule ssubst) |
|
475 apply (erule certified_mail.induct, simp_all) |
|
476 txt{*Message 1*} |
|
477 apply (blast dest: Notes_imp_used) |
|
478 txt{*Message 3*} |
|
479 apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique |
|
480 Spy_see_encrypted_key_imp) |
|
481 done |
|
482 |
|
483 |
|
484 lemma Says_TTP_imp_Notes: |
|
485 "[|Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs; |
|
486 S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, |
|
487 Hash {|Number cleartext, Nonce q, r, em|}|}; |
|
488 evs \<in> certified_mail|] |
|
489 ==> Notes TTP |
|
490 {|Agent R, Agent TTP, S2TTP, Key (RPwd R), |
|
491 Hash {|Number cleartext, Nonce q, r, em|}|} |
|
492 \<in> set evs" |
|
493 apply (erule rev_mp) |
|
494 apply (erule ssubst) |
|
495 apply (erule certified_mail.induct, simp_all) |
|
496 done |
|
497 |
|
498 |
|
499 |
|
500 text{*Recipient's guarantee: if @{term R} sends message 2, and |
|
501 @{term S} gets a delivery certificate, then @{term R} |
|
502 receives the necessary key.*} |
|
503 theorem R_guarantee: |
|
504 "[|Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} \<in> set evs; |
|
505 Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs; |
|
506 S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, |
|
507 Hash {|Number cleartext, Nonce q, r, em|}|}; |
|
508 hr = Hash {|Number cleartext, Nonce q, r, em|}; |
|
509 R\<noteq>Spy; evs \<in> certified_mail|] |
|
510 ==> Notes R {|Agent TTP, Agent R, Key K, hr|} \<in> set evs" |
|
511 apply (erule rev_mp) |
|
512 apply (erule rev_mp) |
|
513 apply (erule ssubst) |
|
514 apply (erule ssubst) |
|
515 apply (erule certified_mail.induct, simp_all) |
|
516 txt{*Message 2*} |
|
517 apply clarify |
|
518 apply (drule Says_TTP_imp_Notes [OF _ refl], assumption) |
|
519 apply simp |
|
520 done |
|
521 |
|
522 end |