18886
|
1 |
(* ID: $Id$
|
|
2 |
Author: Giampaolo Bella, Catania University
|
|
3 |
*)
|
|
4 |
|
|
5 |
header{*Original Shoup-Rubin protocol*}
|
|
6 |
|
|
7 |
theory ShoupRubin imports Smartcard begin
|
|
8 |
|
|
9 |
consts
|
|
10 |
|
|
11 |
sesK :: "nat*key => key"
|
|
12 |
|
|
13 |
axioms
|
|
14 |
|
|
15 |
(*sesK is injective on each component*)
|
|
16 |
inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
|
|
17 |
|
|
18 |
(*all long-term keys differ from sesK*)
|
|
19 |
shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
|
|
20 |
crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
|
|
21 |
pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)"
|
|
22 |
pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)"
|
|
23 |
|
|
24 |
(*needed for base case in analz_image_freshK*)
|
|
25 |
Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
|
|
26 |
Atomic`(KEY`K) \<union> Atomic`(NONCE`N)"
|
|
27 |
|
|
28 |
(*this protocol makes the assumption of secure means
|
|
29 |
between each agent and his smartcard*)
|
|
30 |
shouprubin_assumes_securemeans [iff]: "evs \<in> sr \<Longrightarrow> secureM"
|
|
31 |
|
|
32 |
constdefs
|
|
33 |
|
|
34 |
Unique :: "[event, event list] => bool" ("Unique _ on _")
|
|
35 |
"Unique ev on evs ==
|
|
36 |
ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
|
|
37 |
|
|
38 |
|
|
39 |
consts sr :: "event list set"
|
|
40 |
inductive "sr"
|
|
41 |
intros
|
|
42 |
|
|
43 |
Nil: "[]\<in> sr"
|
|
44 |
|
|
45 |
|
|
46 |
|
|
47 |
Fake: "\<lbrakk> evsF\<in> sr; X\<in> synth (analz (knows Spy evsF));
|
|
48 |
illegalUse(Card B) \<rbrakk>
|
|
49 |
\<Longrightarrow> Says Spy A X #
|
|
50 |
Inputs Spy (Card B) X # evsF \<in> sr"
|
|
51 |
|
|
52 |
(*In general this rule causes the assumption Card B \<notin> cloned
|
|
53 |
in most guarantees for B - starting with confidentiality -
|
|
54 |
otherwise pairK_confidential could not apply*)
|
|
55 |
Forge:
|
|
56 |
"\<lbrakk> evsFo \<in> sr; Nonce Nb \<in> analz (knows Spy evsFo);
|
|
57 |
Key (pairK(A,B)) \<in> knows Spy evsFo \<rbrakk>
|
|
58 |
\<Longrightarrow> Notes Spy (Key (sesK(Nb,pairK(A,B)))) # evsFo \<in> sr"
|
|
59 |
|
|
60 |
|
|
61 |
|
|
62 |
Reception: "\<lbrakk> evsR\<in> sr; Says A B X \<in> set evsR \<rbrakk>
|
|
63 |
\<Longrightarrow> Gets B X # evsR \<in> sr"
|
|
64 |
|
|
65 |
|
|
66 |
|
|
67 |
(*A AND THE SERVER *)
|
|
68 |
SR1: "\<lbrakk> evs1\<in> sr; A \<noteq> Server\<rbrakk>
|
|
69 |
\<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace>
|
|
70 |
# evs1 \<in> sr"
|
|
71 |
|
|
72 |
SR2: "\<lbrakk> evs2\<in> sr;
|
|
73 |
Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk>
|
|
74 |
\<Longrightarrow> Says Server A \<lbrace>Nonce (Pairkey(A,B)),
|
|
75 |
Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>
|
|
76 |
\<rbrace>
|
|
77 |
# evs2 \<in> sr"
|
|
78 |
|
|
79 |
|
|
80 |
|
|
81 |
|
|
82 |
(*A AND HER CARD*)
|
|
83 |
(*A cannot decrypt the verifier for she dosn't know shrK A,
|
|
84 |
but the pairkey is recognisable*)
|
|
85 |
SR3: "\<lbrakk> evs3\<in> sr; legalUse(Card A);
|
|
86 |
Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3;
|
|
87 |
Gets A \<lbrace>Nonce Pk, Certificate\<rbrace> \<in> set evs3 \<rbrakk>
|
|
88 |
\<Longrightarrow> Inputs A (Card A) (Agent A)
|
|
89 |
# evs3 \<in> sr" (*however A only queries her card
|
|
90 |
if she has previously contacted the server to initiate with some B.
|
|
91 |
Otherwise she would do so even if the Server had not been active.
|
|
92 |
Still, this doesn't and can't mean that the pairkey originated with
|
|
93 |
the server*)
|
|
94 |
|
|
95 |
(*The card outputs the nonce Na to A*)
|
|
96 |
SR4: "\<lbrakk> evs4\<in> sr; A \<noteq> Server;
|
|
97 |
Nonce Na \<notin> used evs4; legalUse(Card A);
|
|
98 |
Inputs A (Card A) (Agent A) \<in> set evs4 \<rbrakk>
|
|
99 |
\<Longrightarrow> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
|
|
100 |
# evs4 \<in> sr"
|
|
101 |
|
|
102 |
(*The card can be exploited by the spy*)
|
|
103 |
(*because of the assumptions on the card, A is certainly not server nor spy*)
|
|
104 |
SR4Fake: "\<lbrakk> evs4F\<in> sr; Nonce Na \<notin> used evs4F;
|
|
105 |
illegalUse(Card A);
|
|
106 |
Inputs Spy (Card A) (Agent A) \<in> set evs4F \<rbrakk>
|
|
107 |
\<Longrightarrow> Outpts (Card A) Spy \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
|
|
108 |
# evs4F \<in> sr"
|
|
109 |
|
|
110 |
|
|
111 |
|
|
112 |
|
|
113 |
(*A TOWARDS B*)
|
|
114 |
SR5: "\<lbrakk> evs5\<in> sr;
|
|
115 |
Outpts (Card A) A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs5;
|
|
116 |
\<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk>
|
|
117 |
\<Longrightarrow> Says A B \<lbrace>Agent A, Nonce Na\<rbrace> # evs5 \<in> sr"
|
|
118 |
(*A must check that the verifier is not a compound message,
|
|
119 |
otherwise this would also fire after SR7 *)
|
|
120 |
|
|
121 |
|
|
122 |
|
|
123 |
|
|
124 |
(*B AND HIS CARD*)
|
|
125 |
SR6: "\<lbrakk> evs6\<in> sr; legalUse(Card B);
|
|
126 |
Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs6 \<rbrakk>
|
|
127 |
\<Longrightarrow> Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace>
|
|
128 |
# evs6 \<in> sr"
|
|
129 |
|
|
130 |
(*B gets back from the card the session key and various verifiers*)
|
|
131 |
SR7: "\<lbrakk> evs7\<in> sr;
|
|
132 |
Nonce Nb \<notin> used evs7; legalUse(Card B); B \<noteq> Server;
|
|
133 |
K = sesK(Nb,pairK(A,B));
|
|
134 |
Key K \<notin> used evs7;
|
|
135 |
Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7\<rbrakk>
|
|
136 |
\<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Key K,
|
|
137 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
138 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
|
|
139 |
# evs7 \<in> sr"
|
|
140 |
|
|
141 |
(*The card can be exploited by the spy*)
|
|
142 |
(*because of the assumptions on the card, A is certainly not server nor spy*)
|
|
143 |
SR7Fake: "\<lbrakk> evs7F\<in> sr; Nonce Nb \<notin> used evs7F;
|
|
144 |
illegalUse(Card B);
|
|
145 |
K = sesK(Nb,pairK(A,B));
|
|
146 |
Key K \<notin> used evs7F;
|
|
147 |
Inputs Spy (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7F \<rbrakk>
|
|
148 |
\<Longrightarrow> Outpts (Card B) Spy \<lbrace>Nonce Nb, Key K,
|
|
149 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
150 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
|
|
151 |
# evs7F \<in> sr"
|
|
152 |
|
|
153 |
|
|
154 |
|
|
155 |
|
|
156 |
(*B TOWARDS A*)
|
|
157 |
(*having sent an input that mentions A is the only memory B relies on,
|
|
158 |
since the output doesn't mention A - lack of explicitness*)
|
|
159 |
SR8: "\<lbrakk> evs8\<in> sr;
|
|
160 |
Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs8;
|
|
161 |
Outpts (Card B) B \<lbrace>Nonce Nb, Key K,
|
|
162 |
Cert1, Cert2\<rbrace> \<in> set evs8 \<rbrakk>
|
|
163 |
\<Longrightarrow> Says B A \<lbrace>Nonce Nb, Cert1\<rbrace> # evs8 \<in> sr"
|
|
164 |
|
|
165 |
|
|
166 |
|
|
167 |
|
|
168 |
(*A AND HER CARD*)
|
|
169 |
(*A cannot check the form of the verifiers - although I can prove the form of
|
|
170 |
Cert2 - and just feeds her card with what she's got*)
|
|
171 |
SR9: "\<lbrakk> evs9\<in> sr; legalUse(Card A);
|
|
172 |
Gets A \<lbrace>Nonce Pk, Cert1\<rbrace> \<in> set evs9;
|
|
173 |
Outpts (Card A) A \<lbrace>Nonce Na, Cert2\<rbrace> \<in> set evs9;
|
|
174 |
Gets A \<lbrace>Nonce Nb, Cert3\<rbrace> \<in> set evs9;
|
|
175 |
\<forall> p q. Cert2 \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk>
|
|
176 |
\<Longrightarrow> Inputs A (Card A)
|
|
177 |
\<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
|
|
178 |
Cert1, Cert3, Cert2\<rbrace>
|
|
179 |
# evs9 \<in> sr"
|
|
180 |
|
|
181 |
(*But the card will only give outputs to the inputs of the correct form*)
|
|
182 |
SR10: "\<lbrakk> evs10\<in> sr; legalUse(Card A); A \<noteq> Server;
|
|
183 |
K = sesK(Nb,pairK(A,B));
|
|
184 |
Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb,
|
|
185 |
Nonce (Pairkey(A,B)),
|
|
186 |
Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)),
|
|
187 |
Agent B\<rbrace>,
|
|
188 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
189 |
Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
|
|
190 |
\<in> set evs10 \<rbrakk>
|
|
191 |
\<Longrightarrow> Outpts (Card A) A \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
|
|
192 |
# evs10 \<in> sr"
|
|
193 |
|
|
194 |
(*The card can be exploited by the spy*)
|
|
195 |
(*because of the assumptions on the card, A is certainly not server nor spy*)
|
|
196 |
SR10Fake: "\<lbrakk> evs10F\<in> sr;
|
|
197 |
illegalUse(Card A);
|
|
198 |
K = sesK(Nb,pairK(A,B));
|
|
199 |
Inputs Spy (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb,
|
|
200 |
Nonce (Pairkey(A,B)),
|
|
201 |
Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)),
|
|
202 |
Agent B\<rbrace>,
|
|
203 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
204 |
Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
|
|
205 |
\<in> set evs10F \<rbrakk>
|
|
206 |
\<Longrightarrow> Outpts (Card A) Spy \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
|
|
207 |
# evs10F \<in> sr"
|
|
208 |
|
|
209 |
|
|
210 |
|
|
211 |
|
|
212 |
(*A TOWARDS B*)
|
|
213 |
(*having initiated with B is the only memory A relies on,
|
|
214 |
since the output doesn't mention B - lack of explicitness*)
|
|
215 |
SR11: "\<lbrakk> evs11\<in> sr;
|
|
216 |
Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs11;
|
|
217 |
Outpts (Card A) A \<lbrace>Key K, Certificate\<rbrace> \<in> set evs11 \<rbrakk>
|
|
218 |
\<Longrightarrow> Says A B (Certificate)
|
|
219 |
# evs11 \<in> sr"
|
|
220 |
|
|
221 |
|
|
222 |
|
|
223 |
(*Both peers may leak by accident the session keys obtained from their
|
|
224 |
cards*)
|
|
225 |
Oops1:
|
|
226 |
"\<lbrakk> evsO1 \<in> sr;
|
|
227 |
Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate,
|
|
228 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evsO1 \<rbrakk>
|
|
229 |
\<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO1 \<in> sr"
|
|
230 |
|
|
231 |
Oops2:
|
|
232 |
"\<lbrakk> evsO2 \<in> sr;
|
|
233 |
Outpts (Card A) A \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
|
|
234 |
\<in> set evsO2 \<rbrakk>
|
|
235 |
\<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO2 \<in> sr"
|
|
236 |
|
|
237 |
|
|
238 |
|
|
239 |
|
|
240 |
|
|
241 |
|
|
242 |
(*To solve Fake case when it doesn't involve analz - used to be condensed
|
|
243 |
into Fake_parts_insert_tac*)
|
|
244 |
declare Fake_parts_insert_in_Un [dest]
|
|
245 |
declare analz_into_parts [dest]
|
|
246 |
(*declare parts_insertI [intro]*)
|
|
247 |
|
|
248 |
|
|
249 |
|
|
250 |
(*General facts about message reception*)
|
|
251 |
lemma Gets_imp_Says:
|
|
252 |
"\<lbrakk> Gets B X \<in> set evs; evs \<in> sr \<rbrakk> \<Longrightarrow> \<exists> A. Says A B X \<in> set evs"
|
|
253 |
apply (erule rev_mp, erule sr.induct)
|
|
254 |
apply auto
|
|
255 |
done
|
|
256 |
|
|
257 |
lemma Gets_imp_knows_Spy:
|
|
258 |
"\<lbrakk> Gets B X \<in> set evs; evs \<in> sr \<rbrakk> \<Longrightarrow> X \<in> knows Spy evs"
|
|
259 |
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
|
|
260 |
done
|
|
261 |
|
|
262 |
lemma Gets_imp_knows_Spy_parts_Snd:
|
|
263 |
"\<lbrakk> Gets B \<lbrace>X, Y\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk> \<Longrightarrow> Y \<in> parts (knows Spy evs)"
|
|
264 |
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy parts.Inj parts.Snd)
|
|
265 |
done
|
|
266 |
|
|
267 |
lemma Gets_imp_knows_Spy_analz_Snd:
|
|
268 |
"\<lbrakk> Gets B \<lbrace>X, Y\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk> \<Longrightarrow> Y \<in> analz (knows Spy evs)"
|
|
269 |
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy analz.Inj analz.Snd)
|
|
270 |
done
|
|
271 |
|
|
272 |
(*end general facts*)
|
|
273 |
|
|
274 |
|
|
275 |
|
|
276 |
(*Begin lemmas on secure means, from Event.ML, proved for shouprubin. They help
|
|
277 |
the simplifier, especially in analz_image_freshK*)
|
|
278 |
|
|
279 |
|
|
280 |
lemma Inputs_imp_knows_Spy_secureM_sr:
|
|
281 |
"\<lbrakk> Inputs Spy C X \<in> set evs; evs \<in> sr \<rbrakk> \<Longrightarrow> X \<in> knows Spy evs"
|
|
282 |
apply (simp (no_asm_simp) add: Inputs_imp_knows_Spy_secureM)
|
|
283 |
done
|
|
284 |
|
|
285 |
lemma knows_Spy_Inputs_secureM_sr_Spy:
|
|
286 |
"evs \<in>sr \<Longrightarrow> knows Spy (Inputs Spy C X # evs) = insert X (knows Spy evs)"
|
|
287 |
apply (simp (no_asm_simp))
|
|
288 |
done
|
|
289 |
|
|
290 |
lemma knows_Spy_Inputs_secureM_sr:
|
|
291 |
"\<lbrakk> A \<noteq> Spy; evs \<in>sr \<rbrakk> \<Longrightarrow> knows Spy (Inputs A C X # evs) = knows Spy evs"
|
|
292 |
apply (simp (no_asm_simp))
|
|
293 |
done
|
|
294 |
|
|
295 |
lemma knows_Spy_Outpts_secureM_sr_Spy:
|
|
296 |
"evs \<in>sr \<Longrightarrow> knows Spy (Outpts C Spy X # evs) = insert X (knows Spy evs)"
|
|
297 |
apply (simp (no_asm_simp))
|
|
298 |
done
|
|
299 |
|
|
300 |
lemma knows_Spy_Outpts_secureM_sr:
|
|
301 |
"\<lbrakk> A \<noteq> Spy; evs \<in>sr \<rbrakk> \<Longrightarrow> knows Spy (Outpts C A X # evs) = knows Spy evs"
|
|
302 |
apply (simp (no_asm_simp))
|
|
303 |
done
|
|
304 |
|
|
305 |
(*End lemmas on secure means for shouprubin*)
|
|
306 |
|
|
307 |
|
|
308 |
|
|
309 |
|
|
310 |
(*BEGIN technical lemmas - evolution of forwarding lemmas*)
|
|
311 |
|
|
312 |
(*If an honest agent uses a smart card, then the card is his/her own, is
|
|
313 |
not stolen, and the agent has received suitable data to feed the card.
|
|
314 |
In other words, these are guarantees that an honest agent can only use
|
|
315 |
his/her own card, and must use it correctly.
|
|
316 |
On the contrary, the spy can "Inputs" any cloned cards also by the Fake rule.
|
|
317 |
|
|
318 |
Instead of Auto_tac, proofs here used to asm-simplify and then force-tac.
|
|
319 |
*)
|
|
320 |
lemma Inputs_A_Card_3:
|
|
321 |
"\<lbrakk> Inputs A C (Agent A) \<in> set evs; A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
322 |
\<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>
|
|
323 |
(\<exists> Pk Certificate. Gets A \<lbrace>Pk, Certificate\<rbrace> \<in> set evs)"
|
|
324 |
apply (erule rev_mp, erule sr.induct)
|
|
325 |
apply auto
|
|
326 |
done
|
|
327 |
|
|
328 |
lemma Inputs_B_Card_6:
|
|
329 |
"\<lbrakk> Inputs B C \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs; B \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
330 |
\<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and> Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
|
|
331 |
apply (erule rev_mp, erule sr.induct)
|
|
332 |
apply auto
|
|
333 |
done
|
|
334 |
|
|
335 |
lemma Inputs_A_Card_9:
|
|
336 |
"\<lbrakk> Inputs A C \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
|
|
337 |
Cert1, Cert2, Cert3\<rbrace> \<in> set evs;
|
|
338 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
339 |
\<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>
|
|
340 |
Gets A \<lbrace>Nonce Pk, Cert1\<rbrace> \<in> set evs \<and>
|
|
341 |
Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace> \<in> set evs \<and>
|
|
342 |
Gets A \<lbrace>Nonce Nb, Cert2\<rbrace> \<in> set evs"
|
|
343 |
apply (erule rev_mp, erule sr.induct)
|
|
344 |
apply auto
|
|
345 |
done
|
|
346 |
|
|
347 |
|
|
348 |
(*The two occurrences of A in the Outpts event don't match SR4Fake, where
|
|
349 |
A cannot be the Spy. Hence the card is legally usable by rule SR4*)
|
|
350 |
lemma Outpts_A_Card_4:
|
|
351 |
"\<lbrakk> Outpts C A \<lbrace>Nonce Na, (Crypt (crdK (Card A)) (Nonce Na))\<rbrace> \<in> set evs;
|
|
352 |
evs \<in> sr \<rbrakk>
|
|
353 |
\<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>
|
|
354 |
Inputs A (Card A) (Agent A) \<in> set evs"
|
|
355 |
apply (erule rev_mp, erule sr.induct)
|
|
356 |
apply auto
|
|
357 |
done
|
|
358 |
|
|
359 |
|
|
360 |
(*First certificate is made explicit so that a comment similar to the previous
|
|
361 |
applies. This also provides Na to the Inputs event in the conclusion*)
|
|
362 |
lemma Outpts_B_Card_7:
|
|
363 |
"\<lbrakk> Outpts C B \<lbrace>Nonce Nb, Key K,
|
|
364 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
365 |
Cert2\<rbrace> \<in> set evs;
|
|
366 |
evs \<in> sr \<rbrakk>
|
|
367 |
\<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and>
|
|
368 |
Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
|
|
369 |
apply (erule rev_mp, erule sr.induct)
|
|
370 |
apply auto
|
|
371 |
done
|
|
372 |
|
|
373 |
lemma Outpts_A_Card_10:
|
|
374 |
"\<lbrakk> Outpts C A \<lbrace>Key K, (Crypt (pairK(A,B)) (Nonce Nb))\<rbrace> \<in> set evs;
|
|
375 |
evs \<in> sr \<rbrakk>
|
|
376 |
\<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>
|
|
377 |
(\<exists> Na Ver1 Ver2 Ver3.
|
|
378 |
Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),
|
|
379 |
Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
|
|
380 |
apply (erule rev_mp, erule sr.induct)
|
|
381 |
apply auto
|
|
382 |
done
|
|
383 |
|
|
384 |
|
|
385 |
|
|
386 |
(*
|
|
387 |
A can't check the form of the certificate, and so cannot associate the sesion
|
|
388 |
key to the other peer! This already shows that the protocol fails to satisfy
|
|
389 |
the principle of goal availability for the goal of key association.
|
|
390 |
Similar reasoning below for the goal of confidentiality will be even more
|
|
391 |
accessible.
|
|
392 |
*)
|
|
393 |
lemma Outpts_A_Card_10_imp_Inputs:
|
|
394 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Key K, Certificate\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>
|
|
395 |
\<Longrightarrow> (\<exists> B Na Nb Ver1 Ver2 Ver3.
|
|
396 |
Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),
|
|
397 |
Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
|
|
398 |
apply (erule rev_mp, erule sr.induct)
|
|
399 |
apply simp_all
|
|
400 |
apply blast+
|
|
401 |
done
|
|
402 |
|
|
403 |
|
|
404 |
|
|
405 |
|
|
406 |
(*Weaker version: if the agent can't check the forms of the verifiers, then
|
|
407 |
the agent must not be the spy so as to solve SR4Fake. The verifier must be
|
|
408 |
recognised as some cyphertex in order to distinguish from case SR7,
|
|
409 |
concerning B's output, which also begins with a nonce.
|
|
410 |
*)
|
|
411 |
lemma Outpts_honest_A_Card_4:
|
|
412 |
"\<lbrakk> Outpts C A \<lbrace>Nonce Na, Crypt K X\<rbrace> \<in>set evs;
|
|
413 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
414 |
\<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>
|
|
415 |
Inputs A (Card A) (Agent A) \<in> set evs"
|
|
416 |
apply (erule rev_mp, erule sr.induct)
|
|
417 |
apply auto
|
|
418 |
done
|
|
419 |
|
|
420 |
(*alternative formulation of same theorem
|
|
421 |
Goal "\<lbrakk> Outpts C A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs;
|
|
422 |
\<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>;
|
|
423 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
424 |
\<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>
|
|
425 |
Inputs A (Card A) (Agent A) \<in> set evs"
|
|
426 |
same proof
|
|
427 |
*)
|
|
428 |
|
|
429 |
|
|
430 |
lemma Outpts_honest_B_Card_7:
|
|
431 |
"\<lbrakk> Outpts C B \<lbrace>Nonce Nb, Key K, Cert1, Cert2\<rbrace> \<in> set evs;
|
|
432 |
B \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
433 |
\<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and>
|
|
434 |
(\<exists> A Na. Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs)"
|
|
435 |
apply (erule rev_mp, erule sr.induct)
|
|
436 |
apply auto
|
|
437 |
done
|
|
438 |
|
|
439 |
lemma Outpts_honest_A_Card_10:
|
|
440 |
"\<lbrakk> Outpts C A \<lbrace>Key K, Certificate\<rbrace> \<in> set evs;
|
|
441 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
442 |
\<Longrightarrow> legalUse (C) \<and> C = (Card A) \<and>
|
|
443 |
(\<exists> B Na Nb Pk Ver1 Ver2 Ver3.
|
|
444 |
Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Pk,
|
|
445 |
Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
|
|
446 |
apply (erule rev_mp, erule sr.induct)
|
|
447 |
apply simp_all
|
|
448 |
apply blast+
|
|
449 |
done
|
|
450 |
(*-END-*)
|
|
451 |
|
|
452 |
|
|
453 |
(*Even weaker versions: if the agent can't check the forms of the verifiers
|
|
454 |
and the agent may be the spy, then we must know what card the agent
|
|
455 |
is getting the output from.
|
|
456 |
*)
|
|
457 |
lemma Outpts_which_Card_4:
|
|
458 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt K X\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>
|
|
459 |
\<Longrightarrow> Inputs A (Card A) (Agent A) \<in> set evs"
|
|
460 |
apply (erule rev_mp, erule sr.induct)
|
|
461 |
apply (simp_all (no_asm_simp))
|
|
462 |
apply clarify
|
|
463 |
done
|
|
464 |
|
|
465 |
lemma Outpts_which_Card_7:
|
|
466 |
"\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Cert1, Cert2\<rbrace> \<in> set evs;
|
|
467 |
evs \<in> sr \<rbrakk>
|
|
468 |
\<Longrightarrow> \<exists> A Na. Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
|
|
469 |
apply (erule rev_mp, erule sr.induct)
|
|
470 |
apply auto
|
|
471 |
done
|
|
472 |
|
|
473 |
lemma Outpts_which_Card_10:
|
|
474 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Key (sesK(Nb,pairK(A,B))),
|
|
475 |
Crypt (pairK(A,B)) (Nonce Nb) \<rbrace> \<in> set evs;
|
|
476 |
evs \<in> sr \<rbrakk>
|
|
477 |
\<Longrightarrow> \<exists> Na. Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),
|
|
478 |
Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>,
|
|
479 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
480 |
Crypt (crdK (Card A)) (Nonce Na) \<rbrace> \<in> set evs"
|
|
481 |
apply (erule rev_mp, erule sr.induct)
|
|
482 |
apply auto
|
|
483 |
done
|
|
484 |
|
|
485 |
|
|
486 |
(*Lemmas on the form of outputs*)
|
|
487 |
|
|
488 |
|
|
489 |
(*A needs to check that the verifier is a cipher for it to come from SR4
|
|
490 |
otherwise it could come from SR7 *)
|
|
491 |
lemma Outpts_A_Card_form_4:
|
|
492 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs;
|
|
493 |
\<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>; evs \<in> sr \<rbrakk>
|
|
494 |
\<Longrightarrow> Certificate = (Crypt (crdK (Card A)) (Nonce Na))"
|
|
495 |
apply (erule rev_mp, erule sr.induct)
|
|
496 |
apply (simp_all (no_asm_simp))
|
|
497 |
done
|
|
498 |
|
|
499 |
lemma Outpts_B_Card_form_7:
|
|
500 |
"\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Cert1, Cert2\<rbrace> \<in> set evs;
|
|
501 |
evs \<in> sr \<rbrakk>
|
|
502 |
\<Longrightarrow> \<exists> A Na.
|
|
503 |
K = sesK(Nb,pairK(A,B)) \<and>
|
|
504 |
Cert1 = (Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>) \<and>
|
|
505 |
Cert2 = (Crypt (pairK(A,B)) (Nonce Nb))"
|
|
506 |
apply (erule rev_mp, erule sr.induct)
|
|
507 |
apply auto
|
|
508 |
done
|
|
509 |
|
|
510 |
lemma Outpts_A_Card_form_10:
|
|
511 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Key K, Certificate\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>
|
|
512 |
\<Longrightarrow> \<exists> B Nb.
|
|
513 |
K = sesK(Nb,pairK(A,B)) \<and>
|
|
514 |
Certificate = (Crypt (pairK(A,B)) (Nonce Nb))"
|
|
515 |
apply (erule rev_mp, erule sr.induct)
|
|
516 |
apply (simp_all (no_asm_simp))
|
|
517 |
done
|
|
518 |
|
|
519 |
lemma Outpts_A_Card_form_bis:
|
|
520 |
"\<lbrakk> Outpts (Card A') A' \<lbrace>Key (sesK(Nb,pairK(A,B))), Certificate\<rbrace> \<in> set evs;
|
|
521 |
evs \<in> sr \<rbrakk>
|
|
522 |
\<Longrightarrow> A' = A \<and>
|
|
523 |
Certificate = (Crypt (pairK(A,B)) (Nonce Nb))"
|
|
524 |
apply (erule rev_mp, erule sr.induct)
|
|
525 |
apply (simp_all (no_asm_simp))
|
|
526 |
done
|
|
527 |
|
|
528 |
(*\<dots> and Inputs *)
|
|
529 |
|
|
530 |
lemma Inputs_A_Card_form_9:
|
|
531 |
"\<lbrakk> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
|
|
532 |
Cert1, Cert2, Cert3\<rbrace> \<in> set evs;
|
|
533 |
evs \<in> sr \<rbrakk>
|
|
534 |
\<Longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)"
|
|
535 |
apply (erule rev_mp)
|
|
536 |
apply (erule sr.induct)
|
|
537 |
apply (simp_all (no_asm_simp))
|
|
538 |
(*Fake*)
|
|
539 |
apply force
|
|
540 |
(*SR9*)
|
|
541 |
apply (blast dest!: Outpts_A_Card_form_4)
|
|
542 |
done
|
|
543 |
(* Pk, Cert1, Cert2 cannot be made explicit because they traversed the network in the clear *)
|
|
544 |
|
|
545 |
(*General guarantees on Inputs and Outpts*)
|
|
546 |
|
|
547 |
(*for any agents*)
|
|
548 |
|
|
549 |
|
|
550 |
lemma Inputs_Card_legalUse:
|
|
551 |
"\<lbrakk> Inputs A (Card A) X \<in> set evs; evs \<in> sr \<rbrakk> \<Longrightarrow> legalUse(Card A)"
|
|
552 |
apply (erule rev_mp, erule sr.induct)
|
|
553 |
apply auto
|
|
554 |
done
|
|
555 |
|
|
556 |
lemma Outpts_Card_legalUse:
|
|
557 |
"\<lbrakk> Outpts (Card A) A X \<in> set evs; evs \<in> sr \<rbrakk> \<Longrightarrow> legalUse(Card A)"
|
|
558 |
apply (erule rev_mp, erule sr.induct)
|
|
559 |
apply auto
|
|
560 |
done
|
|
561 |
|
|
562 |
(*for honest agents*)
|
|
563 |
|
|
564 |
lemma Inputs_Card: "\<lbrakk> Inputs A C X \<in> set evs; A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
565 |
\<Longrightarrow> C = (Card A) \<and> legalUse(C)"
|
|
566 |
apply (erule rev_mp, erule sr.induct)
|
|
567 |
apply auto
|
|
568 |
done
|
|
569 |
|
|
570 |
lemma Outpts_Card: "\<lbrakk> Outpts C A X \<in> set evs; A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
571 |
\<Longrightarrow> C = (Card A) \<and> legalUse(C)"
|
|
572 |
apply (erule rev_mp, erule sr.induct)
|
|
573 |
apply auto
|
|
574 |
done
|
|
575 |
|
|
576 |
lemma Inputs_Outpts_Card:
|
|
577 |
"\<lbrakk> Inputs A C X \<in> set evs \<or> Outpts C A Y \<in> set evs;
|
|
578 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
579 |
\<Longrightarrow> C = (Card A) \<and> legalUse(Card A)"
|
|
580 |
apply (blast dest: Inputs_Card Outpts_Card)
|
|
581 |
done
|
|
582 |
|
|
583 |
|
|
584 |
(*for the spy - they stress that the model behaves as it is meant to*)
|
|
585 |
|
|
586 |
(*The or version can be also proved directly.
|
|
587 |
It stresses that the spy may use either her own legally usable card or
|
|
588 |
all the illegally usable cards.
|
|
589 |
*)
|
|
590 |
lemma Inputs_Card_Spy:
|
|
591 |
"\<lbrakk> Inputs Spy C X \<in> set evs \<or> Outpts C Spy X \<in> set evs; evs \<in> sr \<rbrakk>
|
|
592 |
\<Longrightarrow> C = (Card Spy) \<and> legalUse(Card Spy) \<or>
|
|
593 |
(\<exists> A. C = (Card A) \<and> illegalUse(Card A))"
|
|
594 |
apply (erule rev_mp, erule sr.induct)
|
|
595 |
apply auto
|
|
596 |
done
|
|
597 |
|
|
598 |
|
|
599 |
(*END technical lemmas*)
|
|
600 |
|
|
601 |
|
|
602 |
|
|
603 |
|
|
604 |
|
|
605 |
|
|
606 |
(*BEGIN unicity theorems: certain items uniquely identify a smart card's
|
|
607 |
output*)
|
|
608 |
|
|
609 |
(*A's card's first output: the nonce uniquely identifies the rest*)
|
|
610 |
lemma Outpts_A_Card_unique_nonce:
|
|
611 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
|
|
612 |
\<in> set evs;
|
|
613 |
Outpts (Card A') A' \<lbrace>Nonce Na, Crypt (crdK (Card A')) (Nonce Na)\<rbrace>
|
|
614 |
\<in> set evs;
|
|
615 |
evs \<in> sr \<rbrakk> \<Longrightarrow> A=A'"
|
|
616 |
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
|
|
617 |
apply (fastsimp dest: Outpts_parts_used)
|
|
618 |
apply blast
|
|
619 |
done
|
|
620 |
|
|
621 |
(*B's card's output: the NONCE uniquely identifies the rest*)
|
|
622 |
lemma Outpts_B_Card_unique_nonce:
|
|
623 |
"\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Key SK, Cert1, Cert2\<rbrace> \<in> set evs;
|
|
624 |
Outpts (Card B') B' \<lbrace>Nonce Nb, Key SK', Cert1', Cert2'\<rbrace> \<in> set evs;
|
|
625 |
evs \<in> sr \<rbrakk> \<Longrightarrow> B=B' \<and> SK=SK' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
|
|
626 |
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
|
|
627 |
apply (fastsimp dest: Outpts_parts_used)
|
|
628 |
apply blast
|
|
629 |
done
|
|
630 |
|
|
631 |
|
|
632 |
(*B's card's output: the SESKEY uniquely identifies the rest*)
|
|
633 |
lemma Outpts_B_Card_unique_key:
|
|
634 |
"\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Key SK, Cert1, Cert2\<rbrace> \<in> set evs;
|
|
635 |
Outpts (Card B') B' \<lbrace>Nonce Nb', Key SK, Cert1', Cert2'\<rbrace> \<in> set evs;
|
|
636 |
evs \<in> sr \<rbrakk> \<Longrightarrow> B=B' \<and> Nb=Nb' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
|
|
637 |
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
|
|
638 |
apply (fastsimp dest: Outpts_parts_used)
|
|
639 |
apply blast
|
|
640 |
done
|
|
641 |
|
|
642 |
lemma Outpts_A_Card_unique_key: "\<lbrakk> Outpts (Card A) A \<lbrace>Key K, V\<rbrace> \<in> set evs;
|
|
643 |
Outpts (Card A') A' \<lbrace>Key K, V'\<rbrace> \<in> set evs;
|
|
644 |
evs \<in> sr \<rbrakk> \<Longrightarrow> A=A' \<and> V=V'"
|
|
645 |
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
|
|
646 |
apply (blast dest: Outpts_A_Card_form_bis)
|
|
647 |
apply blast
|
|
648 |
done
|
|
649 |
|
|
650 |
|
|
651 |
(*Revised unicity theorems - applies to both steps 4 and 7*)
|
|
652 |
lemma Outpts_A_Card_Unique:
|
|
653 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>
|
|
654 |
\<Longrightarrow> Unique (Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace>) on evs"
|
|
655 |
apply (erule rev_mp, erule sr.induct, simp_all add: Unique_def)
|
|
656 |
apply (fastsimp dest: Outpts_parts_used)
|
|
657 |
apply blast
|
|
658 |
apply (fastsimp dest: Outpts_parts_used)
|
|
659 |
apply blast
|
|
660 |
done
|
|
661 |
|
|
662 |
(*can't prove the same on evs10 for it doesn't have a freshness assumption!*)
|
|
663 |
|
|
664 |
|
|
665 |
(*END unicity theorems*)
|
|
666 |
|
|
667 |
|
|
668 |
(*BEGIN counterguarantees about spy's knowledge*)
|
|
669 |
|
|
670 |
(*on nonces*)
|
|
671 |
|
|
672 |
lemma Spy_knows_Na:
|
|
673 |
"\<lbrakk> Says A B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>
|
|
674 |
\<Longrightarrow> Nonce Na \<in> analz (knows Spy evs)"
|
|
675 |
apply (blast dest!: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd])
|
|
676 |
done
|
|
677 |
|
|
678 |
lemma Spy_knows_Nb:
|
|
679 |
"\<lbrakk> Says B A \<lbrace>Nonce Nb, Certificate\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>
|
|
680 |
\<Longrightarrow> Nonce Nb \<in> analz (knows Spy evs)"
|
|
681 |
apply (blast dest!: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Fst])
|
|
682 |
done
|
|
683 |
|
|
684 |
|
|
685 |
(*on Pairkey*)
|
|
686 |
|
|
687 |
lemma Pairkey_Gets_analz_knows_Spy:
|
|
688 |
"\<lbrakk> Gets A \<lbrace>Nonce (Pairkey(A,B)), Certificate\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>
|
|
689 |
\<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
|
|
690 |
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
|
|
691 |
done
|
|
692 |
|
|
693 |
lemma Pairkey_Inputs_imp_Gets:
|
|
694 |
"\<lbrakk> Inputs A (Card A)
|
|
695 |
\<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),
|
|
696 |
Cert1, Cert3, Cert2\<rbrace> \<in> set evs;
|
|
697 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
698 |
\<Longrightarrow> Gets A \<lbrace>Nonce (Pairkey(A,B)), Cert1\<rbrace> \<in> set evs"
|
|
699 |
apply (erule rev_mp, erule sr.induct)
|
|
700 |
apply (simp_all (no_asm_simp))
|
|
701 |
apply force
|
|
702 |
done
|
|
703 |
|
|
704 |
lemma Pairkey_Inputs_analz_knows_Spy:
|
|
705 |
"\<lbrakk> Inputs A (Card A)
|
|
706 |
\<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),
|
|
707 |
Cert1, Cert3, Cert2\<rbrace> \<in> set evs;
|
|
708 |
evs \<in> sr \<rbrakk>
|
|
709 |
\<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
|
|
710 |
apply (case_tac "A = Spy")
|
|
711 |
apply (fastsimp dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
|
|
712 |
apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy])
|
|
713 |
done
|
|
714 |
|
|
715 |
(* This fails on base case because of XOR properties.
|
|
716 |
lemma Pairkey_authentic:
|
|
717 |
"\<lbrakk> Nonce (Pairkey(A,B)) \<in> parts (knows Spy evs);
|
|
718 |
Card A \<notin> cloned; evs \<in> sr \<rbrakk>
|
|
719 |
\<Longrightarrow> \<exists> cert. Says Server A \<lbrace>Nonce (Pairkey(A,B)), Cert\<rbrace> \<in> set evs"
|
|
720 |
apply (erule rev_mp)
|
|
721 |
apply (erule sr.induct, simp_all)
|
|
722 |
apply clarify
|
|
723 |
oops
|
|
724 |
|
|
725 |
1. \<And>x a b.
|
|
726 |
\<lbrakk>Card A \<notin> cloned; Pairkey (A, B) = Pairkey (a, b); Card a \<in> cloned;
|
|
727 |
Card b \<in> cloned\<rbrakk>
|
|
728 |
\<Longrightarrow> False
|
|
729 |
*)
|
|
730 |
|
|
731 |
(*END counterguarantees on spy's knowledge*)
|
|
732 |
|
|
733 |
|
|
734 |
(*BEGIN rewrite rules for parts operator*)
|
|
735 |
|
|
736 |
|
|
737 |
declare shrK_disj_sesK [THEN not_sym, iff]
|
|
738 |
declare pin_disj_sesK [THEN not_sym, iff]
|
|
739 |
declare crdK_disj_sesK [THEN not_sym, iff]
|
|
740 |
declare pairK_disj_sesK [THEN not_sym, iff]
|
|
741 |
|
|
742 |
|
|
743 |
ML
|
|
744 |
{*
|
|
745 |
val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7"
|
|
746 |
val Outpts_A_Card_form_4 = thm "Outpts_A_Card_form_4"
|
|
747 |
val Outpts_A_Card_form_10 = thm "Outpts_A_Card_form_10"
|
|
748 |
val Gets_imp_knows_Spy = thm "Gets_imp_knows_Spy"
|
|
749 |
val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7"
|
|
750 |
val Gets_imp_knows_Spy_parts_Snd = thm "Gets_imp_knows_Spy_parts_Snd"
|
|
751 |
val Gets_imp_knows_Spy_analz_Snd = thm "Gets_imp_knows_Spy_analz_Snd"
|
|
752 |
|
|
753 |
val prepare_tac =
|
|
754 |
(*SR8*) forward_tac [Outpts_B_Card_form_7] 14 THEN
|
|
755 |
eresolve_tac [exE] 15 THEN eresolve_tac [exE] 15 THEN
|
|
756 |
(*SR9*) forward_tac [Outpts_A_Card_form_4] 16 THEN
|
|
757 |
(*SR11*) forward_tac [Outpts_A_Card_form_10] 21 THEN
|
|
758 |
eresolve_tac [exE] 22 THEN eresolve_tac [exE] 22
|
|
759 |
|
|
760 |
val parts_prepare_tac =
|
|
761 |
prepare_tac THEN
|
|
762 |
(*SR9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN
|
|
763 |
(*SR9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN
|
|
764 |
(*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25 THEN
|
|
765 |
(*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN
|
|
766 |
(*Base*) Force_tac 1
|
|
767 |
|
|
768 |
val analz_prepare_tac =
|
|
769 |
prepare_tac THEN
|
|
770 |
dtac (Gets_imp_knows_Spy_analz_Snd) 18 THEN
|
|
771 |
(*SR9*) dtac (Gets_imp_knows_Spy_analz_Snd) 19 THEN
|
|
772 |
REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
|
|
773 |
|
|
774 |
*}
|
|
775 |
|
|
776 |
method_setup prepare = {*
|
21588
|
777 |
Method.no_args (Method.SIMPLE_METHOD prepare_tac) *}
|
18886
|
778 |
"to launch a few simple facts that'll help the simplifier"
|
|
779 |
|
|
780 |
method_setup parts_prepare = {*
|
21588
|
781 |
Method.no_args (Method.SIMPLE_METHOD parts_prepare_tac) *}
|
18886
|
782 |
"additional facts to reason about parts"
|
|
783 |
|
|
784 |
method_setup analz_prepare = {*
|
21588
|
785 |
Method.no_args (Method.SIMPLE_METHOD analz_prepare_tac) *}
|
18886
|
786 |
"additional facts to reason about analz"
|
|
787 |
|
|
788 |
|
|
789 |
(*Treatment of pins is here for completeness. This protocol doesn't use pins*)
|
|
790 |
lemma Spy_parts_keys [simp]: "evs \<in> sr \<Longrightarrow>
|
|
791 |
(Key (shrK P) \<in> parts (knows Spy evs)) = (Card P \<in> cloned) \<and>
|
|
792 |
(Key (pin P) \<in> parts (knows Spy evs)) = (P \<in> bad \<or> Card P \<in> cloned) \<and>
|
|
793 |
(Key (crdK C) \<in> parts (knows Spy evs)) = (C \<in> cloned) \<and>
|
|
794 |
(Key (pairK(A,B)) \<in> parts (knows Spy evs)) = (Card B \<in> cloned)"
|
|
795 |
apply (erule sr.induct)
|
|
796 |
apply parts_prepare
|
|
797 |
apply simp_all
|
|
798 |
apply (blast intro: parts_insertI)
|
|
799 |
done
|
|
800 |
|
|
801 |
|
|
802 |
(*END rewrite rules for parts operator*)
|
|
803 |
|
|
804 |
(*BEGIN rewrite rules for analz operator*)
|
|
805 |
|
|
806 |
lemma Spy_analz_shrK[simp]: "evs \<in> sr \<Longrightarrow>
|
|
807 |
(Key (shrK P) \<in> analz (knows Spy evs)) = (Card P \<in> cloned)"
|
|
808 |
apply (auto dest!: Spy_knows_cloned)
|
|
809 |
done
|
|
810 |
|
|
811 |
lemma Spy_analz_crdK[simp]: "evs \<in> sr \<Longrightarrow>
|
|
812 |
(Key (crdK C) \<in> analz (knows Spy evs)) = (C \<in> cloned)"
|
|
813 |
apply (auto dest!: Spy_knows_cloned)
|
|
814 |
done
|
|
815 |
|
|
816 |
lemma Spy_analz_pairK[simp]: "evs \<in> sr \<Longrightarrow>
|
|
817 |
(Key (pairK(A,B)) \<in> analz (knows Spy evs)) = (Card B \<in> cloned)"
|
|
818 |
apply (auto dest!: Spy_knows_cloned)
|
|
819 |
done
|
|
820 |
|
|
821 |
|
|
822 |
|
|
823 |
(*Because initState contains a set of nonces, this is needed for base case of
|
|
824 |
analz_image_freshK*)
|
|
825 |
lemma analz_image_Key_Un_Nonce: "analz (Key`K \<union> Nonce`N) = Key`K \<union> Nonce`N"
|
|
826 |
apply auto
|
|
827 |
done
|
|
828 |
|
|
829 |
ML
|
|
830 |
{*
|
|
831 |
val knows_Spy_Inputs_secureM_sr_Spy = thm "knows_Spy_Inputs_secureM_sr_Spy"
|
|
832 |
val knows_Spy_Outpts_secureM_sr_Spy = thm "knows_Spy_Outpts_secureM_sr_Spy"
|
|
833 |
val shouprubin_assumes_securemeans = thm "shouprubin_assumes_securemeans"
|
|
834 |
val analz_image_Key_Un_Nonce= thm "analz_image_Key_Un_Nonce"
|
|
835 |
*}
|
|
836 |
|
|
837 |
method_setup sc_analz_freshK = {*
|
20048
|
838 |
Method.ctxt_args (fn ctxt =>
|
21588
|
839 |
(Method.SIMPLE_METHOD
|
|
840 |
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
|
18886
|
841 |
REPEAT_FIRST (rtac analz_image_freshK_lemma),
|
20048
|
842 |
ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss
|
18886
|
843 |
addsimps [knows_Spy_Inputs_secureM_sr_Spy,
|
|
844 |
knows_Spy_Outpts_secureM_sr_Spy,
|
|
845 |
shouprubin_assumes_securemeans,
|
20048
|
846 |
analz_image_Key_Un_Nonce]))]))) *}
|
18886
|
847 |
"for proving the Session Key Compromise theorem for smartcard protocols"
|
|
848 |
|
|
849 |
|
|
850 |
lemma analz_image_freshK [rule_format]:
|
|
851 |
"evs \<in> sr \<Longrightarrow> \<forall> K KK.
|
|
852 |
(Key K \<in> analz (Key`KK \<union> (knows Spy evs))) =
|
|
853 |
(K \<in> KK \<or> Key K \<in> analz (knows Spy evs))"
|
|
854 |
apply (erule sr.induct)
|
|
855 |
apply analz_prepare
|
|
856 |
apply sc_analz_freshK
|
|
857 |
apply spy_analz
|
|
858 |
done
|
|
859 |
|
|
860 |
|
|
861 |
lemma analz_insert_freshK: "evs \<in> sr \<Longrightarrow>
|
|
862 |
Key K \<in> analz (insert (Key K') (knows Spy evs)) =
|
|
863 |
(K = K' \<or> Key K \<in> analz (knows Spy evs))"
|
|
864 |
apply (simp only: analz_image_freshK_simps analz_image_freshK)
|
|
865 |
done
|
|
866 |
|
|
867 |
(*END rewrite rules for analz operator*)
|
|
868 |
|
|
869 |
(*BEGIN authenticity theorems*)
|
|
870 |
|
|
871 |
|
|
872 |
|
|
873 |
|
|
874 |
(*Card B \<notin> cloned needed for Fake
|
|
875 |
B \<notin> bad needed for SR7Fake; equivalent to Card B \<notin> stolen
|
|
876 |
*)
|
|
877 |
|
|
878 |
lemma Na_Nb_certificate_authentic:
|
|
879 |
"\<lbrakk> Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<in> parts (knows Spy evs);
|
|
880 |
\<not>illegalUse(Card B);
|
|
881 |
evs \<in> sr \<rbrakk>
|
|
882 |
\<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Key (sesK(Nb,pairK(A,B))),
|
|
883 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
884 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
|
|
885 |
apply (erule rev_mp, erule sr.induct)
|
|
886 |
apply parts_prepare
|
|
887 |
apply simp_all
|
|
888 |
(*Fake*)
|
|
889 |
apply spy_analz
|
|
890 |
(*SR7F*)
|
|
891 |
apply clarify
|
|
892 |
done
|
|
893 |
|
|
894 |
(* Card B \<notin> cloned needed for Fake and SR7F
|
|
895 |
B \<noteq> Spy needed for SR7
|
|
896 |
B \<notin> bad - or Card B \<notin> stolen - needed for SR7F
|
|
897 |
Card A \<notin> cloned needed for SR10F
|
|
898 |
A \<notin> bad - or Card A \<notin> stolen - needed for SR10F
|
|
899 |
|
|
900 |
Non-trivial case done by the simplifier.*)
|
|
901 |
lemma Nb_certificate_authentic:
|
|
902 |
"\<lbrakk> Crypt (pairK(A,B)) (Nonce Nb) \<in> parts (knows Spy evs);
|
|
903 |
B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B);
|
|
904 |
evs \<in> sr \<rbrakk>
|
|
905 |
\<Longrightarrow> Outpts (Card A) A \<lbrace>Key (sesK(Nb,pairK(A,B))),
|
|
906 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
|
|
907 |
apply (erule rev_mp, erule sr.induct)
|
|
908 |
apply parts_prepare
|
|
909 |
apply (case_tac [17] "Aa = Spy")
|
|
910 |
apply simp_all
|
|
911 |
(*Fake*)
|
|
912 |
apply spy_analz
|
|
913 |
(*SR7F, SR10F*)
|
|
914 |
apply clarify+
|
|
915 |
done
|
|
916 |
|
|
917 |
|
|
918 |
|
|
919 |
(*Discovering the very origin of the Nb certificate... non needed!*)
|
|
920 |
(*lemma*)
|
|
921 |
lemma Outpts_A_Card_imp_pairK_parts:
|
|
922 |
"\<lbrakk> Outpts (Card A) A
|
|
923 |
\<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs;
|
|
924 |
evs \<in> sr \<rbrakk>
|
|
925 |
\<Longrightarrow> \<exists> Na. Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<in> parts (knows Spy evs)"
|
|
926 |
apply (erule rev_mp, erule sr.induct)
|
|
927 |
apply parts_prepare
|
|
928 |
apply simp_all
|
|
929 |
(*Fake*)
|
|
930 |
apply (blast dest: parts_insertI)
|
|
931 |
(*SR7*)
|
|
932 |
apply force
|
|
933 |
(*SR7F*)
|
|
934 |
apply force
|
|
935 |
(*SR8*)
|
|
936 |
apply blast
|
|
937 |
(*SR10*)
|
|
938 |
apply (blast dest: Inputs_imp_knows_Spy_secureM_sr parts.Inj Inputs_A_Card_9 Gets_imp_knows_Spy elim: knows_Spy_partsEs)
|
|
939 |
(*SR10F*)
|
|
940 |
apply (blast dest: Inputs_imp_knows_Spy_secureM_sr [THEN parts.Inj]
|
|
941 |
Inputs_A_Card_9 Gets_imp_knows_Spy
|
|
942 |
elim: knows_Spy_partsEs)
|
|
943 |
done
|
|
944 |
|
|
945 |
|
|
946 |
|
|
947 |
lemma Nb_certificate_authentic_bis:
|
|
948 |
"\<lbrakk> Crypt (pairK(A,B)) (Nonce Nb) \<in> parts (knows Spy evs);
|
|
949 |
B \<noteq> Spy; \<not>illegalUse(Card B);
|
|
950 |
evs \<in> sr \<rbrakk>
|
|
951 |
\<Longrightarrow> \<exists> Na. Outpts (Card B) B \<lbrace>Nonce Nb, Key (sesK(Nb,pairK(A,B))),
|
|
952 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
953 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
|
|
954 |
apply (erule rev_mp, erule sr.induct)
|
|
955 |
apply parts_prepare
|
|
956 |
apply (simp_all (no_asm_simp))
|
|
957 |
(*Fake*)
|
|
958 |
apply spy_analz
|
|
959 |
(*SR7*)
|
|
960 |
apply blast
|
|
961 |
(*SR7F*)
|
|
962 |
apply blast
|
|
963 |
(*SR10*)
|
|
964 |
apply (blast dest: Na_Nb_certificate_authentic Inputs_imp_knows_Spy_secureM_sr [THEN parts.Inj] elim: knows_Spy_partsEs)
|
|
965 |
(*SR10F*)
|
|
966 |
apply (blast dest: Na_Nb_certificate_authentic Inputs_imp_knows_Spy_secureM_sr [THEN parts.Inj] elim: knows_Spy_partsEs)
|
|
967 |
(*SR11*)
|
|
968 |
apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_imp_pairK_parts)
|
|
969 |
done
|
|
970 |
|
|
971 |
|
|
972 |
lemma Pairkey_certificate_authentic:
|
|
973 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace> \<in> parts (knows Spy evs);
|
|
974 |
Card A \<notin> cloned; evs \<in> sr \<rbrakk>
|
|
975 |
\<Longrightarrow> Pk = Pairkey(A,B) \<and>
|
|
976 |
Says Server A \<lbrace>Nonce Pk,
|
|
977 |
Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>\<rbrace>
|
|
978 |
\<in> set evs"
|
|
979 |
apply (erule rev_mp, erule sr.induct)
|
|
980 |
apply parts_prepare
|
|
981 |
apply (simp_all (no_asm_simp))
|
|
982 |
(*Fake*)
|
|
983 |
apply spy_analz
|
|
984 |
done
|
|
985 |
|
|
986 |
|
|
987 |
(*Alternatively: A \<notin> bad; Card A \<notin> cloned; B \<notin> bad; Card B \<notin> cloned;*)
|
|
988 |
lemma sesK_authentic:
|
|
989 |
"\<lbrakk> Key (sesK(Nb,pairK(A,B))) \<in> parts (knows Spy evs);
|
|
990 |
A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B);
|
|
991 |
evs \<in> sr \<rbrakk>
|
|
992 |
\<Longrightarrow> Notes Spy \<lbrace>Key (sesK(Nb,pairK(A,B))), Nonce Nb, Agent A, Agent B\<rbrace>
|
|
993 |
\<in> set evs"
|
|
994 |
apply (erule rev_mp, erule sr.induct)
|
|
995 |
apply parts_prepare
|
|
996 |
apply (simp_all (no_asm_simp))
|
|
997 |
(*fake*)
|
|
998 |
apply spy_analz
|
|
999 |
(*forge*)
|
|
1000 |
apply (fastsimp dest: analz.Inj)
|
|
1001 |
(*SR7: used B\<noteq>Spy*)
|
|
1002 |
(*SR7F*)
|
|
1003 |
apply clarify
|
|
1004 |
(*SR10: used A\<noteq>Spy*)
|
|
1005 |
(*SR10F*)
|
|
1006 |
apply clarify
|
|
1007 |
(*Oops*)
|
|
1008 |
apply simp_all
|
|
1009 |
done
|
|
1010 |
|
|
1011 |
|
|
1012 |
(*END authenticity theorems*)
|
|
1013 |
|
|
1014 |
|
|
1015 |
(*BEGIN confidentiality theorems*)
|
|
1016 |
|
|
1017 |
(*If B were bad and his card stolen, they spy could use B's card but would
|
|
1018 |
not obtain this K because B's card only issues new session keys out
|
|
1019 |
of new nonces.
|
|
1020 |
If A were bad, then her card could be stolen, hence the spy could feed it
|
|
1021 |
with Nb and get this K. Thus, A\<notin>bad can be replaced by Card A \<notin> stolen
|
|
1022 |
Hence these are the minimal assumptions:
|
|
1023 |
A \<notin> bad; B \<noteq> Spy; Card A \<notin> cloned; Card B \<notin> cloned;
|
|
1024 |
A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); Card B \<notin> cloned;
|
|
1025 |
*)
|
|
1026 |
|
|
1027 |
lemma Confidentiality:
|
|
1028 |
"\<lbrakk> Notes Spy \<lbrace>Key (sesK(Nb,pairK(A,B))), Nonce Nb, Agent A, Agent B\<rbrace>
|
|
1029 |
\<notin> set evs;
|
|
1030 |
A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B);
|
|
1031 |
evs \<in> sr \<rbrakk>
|
|
1032 |
\<Longrightarrow> Key (sesK(Nb,pairK(A,B))) \<notin> analz (knows Spy evs)"
|
|
1033 |
apply (blast intro: sesK_authentic)
|
|
1034 |
done
|
|
1035 |
|
|
1036 |
lemma Confidentiality_B:
|
|
1037 |
"\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate,
|
|
1038 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs;
|
|
1039 |
Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> \<notin> set evs;
|
|
1040 |
A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); Card B \<notin> cloned;
|
|
1041 |
evs \<in> sr \<rbrakk>
|
|
1042 |
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
|
|
1043 |
apply (erule rev_mp, erule rev_mp, erule sr.induct)
|
|
1044 |
apply analz_prepare
|
|
1045 |
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
|
|
1046 |
(*Fake*)
|
|
1047 |
apply spy_analz
|
|
1048 |
(*Forge*)
|
|
1049 |
apply (rotate_tac 7)
|
|
1050 |
apply (drule parts.Inj)
|
|
1051 |
apply (fastsimp dest: Outpts_B_Card_form_7)
|
|
1052 |
(*SR7*)
|
|
1053 |
apply (blast dest!: Outpts_B_Card_form_7)
|
|
1054 |
(*SR7F*)
|
|
1055 |
apply clarify
|
|
1056 |
apply (drule Outpts_parts_used)
|
|
1057 |
apply simp
|
|
1058 |
(*faster than
|
|
1059 |
by (fast_tac (claset() addDs [Outpts_parts_used] addss (simpset())) 1)
|
|
1060 |
*)
|
|
1061 |
(*SR10*)
|
|
1062 |
apply (fastsimp dest: Outpts_B_Card_form_7)
|
|
1063 |
(*SR10F - uses assumption Card A not cloned*)
|
|
1064 |
apply clarify
|
|
1065 |
apply (drule Outpts_B_Card_form_7, assumption)
|
|
1066 |
apply simp
|
|
1067 |
(*Oops1*)
|
|
1068 |
apply (blast dest!: Outpts_B_Card_form_7)
|
|
1069 |
(*Oops2*)
|
|
1070 |
apply (blast dest!: Outpts_B_Card_form_7 Outpts_A_Card_form_10)
|
|
1071 |
done
|
|
1072 |
|
|
1073 |
(*Confidentiality_A can be is faster to prove in forward style, using
|
|
1074 |
the authentication theorems. So it is moved below*)
|
|
1075 |
|
|
1076 |
|
|
1077 |
(*END confidentiality theorems*)
|
|
1078 |
|
|
1079 |
|
|
1080 |
|
|
1081 |
(*BEGIN authentication theorems*)
|
|
1082 |
|
|
1083 |
lemma A_authenticates_B:
|
|
1084 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs;
|
|
1085 |
\<not>illegalUse(Card B);
|
|
1086 |
evs \<in> sr \<rbrakk>
|
|
1087 |
\<Longrightarrow> \<exists> Na.
|
|
1088 |
Outpts (Card B) B \<lbrace>Nonce Nb, Key K,
|
|
1089 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
1090 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
|
|
1091 |
apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_form_10 Outpts_A_Card_imp_pairK_parts)
|
|
1092 |
done
|
|
1093 |
|
|
1094 |
lemma A_authenticates_B_Gets:
|
|
1095 |
"\<lbrakk> Gets A \<lbrace>Nonce Nb, Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>\<rbrace>
|
|
1096 |
\<in> set evs;
|
|
1097 |
\<not>illegalUse(Card B);
|
|
1098 |
evs \<in> sr \<rbrakk>
|
|
1099 |
\<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Key (sesK(Nb, pairK (A, B))),
|
|
1100 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
1101 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
|
|
1102 |
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN Na_Nb_certificate_authentic])
|
|
1103 |
done
|
|
1104 |
|
|
1105 |
|
|
1106 |
|
|
1107 |
|
|
1108 |
lemma B_authenticates_A:
|
|
1109 |
"\<lbrakk> Gets B (Crypt (pairK(A,B)) (Nonce Nb)) \<in> set evs;
|
|
1110 |
B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B);
|
|
1111 |
evs \<in> sr \<rbrakk>
|
|
1112 |
\<Longrightarrow> Outpts (Card A) A
|
|
1113 |
\<lbrace>Key (sesK(Nb,pairK(A,B))), Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
|
|
1114 |
apply (erule rev_mp)
|
|
1115 |
apply (erule sr.induct)
|
|
1116 |
apply (simp_all (no_asm_simp))
|
|
1117 |
apply (blast dest: Says_imp_knows_Spy [THEN parts.Inj] Nb_certificate_authentic)
|
|
1118 |
done
|
|
1119 |
|
|
1120 |
|
|
1121 |
(*END authentication theorems*)
|
|
1122 |
|
|
1123 |
lemma Confidentiality_A: "\<lbrakk> Outpts (Card A) A
|
|
1124 |
\<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs;
|
|
1125 |
Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> \<notin> set evs;
|
|
1126 |
A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B);
|
|
1127 |
evs \<in> sr \<rbrakk>
|
|
1128 |
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
|
|
1129 |
apply (drule A_authenticates_B)
|
|
1130 |
prefer 3
|
|
1131 |
apply (erule exE)
|
|
1132 |
apply (drule Confidentiality_B)
|
|
1133 |
apply auto
|
|
1134 |
done
|
|
1135 |
|
|
1136 |
lemma Outpts_imp_knows_agents_secureM_sr:
|
|
1137 |
"\<lbrakk> Outpts (Card A) A X \<in> set evs; evs \<in> sr \<rbrakk> \<Longrightarrow> X \<in> knows A evs"
|
|
1138 |
apply (simp (no_asm_simp) add: Outpts_imp_knows_agents_secureM)
|
|
1139 |
done
|
|
1140 |
|
|
1141 |
|
|
1142 |
(*BEGIN key distribution theorems*)
|
|
1143 |
|
|
1144 |
|
|
1145 |
(*Alternatively: B \<notin> bad; Card B \<notin> cloned;*)
|
|
1146 |
lemma A_keydist_to_B:
|
|
1147 |
"\<lbrakk> Outpts (Card A) A
|
|
1148 |
\<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs;
|
|
1149 |
\<not>illegalUse(Card B);
|
|
1150 |
evs \<in> sr \<rbrakk>
|
|
1151 |
\<Longrightarrow> Key K \<in> analz (knows B evs)"
|
|
1152 |
apply (drule A_authenticates_B)
|
|
1153 |
prefer 3
|
|
1154 |
apply (erule exE)
|
|
1155 |
apply (rule Outpts_imp_knows_agents_secureM_sr [THEN analz.Inj, THEN analz.Snd, THEN analz.Fst])
|
|
1156 |
apply assumption+
|
|
1157 |
done
|
|
1158 |
|
|
1159 |
|
|
1160 |
(*Alternatively: A \<notin> bad; B \<notin> bad; Card A \<notin> cloned; Card B \<notin> cloned;*)
|
|
1161 |
lemma B_keydist_to_A:
|
|
1162 |
"\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate,
|
|
1163 |
(Crypt (pairK(A,B)) (Nonce Nb))\<rbrace> \<in> set evs;
|
|
1164 |
Gets B (Crypt (pairK(A,B)) (Nonce Nb)) \<in> set evs;
|
|
1165 |
B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B);
|
|
1166 |
evs \<in> sr \<rbrakk>
|
|
1167 |
\<Longrightarrow> Key K \<in> analz (knows A evs)"
|
|
1168 |
apply (frule B_authenticates_A)
|
|
1169 |
apply (drule_tac [5] Outpts_B_Card_form_7)
|
|
1170 |
apply (rule_tac [6] Outpts_imp_knows_agents_secureM_sr [THEN analz.Inj, THEN analz.Fst])
|
|
1171 |
prefer 6 apply force
|
|
1172 |
apply assumption+
|
|
1173 |
done
|
|
1174 |
|
|
1175 |
(*END key distribution theorems*)
|
|
1176 |
|
|
1177 |
|
|
1178 |
|
|
1179 |
|
|
1180 |
|
|
1181 |
|
|
1182 |
|
|
1183 |
|
|
1184 |
(*BEGIN further theorems about authenticity of verifiers
|
|
1185 |
(useful to agents and cards). *)
|
|
1186 |
|
|
1187 |
(*MSG11
|
|
1188 |
If B receives the verifier of msg11, then the verifier originated with msg7.
|
|
1189 |
Alternatively: A \<notin> bad; B \<notin> bad; Card A \<notin> cloned; Card B \<notin> cloned;
|
|
1190 |
*)
|
|
1191 |
lemma Nb_certificate_authentic_B:
|
|
1192 |
"\<lbrakk> Gets B (Crypt (pairK(A,B)) (Nonce Nb)) \<in> set evs;
|
|
1193 |
B \<noteq> Spy; \<not>illegalUse(Card B);
|
|
1194 |
evs \<in> sr \<rbrakk>
|
|
1195 |
\<Longrightarrow> \<exists> Na.
|
|
1196 |
Outpts (Card B) B \<lbrace>Nonce Nb, Key (sesK(Nb,pairK(A,B))),
|
|
1197 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
1198 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
|
|
1199 |
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN Nb_certificate_authentic_bis])
|
|
1200 |
done
|
|
1201 |
(*Useless to B: B can't check the form of the verifier because he doesn't know
|
|
1202 |
pairK(A,B) *)
|
|
1203 |
|
|
1204 |
(*MSG10
|
|
1205 |
If A obtains the verifier of msg10, then the verifier originated with msg7:
|
|
1206 |
A_authenticates_B. It is useful to A, who can check the form of the
|
|
1207 |
verifier by application of Outpts_A_Card_form_10.
|
|
1208 |
*)
|
|
1209 |
|
|
1210 |
(*MSG9
|
|
1211 |
The first verifier verifies the Pairkey to the card: since it's encrypted
|
|
1212 |
under Ka, it must come from the server (if A's card is not cloned).
|
|
1213 |
The second verifier verifies both nonces, since it's encrypted under the
|
|
1214 |
pairK, it must originate with B's card (if A and B's cards not cloned).
|
|
1215 |
The third verifier verifies Na: since it's encrytped under the card's key,
|
|
1216 |
it originated with the card; so the card does not need to save Na
|
|
1217 |
in the first place and do a comparison now: it just verifies Na through the
|
|
1218 |
verifier. Three theorems related to these three statements.
|
|
1219 |
|
|
1220 |
Recall that a card can check the form of the verifiers (can decrypt them),
|
|
1221 |
while an agent in general cannot, if not provided with a suitable theorem.
|
|
1222 |
*)
|
|
1223 |
|
|
1224 |
(*Card A can't reckon the pairkey - we need to guarantee its integrity!*)
|
|
1225 |
lemma Pairkey_certificate_authentic_A_Card:
|
|
1226 |
"\<lbrakk> Inputs A (Card A)
|
|
1227 |
\<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
|
|
1228 |
Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>,
|
|
1229 |
Cert2, Cert3\<rbrace> \<in> set evs;
|
|
1230 |
A \<noteq> Spy; Card A \<notin> cloned; evs \<in> sr \<rbrakk>
|
|
1231 |
\<Longrightarrow> Pk = Pairkey(A,B) \<and>
|
|
1232 |
Says Server A \<lbrace>Nonce (Pairkey(A,B)),
|
|
1233 |
Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>\<rbrace>
|
|
1234 |
\<in> set evs "
|
|
1235 |
apply (blast dest: Inputs_A_Card_9 Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd] Pairkey_certificate_authentic)
|
|
1236 |
done
|
|
1237 |
(*the second conjunct of the thesis might be regarded as a form of integrity
|
|
1238 |
in the sense of Neuman-Ts'o*)
|
|
1239 |
|
|
1240 |
lemma Na_Nb_certificate_authentic_A_Card:
|
|
1241 |
"\<lbrakk> Inputs A (Card A)
|
|
1242 |
\<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
|
|
1243 |
Cert1,
|
|
1244 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, Cert3\<rbrace> \<in> set evs;
|
|
1245 |
A \<noteq> Spy; \<not>illegalUse(Card B); evs \<in> sr \<rbrakk>
|
|
1246 |
\<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Key (sesK(Nb, pairK (A, B))),
|
|
1247 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
1248 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
|
|
1249 |
\<in> set evs "
|
|
1250 |
apply (blast dest: Inputs_A_Card_9 Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN Na_Nb_certificate_authentic])
|
|
1251 |
done
|
|
1252 |
|
|
1253 |
lemma Na_authentic_A_Card:
|
|
1254 |
"\<lbrakk> Inputs A (Card A)
|
|
1255 |
\<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
|
|
1256 |
Cert1, Cert2, Cert3\<rbrace> \<in> set evs;
|
|
1257 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
1258 |
\<Longrightarrow> Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace>
|
|
1259 |
\<in> set evs"
|
|
1260 |
apply (blast dest: Inputs_A_Card_9)
|
|
1261 |
done
|
|
1262 |
|
|
1263 |
(* The last three theorems for Card A can be put togheter trivially.
|
|
1264 |
They are separated to highlight the different requirements on agents
|
|
1265 |
and their cards.*)
|
|
1266 |
|
|
1267 |
|
|
1268 |
(*Alternatively:
|
|
1269 |
A \<noteq> Spy; B \<notin> bad; Card A \<notin> cloned; Card B \<notin> cloned; evs \<in> sr \<rbrakk> *)
|
|
1270 |
lemma Inputs_A_Card_9_authentic:
|
|
1271 |
"\<lbrakk> Inputs A (Card A)
|
|
1272 |
\<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
|
|
1273 |
Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>,
|
|
1274 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, Cert3\<rbrace> \<in> set evs;
|
|
1275 |
A \<noteq> Spy; Card A \<notin> cloned;\<not>illegalUse(Card B); evs \<in> sr \<rbrakk>
|
|
1276 |
\<Longrightarrow> Says Server A \<lbrace>Nonce Pk, Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>\<rbrace>
|
|
1277 |
\<in> set evs \<and>
|
|
1278 |
Outpts (Card B) B \<lbrace>Nonce Nb, Key (sesK(Nb, pairK (A, B))),
|
|
1279 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
1280 |
Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
|
|
1281 |
\<in> set evs \<and>
|
|
1282 |
Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace>
|
|
1283 |
\<in> set evs"
|
|
1284 |
apply (blast dest: Inputs_A_Card_9 Na_Nb_certificate_authentic Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd] Pairkey_certificate_authentic)
|
|
1285 |
done
|
|
1286 |
|
|
1287 |
(*MSG8
|
|
1288 |
Nothing to prove because the message is a cleartext that comes from the
|
|
1289 |
network*)
|
|
1290 |
|
|
1291 |
(*Other messages: nothing to prove because the verifiers involved are new*)
|
|
1292 |
|
|
1293 |
|
|
1294 |
(*END further theorems about authenticity of verifiers*)
|
|
1295 |
|
|
1296 |
|
|
1297 |
|
|
1298 |
(* BEGIN trivial guarantees on outputs for agents *)
|
|
1299 |
|
|
1300 |
(*MSG4*)
|
|
1301 |
lemma SR4_imp:
|
|
1302 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
|
|
1303 |
\<in> set evs;
|
|
1304 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
1305 |
\<Longrightarrow> \<exists> Pk V. Gets A \<lbrace>Pk, V\<rbrace> \<in> set evs"
|
|
1306 |
apply (blast dest: Outpts_A_Card_4 Inputs_A_Card_3)
|
|
1307 |
done
|
|
1308 |
(*weak: could strengthen the model adding verifier for the Pairkey to msg3*)
|
|
1309 |
|
|
1310 |
|
|
1311 |
(*MSG7*)
|
|
1312 |
lemma SR7_imp:
|
|
1313 |
"\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Key K,
|
|
1314 |
Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,
|
|
1315 |
Cert2\<rbrace> \<in> set evs;
|
|
1316 |
B \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
1317 |
\<Longrightarrow> Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
|
|
1318 |
apply (blast dest: Outpts_B_Card_7 Inputs_B_Card_6)
|
|
1319 |
done
|
|
1320 |
|
|
1321 |
(*MSG10*)
|
|
1322 |
lemma SR10_imp:
|
|
1323 |
"\<lbrakk> Outpts (Card A) A \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
|
|
1324 |
\<in> set evs;
|
|
1325 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
1326 |
\<Longrightarrow> \<exists> Cert1 Cert2.
|
|
1327 |
Gets A \<lbrace>Nonce (Pairkey (A, B)), Cert1\<rbrace> \<in> set evs \<and>
|
|
1328 |
Gets A \<lbrace>Nonce Nb, Cert2\<rbrace> \<in> set evs"
|
|
1329 |
apply (blast dest: Outpts_A_Card_10 Inputs_A_Card_9)
|
|
1330 |
done
|
|
1331 |
|
|
1332 |
|
|
1333 |
(*END trivial guarantees on outputs for agents*)
|
|
1334 |
|
|
1335 |
|
|
1336 |
|
|
1337 |
(*INTEGRITY*)
|
|
1338 |
lemma Outpts_Server_not_evs: "evs \<in> sr \<Longrightarrow> Outpts (Card Server) P X \<notin> set evs"
|
|
1339 |
apply (erule sr.induct)
|
|
1340 |
apply auto
|
|
1341 |
done
|
|
1342 |
|
|
1343 |
text{*@{term step2_integrity} also is a reliability theorem*}
|
|
1344 |
lemma Says_Server_message_form:
|
|
1345 |
"\<lbrakk> Says Server A \<lbrace>Pk, Certificate\<rbrace> \<in> set evs;
|
|
1346 |
evs \<in> sr \<rbrakk>
|
|
1347 |
\<Longrightarrow> \<exists> B. Pk = Nonce (Pairkey(A,B)) \<and>
|
|
1348 |
Certificate = Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>"
|
|
1349 |
apply (erule rev_mp)
|
|
1350 |
apply (erule sr.induct)
|
|
1351 |
apply auto
|
|
1352 |
apply (blast dest!: Outpts_Server_not_evs)+
|
|
1353 |
done
|
|
1354 |
(*cannot be made useful to A in form of a Gets event*)
|
|
1355 |
|
|
1356 |
text{*
|
|
1357 |
step4integrity is @{term Outpts_A_Card_form_4}
|
|
1358 |
|
|
1359 |
step7integrity is @{term Outpts_B_Card_form_7}
|
|
1360 |
*}
|
|
1361 |
|
|
1362 |
lemma step8_integrity:
|
|
1363 |
"\<lbrakk> Says B A \<lbrace>Nonce Nb, Certificate\<rbrace> \<in> set evs;
|
|
1364 |
B \<noteq> Server; B \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
1365 |
\<Longrightarrow> \<exists> Cert2 K.
|
|
1366 |
Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Cert2\<rbrace> \<in> set evs"
|
|
1367 |
apply (erule rev_mp)
|
|
1368 |
apply (erule sr.induct)
|
|
1369 |
prefer 18 apply (fastsimp dest: Outpts_A_Card_form_10)
|
|
1370 |
apply auto
|
|
1371 |
done
|
|
1372 |
|
|
1373 |
|
|
1374 |
text{* step9integrity is @{term Inputs_A_Card_form_9}
|
|
1375 |
|
|
1376 |
step10integrity is @{term Outpts_A_Card_form_10}.
|
|
1377 |
*}
|
|
1378 |
|
|
1379 |
lemma step11_integrity:
|
|
1380 |
"\<lbrakk> Says A B (Certificate) \<in> set evs;
|
|
1381 |
\<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>;
|
|
1382 |
A \<noteq> Spy; evs \<in> sr \<rbrakk>
|
|
1383 |
\<Longrightarrow> \<exists> K.
|
|
1384 |
Outpts (Card A) A \<lbrace>Key K, Certificate\<rbrace> \<in> set evs"
|
|
1385 |
apply (erule rev_mp)
|
|
1386 |
apply (erule sr.induct)
|
|
1387 |
apply auto
|
|
1388 |
done
|
|
1389 |
|
|
1390 |
|
|
1391 |
|
|
1392 |
|
|
1393 |
|
|
1394 |
|
|
1395 |
end
|
|
1396 |
|