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