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