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