13922
|
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
|
13926
|
19 |
"TTP" == "Server "
|
|
20 |
"RPwd" == "shrK "
|
13922
|
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'|} #
|
13926
|
92 |
Gets S (Crypt TTPSigKey S2TTP'') #
|
13922
|
93 |
Says TTP S (Crypt TTPSigKey S2TTP'') # evs3 \<in> certified_mail"
|
|
94 |
|
|
95 |
Reception:
|
|
96 |
"[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
|
|
97 |
==> Gets B X#evsr \<in> certified_mail"
|
|
98 |
|
|
99 |
|
|
100 |
(*A "possibility property": there are traces that reach the end*)
|
|
101 |
lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
|
|
102 |
Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
|
|
103 |
apply (rule bexE [OF Key_supply1])
|
|
104 |
apply (intro exI bexI)
|
|
105 |
apply (rule_tac [2] certified_mail.Nil
|
|
106 |
[THEN certified_mail.CM1, THEN certified_mail.Reception,
|
|
107 |
THEN certified_mail.CM2,
|
|
108 |
THEN certified_mail.CM3], possibility, possibility)
|
|
109 |
apply auto
|
|
110 |
done
|
|
111 |
|
|
112 |
|
|
113 |
lemma Gets_imp_Says:
|
|
114 |
"[| Gets B X \<in> set evs; evs \<in> certified_mail |] ==> \<exists>A. Says A B X \<in> set evs"
|
|
115 |
apply (erule rev_mp)
|
|
116 |
apply (erule certified_mail.induct, auto)
|
|
117 |
done
|
|
118 |
|
|
119 |
|
|
120 |
lemma Gets_imp_parts_knows_Spy:
|
|
121 |
"[|Gets A X \<in> set evs; evs \<in> certified_mail|] ==> X \<in> parts(spies evs)"
|
|
122 |
apply (drule Gets_imp_Says, simp)
|
|
123 |
apply (blast dest: Says_imp_knows_Spy parts.Inj)
|
|
124 |
done
|
|
125 |
|
|
126 |
lemma CM2_S2TTP_analz_knows_Spy:
|
|
127 |
"[|Gets R {|Agent A, Agent B, em, Number AO, Number cleartext,
|
|
128 |
Nonce q, S2TTP|} \<in> set evs;
|
|
129 |
evs \<in> certified_mail|]
|
|
130 |
==> S2TTP \<in> analz(knows Spy evs)"
|
|
131 |
apply (drule Gets_imp_Says, simp)
|
|
132 |
apply (blast dest: Says_imp_knows_Spy analz.Inj)
|
|
133 |
done
|
|
134 |
|
|
135 |
lemmas CM2_S2TTP_parts_knows_Spy =
|
|
136 |
CM2_S2TTP_analz_knows_Spy [THEN analz_subset_parts [THEN subsetD]]
|
|
137 |
|
|
138 |
lemma hr_form_lemma [rule_format]:
|
|
139 |
"evs \<in> certified_mail
|
|
140 |
==> hr \<notin> synth (analz (knows Spy evs)) -->
|
|
141 |
(\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|}
|
|
142 |
\<in> set evs -->
|
|
143 |
(\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|}))"
|
|
144 |
apply (erule certified_mail.induct)
|
|
145 |
apply (synth_analz_mono_contra, simp_all, blast+)
|
|
146 |
done
|
|
147 |
|
|
148 |
text{*Cannot strengthen the first disjunct to @{term "R\<noteq>Spy"} because
|
|
149 |
the fakessl rule allows Spy to spoof the sender's name. Maybe can
|
|
150 |
strengthen the second disjunct with @{term "R\<noteq>Spy"}.*}
|
|
151 |
lemma hr_form:
|
|
152 |
"[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs;
|
|
153 |
evs \<in> certified_mail|]
|
|
154 |
==> hr \<in> synth (analz (knows Spy evs)) |
|
|
155 |
(\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})"
|
|
156 |
by (blast intro: hr_form_lemma)
|
|
157 |
|
|
158 |
lemma Spy_dont_know_private_keys [rule_format]:
|
|
159 |
"evs \<in> certified_mail
|
|
160 |
==> Key (privateKey b A) \<in> parts (spies evs) --> A \<in> bad"
|
|
161 |
apply (erule certified_mail.induct, simp_all)
|
|
162 |
txt{*Fake*}
|
|
163 |
apply (blast dest: Fake_parts_insert[THEN subsetD]
|
|
164 |
analz_subset_parts[THEN subsetD])
|
|
165 |
txt{*Message 1*}
|
|
166 |
apply blast
|
|
167 |
txt{*Message 3*}
|
|
168 |
apply (frule_tac hr_form, assumption)
|
|
169 |
apply (elim disjE exE)
|
|
170 |
apply (simp_all add: parts_insert2)
|
|
171 |
apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
|
|
172 |
analz_subset_parts[THEN subsetD], blast)
|
|
173 |
done
|
|
174 |
|
|
175 |
lemma Spy_know_private_keys_iff [simp]:
|
|
176 |
"evs \<in> certified_mail
|
|
177 |
==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
|
|
178 |
by (blast intro: Spy_dont_know_private_keys parts.Inj)
|
|
179 |
|
|
180 |
|
|
181 |
lemma CM3_k_parts_knows_Spy:
|
|
182 |
"[| evs \<in> certified_mail;
|
|
183 |
Notes TTP {|Agent A, Agent TTP,
|
|
184 |
Crypt TTPEncKey {|Agent S, Number AO, Key K,
|
|
185 |
Agent R, hs|}, Key (RPwd R), hs|} \<in> set evs|]
|
|
186 |
==> Key K \<in> parts(spies evs)"
|
|
187 |
apply (rotate_tac 1)
|
|
188 |
apply (erule rev_mp)
|
|
189 |
apply (erule certified_mail.induct, simp_all)
|
|
190 |
apply (blast intro:parts_insertI)
|
|
191 |
txt{*Fake SSL*}
|
|
192 |
apply (blast dest: analz_subset_parts[THEN subsetD] parts.Body)
|
|
193 |
txt{*Message 2*}
|
|
194 |
apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] Gets_imp_Says
|
|
195 |
elim!: knows_Spy_partsEs)
|
|
196 |
txt{*Message 3*}
|
|
197 |
apply (frule_tac hr_form, assumption)
|
|
198 |
apply (elim disjE exE)
|
|
199 |
apply (simp_all add: parts_insert2)
|
|
200 |
apply (blast intro: subsetD [OF parts_mono [OF Set.subset_insertI]])
|
|
201 |
done
|
|
202 |
|
|
203 |
lemma Spy_dont_know_RPwd [rule_format]:
|
|
204 |
"evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
|
|
205 |
apply (erule certified_mail.induct, simp_all)
|
|
206 |
txt{*Fake*}
|
|
207 |
apply (blast dest: Fake_parts_insert[THEN subsetD]
|
|
208 |
analz_subset_parts[THEN subsetD])
|
|
209 |
txt{*Message 1*}
|
|
210 |
apply blast
|
|
211 |
txt{*Message 3*}
|
|
212 |
apply (frule CM3_k_parts_knows_Spy, assumption)
|
|
213 |
apply (frule_tac hr_form, assumption)
|
|
214 |
apply (elim disjE exE)
|
|
215 |
apply (simp_all add: parts_insert2)
|
|
216 |
apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
|
|
217 |
analz_subset_parts[THEN subsetD])
|
|
218 |
done
|
|
219 |
|
|
220 |
|
|
221 |
lemma Spy_know_RPwd_iff [simp]:
|
|
222 |
"evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(knows Spy evs)) = (A\<in>bad)"
|
|
223 |
by (auto simp add: Spy_dont_know_RPwd)
|
|
224 |
|
|
225 |
lemma Spy_analz_RPwd_iff [simp]:
|
|
226 |
"evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(knows Spy evs)) = (A\<in>bad)"
|
|
227 |
by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts[THEN subsetD]])
|
|
228 |
|
|
229 |
|
|
230 |
text{*Unused, but a guarantee of sorts*}
|
|
231 |
theorem CertAutenticity:
|
|
232 |
"[|Crypt TTPSigKey X \<in> parts (spies evs); evs \<in> certified_mail|]
|
|
233 |
==> \<exists>A. Says TTP A (Crypt TTPSigKey X) \<in> set evs"
|
|
234 |
apply (erule rev_mp)
|
|
235 |
apply (erule certified_mail.induct, simp_all)
|
|
236 |
txt{*Fake*}
|
|
237 |
apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert[THEN subsetD]
|
|
238 |
analz_subset_parts[THEN subsetD])
|
|
239 |
txt{*Message 1*}
|
|
240 |
apply blast
|
|
241 |
txt{*Message 3*}
|
|
242 |
apply (frule_tac hr_form, assumption)
|
|
243 |
apply (elim disjE exE)
|
|
244 |
apply (simp_all add: parts_insert2)
|
|
245 |
apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
|
|
246 |
analz_subset_parts[THEN subsetD], blast)
|
|
247 |
done
|
|
248 |
|
|
249 |
|
|
250 |
lemma Spy_dont_know_TTPDecKey [simp]:
|
|
251 |
"evs \<in> certified_mail ==> Key TTPDecKey \<notin> parts(knows Spy evs)"
|
|
252 |
by auto
|
|
253 |
|
|
254 |
lemma Spy_dont_know_TTPDecKey_analz [simp]:
|
|
255 |
"evs \<in> certified_mail ==> Key TTPDecKey \<notin> analz(knows Spy evs)"
|
|
256 |
by (force dest!: analz_subset_parts[THEN subsetD])
|
|
257 |
|
|
258 |
|
|
259 |
lemma Spy_knows_TTPVerKey [simp]:
|
|
260 |
"Key (invKey TTPSigKey) \<in> analz(knows Spy evs)"
|
|
261 |
by simp
|
|
262 |
|
|
263 |
|
|
264 |
subsection{*Proving Confidentiality Results*}
|
|
265 |
|
|
266 |
lemma analz_image_freshK [rule_format]:
|
|
267 |
"evs \<in> certified_mail ==>
|
|
268 |
\<forall>K KK. invKey TTPEncKey \<notin> KK -->
|
|
269 |
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
|
|
270 |
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
|
|
271 |
apply (erule certified_mail.induct)
|
|
272 |
apply (drule_tac [6] A=TTP in symKey_neq_priEK)
|
|
273 |
apply (erule_tac [6] disjE [OF hr_form])
|
|
274 |
apply (drule_tac [5] CM2_S2TTP_analz_knows_Spy)
|
|
275 |
prefer 9
|
|
276 |
apply (elim exE)
|
|
277 |
apply (simp_all add: synth_analz_insert_eq
|
|
278 |
subset_trans [OF _ subset_insertI]
|
|
279 |
subset_trans [OF _ Un_upper2]
|
|
280 |
del: image_insert image_Un add: analz_image_freshK_simps)
|
|
281 |
done
|
|
282 |
|
|
283 |
|
|
284 |
lemma analz_insert_freshK:
|
|
285 |
"[| evs \<in> certified_mail; KAB \<noteq> invKey TTPEncKey |] ==>
|
|
286 |
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
|
|
287 |
(K = KAB | Key K \<in> analz (knows Spy evs))"
|
|
288 |
by (simp only: analz_image_freshK analz_image_freshK_simps)
|
|
289 |
|
|
290 |
text{*@{term S2TTP} must have originated from a valid sender
|
|
291 |
provided @{term K} is secure. Proof is surprisingly hard.*}
|
|
292 |
|
|
293 |
lemma Notes_SSL_imp_used:
|
|
294 |
"[|Notes B {|Agent A, Agent B, X|} \<in> set evs|] ==> X \<in> used evs"
|
|
295 |
by (blast dest!: Notes_imp_used)
|
|
296 |
|
|
297 |
|
|
298 |
(*The weaker version, replacing "used evs" by "parts (knows Spy evs)",
|
|
299 |
isn't inductive: message 3 case can't be proved *)
|
|
300 |
lemma S2TTP_sender_lemma [rule_format]:
|
|
301 |
"evs \<in> certified_mail ==>
|
|
302 |
Key K \<notin> analz (knows Spy evs) -->
|
|
303 |
(\<forall>AO. Crypt TTPEncKey
|
|
304 |
{|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
|
|
305 |
(\<exists>m ctxt q.
|
|
306 |
hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
|
|
307 |
Says S R
|
|
308 |
{|Agent S, Agent TTP, Crypt K (Number m), Number AO,
|
|
309 |
Number ctxt, Nonce q,
|
|
310 |
Crypt TTPEncKey
|
|
311 |
{|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))"
|
|
312 |
apply (erule certified_mail.induct, analz_mono_contra)
|
|
313 |
apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
|
|
314 |
apply (simp add: used_Nil Crypt_notin_initState, simp_all)
|
|
315 |
txt{*Fake*}
|
|
316 |
apply (blast dest: Fake_parts_sing[THEN subsetD]
|
|
317 |
dest!: analz_subset_parts[THEN subsetD])
|
|
318 |
txt{*Fake SSL*}
|
|
319 |
apply (blast dest: Fake_parts_sing[THEN subsetD]
|
|
320 |
dest: analz_subset_parts[THEN subsetD])
|
|
321 |
txt{*Message 1*}
|
|
322 |
apply clarsimp
|
|
323 |
apply blast
|
|
324 |
txt{*Message 2*}
|
|
325 |
apply (simp add: parts_insert2, clarify)
|
|
326 |
apply (drule parts_cut, assumption, simp)
|
|
327 |
apply (blast dest: parts_knows_Spy_subset_used [THEN subsetD])
|
|
328 |
txt{*Message 3*}
|
|
329 |
apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts)
|
|
330 |
done
|
|
331 |
|
|
332 |
lemma S2TTP_sender:
|
|
333 |
"[|Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
|
|
334 |
Key K \<notin> analz (knows Spy evs);
|
|
335 |
evs \<in> certified_mail|]
|
|
336 |
==> \<exists>m ctxt q.
|
|
337 |
hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
|
|
338 |
Says S R
|
|
339 |
{|Agent S, Agent TTP, Crypt K (Number m), Number AO,
|
|
340 |
Number ctxt, Nonce q,
|
|
341 |
Crypt TTPEncKey
|
|
342 |
{|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs"
|
|
343 |
by (blast intro: S2TTP_sender_lemma)
|
|
344 |
|
|
345 |
|
|
346 |
text{*Nobody can have used non-existent keys!*}
|
|
347 |
lemma new_keys_not_used [rule_format, simp]:
|
|
348 |
"[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> certified_mail|]
|
|
349 |
==> K \<notin> keysFor (parts (spies evs))"
|
|
350 |
apply (erule rev_mp)
|
|
351 |
apply (erule certified_mail.induct, simp_all)
|
|
352 |
txt{*Fake*}
|
|
353 |
apply (force dest!: keysFor_parts_insert)
|
|
354 |
txt{*Message 1*}
|
|
355 |
apply blast
|
|
356 |
txt{*Message 3*}
|
|
357 |
apply (frule CM3_k_parts_knows_Spy, assumption)
|
|
358 |
apply (frule_tac hr_form, assumption)
|
|
359 |
apply (force dest!: keysFor_parts_insert)
|
|
360 |
done
|
|
361 |
|
|
362 |
|
|
363 |
text{*Less easy to prove @{term "m'=m"}. Maybe needs a separate unicity
|
13926
|
364 |
theorem for ciphertexts of the form @{term "Crypt K (Number m)"},
|
13922
|
365 |
where @{term K} is secure.*}
|
|
366 |
lemma Key_unique_lemma [rule_format]:
|
|
367 |
"evs \<in> certified_mail ==>
|
|
368 |
Key K \<notin> analz (knows Spy evs) -->
|
|
369 |
(\<forall>m cleartext q hs.
|
|
370 |
Says S R
|
|
371 |
{|Agent S, Agent TTP, Crypt K (Number m), Number AO,
|
|
372 |
Number cleartext, Nonce q,
|
|
373 |
Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|}
|
|
374 |
\<in> set evs -->
|
|
375 |
(\<forall>m' cleartext' q' hs'.
|
|
376 |
Says S' R'
|
|
377 |
{|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
|
|
378 |
Number cleartext', Nonce q',
|
|
379 |
Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|}
|
|
380 |
\<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))"
|
|
381 |
apply (erule certified_mail.induct, analz_mono_contra, simp_all)
|
|
382 |
txt{*Fake*}
|
|
383 |
apply (blast dest!: usedI S2TTP_sender analz_subset_parts[THEN subsetD])
|
|
384 |
txt{*Message 1*}
|
|
385 |
apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
|
|
386 |
done
|
|
387 |
|
|
388 |
text{*The key determines the sender, recipient and protocol options.*}
|
13926
|
389 |
lemma Key_unique:
|
13922
|
390 |
"[|Says S R
|
|
391 |
{|Agent S, Agent TTP, Crypt K (Number m), Number AO,
|
|
392 |
Number cleartext, Nonce q,
|
|
393 |
Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|}
|
|
394 |
\<in> set evs;
|
|
395 |
Says S' R'
|
|
396 |
{|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
|
|
397 |
Number cleartext', Nonce q',
|
|
398 |
Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|}
|
|
399 |
\<in> set evs;
|
|
400 |
Key K \<notin> analz (knows Spy evs);
|
|
401 |
evs \<in> certified_mail|]
|
|
402 |
==> R' = R & S' = S & AO' = AO & hs' = hs"
|
|
403 |
by (rule Key_unique_lemma, assumption+)
|
|
404 |
|
13926
|
405 |
subsection{*The Guarantees for Sender and Recipient*}
|
|
406 |
|
13922
|
407 |
text{*If Spy gets the key then @{term R} is bad and also @{term S} at least
|
|
408 |
gets his return receipt (and therefore has no grounds for complaint).*}
|
13926
|
409 |
theorem Spy_see_encrypted_key_imp:
|
13922
|
410 |
"[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
|
|
411 |
Number cleartext, Nonce q, S2TTP|} \<in> set evs;
|
|
412 |
Key K \<in> analz(knows Spy evs);
|
|
413 |
S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
|
|
414 |
evs \<in> certified_mail;
|
|
415 |
S\<noteq>Spy|]
|
|
416 |
==> R \<in> bad & Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
|
|
417 |
apply (erule rev_mp)
|
|
418 |
apply (erule rev_mp)
|
|
419 |
apply (erule ssubst)
|
|
420 |
apply (erule certified_mail.induct, simp_all)
|
|
421 |
txt{*Fake*}
|
|
422 |
apply spy_analz
|
|
423 |
txt{*Fake SSL*}
|
|
424 |
apply spy_analz
|
|
425 |
txt{*Message 3*}
|
|
426 |
apply (frule_tac hr_form, assumption)
|
|
427 |
apply (elim disjE exE)
|
|
428 |
apply (simp_all add: synth_analz_insert_eq
|
|
429 |
subset_trans [OF _ subset_insertI]
|
|
430 |
subset_trans [OF _ Un_upper2]
|
|
431 |
del: image_insert image_Un add: analz_image_freshK_simps)
|
|
432 |
apply (simp_all add: symKey_neq_priEK analz_insert_freshK)
|
|
433 |
apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique)+
|
|
434 |
done
|
|
435 |
|
|
436 |
text{*Confidentially for the symmetric key*}
|
|
437 |
theorem Spy_not_see_encrypted_key:
|
|
438 |
"[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
|
|
439 |
Number cleartext, Nonce q, S2TTP|} \<in> set evs;
|
|
440 |
S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
|
|
441 |
evs \<in> certified_mail;
|
|
442 |
S\<noteq>Spy; R \<notin> bad|]
|
|
443 |
==> Key K \<notin> analz(knows Spy evs)"
|
|
444 |
by (blast dest: Spy_see_encrypted_key_imp)
|
|
445 |
|
|
446 |
|
|
447 |
text{*Agent @{term R}, who may be the Spy, doesn't receive the key
|
|
448 |
until @{term S} has access to the return receipt.*}
|
|
449 |
theorem S_guarantee:
|
|
450 |
"[|Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
|
|
451 |
Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
|
|
452 |
Number cleartext, Nonce q, S2TTP|} \<in> set evs;
|
|
453 |
S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
|
|
454 |
hs = Hash {|Number cleartext, Nonce q, response S R q,
|
|
455 |
Crypt K (Number m)|};
|
|
456 |
S\<noteq>Spy; evs \<in> certified_mail|]
|
|
457 |
==> Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
|
|
458 |
apply (erule rev_mp)
|
|
459 |
apply (erule rev_mp)
|
|
460 |
apply (erule ssubst)
|
|
461 |
apply (erule ssubst)
|
|
462 |
apply (erule certified_mail.induct, simp_all)
|
|
463 |
txt{*Message 1*}
|
|
464 |
apply (blast dest: Notes_imp_used)
|
|
465 |
txt{*Message 3*}
|
|
466 |
apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique
|
|
467 |
Spy_see_encrypted_key_imp)
|
|
468 |
done
|
|
469 |
|
|
470 |
|
|
471 |
lemma Says_TTP_imp_Notes:
|
|
472 |
"[|Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs;
|
|
473 |
S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R,
|
|
474 |
Hash {|Number cleartext, Nonce q, r, em|}|};
|
|
475 |
evs \<in> certified_mail|]
|
|
476 |
==> Notes TTP
|
|
477 |
{|Agent R, Agent TTP, S2TTP, Key (RPwd R),
|
|
478 |
Hash {|Number cleartext, Nonce q, r, em|}|}
|
|
479 |
\<in> set evs"
|
|
480 |
apply (erule rev_mp)
|
|
481 |
apply (erule ssubst)
|
|
482 |
apply (erule certified_mail.induct, simp_all)
|
|
483 |
done
|
|
484 |
|
|
485 |
|
|
486 |
|
|
487 |
text{*Recipient's guarantee: if @{term R} sends message 2, and
|
|
488 |
@{term S} gets a delivery certificate, then @{term R}
|
|
489 |
receives the necessary key.*}
|
|
490 |
theorem R_guarantee:
|
|
491 |
"[|Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} \<in> set evs;
|
|
492 |
Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs;
|
|
493 |
S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R,
|
|
494 |
Hash {|Number cleartext, Nonce q, r, em|}|};
|
|
495 |
hr = Hash {|Number cleartext, Nonce q, r, em|};
|
|
496 |
R\<noteq>Spy; evs \<in> certified_mail|]
|
|
497 |
==> Notes R {|Agent TTP, Agent R, Key K, hr|} \<in> set evs"
|
|
498 |
apply (erule rev_mp)
|
|
499 |
apply (erule rev_mp)
|
|
500 |
apply (erule ssubst)
|
|
501 |
apply (erule ssubst)
|
|
502 |
apply (erule certified_mail.induct, simp_all)
|
|
503 |
txt{*Message 2*}
|
|
504 |
apply clarify
|
|
505 |
apply (drule Says_TTP_imp_Notes [OF _ refl], assumption)
|
|
506 |
apply simp
|
|
507 |
done
|
|
508 |
|
|
509 |
end
|