author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 41775 | 6214816d79d3 |
child 61830 | 4f5ab843cf5b |
permissions | -rw-r--r-- |
41775 | 1 |
(* Title: HOL/Auth/Guard/P2.thy |
2 |
Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 |
Copyright 2002 University of Cambridge |
|
13508 | 4 |
|
41775 | 5 |
From G. Karjoth, N. Asokan and C. Gulcu |
6 |
"Protecting the computation results of free-roaming agents" |
|
7 |
Mobiles Agents 1998, LNCS 1477. |
|
8 |
*) |
|
13508 | 9 |
|
58889 | 10 |
section{*Protocol P2*} |
13508 | 11 |
|
16417 | 12 |
theory P2 imports Guard_Public List_Msg begin |
13508 | 13 |
|
14 |
subsection{*Protocol Definition*} |
|
15 |
||
16 |
||
17 |
text{*Like P1 except the definitions of @{text chain}, @{text shop}, |
|
18 |
@{text next_shop} and @{text nonce}*} |
|
19 |
||
20 |
subsubsection{*offer chaining: |
|
21 |
B chains his offer for A with the head offer of L for sending it to C*} |
|
22 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
23 |
definition chain :: "agent => nat => agent => msg => agent => msg" where |
13508 | 24 |
"chain B ofr A L C == |
25 |
let m1= sign B (Nonce ofr) in |
|
26 |
let m2= Hash {|head L, Agent C|} in |
|
27 |
{|Crypt (pubK A) m1, m2|}" |
|
28 |
||
29 |
declare Let_def [simp] |
|
30 |
||
31 |
lemma chain_inj [iff]: "(chain B ofr A L C = chain B' ofr' A' L' C') |
|
32 |
= (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')" |
|
33 |
by (auto simp: chain_def Let_def) |
|
34 |
||
35 |
lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}" |
|
36 |
by (auto simp: chain_def sign_def) |
|
37 |
||
38 |
subsubsection{*agent whose key is used to sign an offer*} |
|
39 |
||
35418 | 40 |
fun shop :: "msg => msg" where |
13508 | 41 |
"shop {|Crypt K {|B,ofr,Crypt K' H|},m2|} = Agent (agt K')" |
42 |
||
43 |
lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B" |
|
44 |
by (simp add: chain_def sign_def) |
|
45 |
||
46 |
subsubsection{*nonce used in an offer*} |
|
47 |
||
35418 | 48 |
fun nonce :: "msg => msg" where |
13508 | 49 |
"nonce {|Crypt K {|B,ofr,CryptH|},m2|} = ofr" |
50 |
||
51 |
lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr" |
|
52 |
by (simp add: chain_def sign_def) |
|
53 |
||
54 |
subsubsection{*next shop*} |
|
55 |
||
35418 | 56 |
fun next_shop :: "msg => agent" where |
13508 | 57 |
"next_shop {|m1,Hash {|headL,Agent C|}|} = C" |
58 |
||
59 |
lemma "next_shop (chain B ofr A L C) = C" |
|
60 |
by (simp add: chain_def sign_def) |
|
61 |
||
62 |
subsubsection{*anchor of the offer list*} |
|
63 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
64 |
definition anchor :: "agent => nat => agent => msg" where |
13508 | 65 |
"anchor A n B == chain A n A (cons nil nil) B" |
66 |
||
67 |
lemma anchor_inj [iff]: |
|
68 |
"(anchor A n B = anchor A' n' B') = (A=A' & n=n' & B=B')" |
|
69 |
by (auto simp: anchor_def) |
|
70 |
||
71 |
lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}" |
|
72 |
by (auto simp: anchor_def) |
|
73 |
||
74 |
lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A" |
|
75 |
by (simp add: anchor_def) |
|
76 |
||
77 |
subsubsection{*request event*} |
|
78 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
79 |
definition reqm :: "agent => nat => nat => msg => agent => msg" where |
13508 | 80 |
"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I), |
81 |
cons (anchor A n B) nil|}" |
|
82 |
||
83 |
lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B') |
|
84 |
= (A=A' & r=r' & n=n' & I=I' & B=B')" |
|
85 |
by (auto simp: reqm_def) |
|
86 |
||
87 |
lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}" |
|
88 |
by (auto simp: reqm_def) |
|
89 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
90 |
definition req :: "agent => nat => nat => msg => agent => event" where |
13508 | 91 |
"req A r n I B == Says A B (reqm A r n I B)" |
92 |
||
93 |
lemma req_inj [iff]: "(req A r n I B = req A' r' n' I' B') |
|
94 |
= (A=A' & r=r' & n=n' & I=I' & B=B')" |
|
95 |
by (auto simp: req_def) |
|
96 |
||
97 |
subsubsection{*propose event*} |
|
98 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
99 |
definition prom :: "agent => nat => agent => nat => msg => msg => |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
100 |
msg => agent => msg" where |
13508 | 101 |
"prom B ofr A r I L J C == {|Agent A, Number r, |
102 |
app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}" |
|
103 |
||
104 |
lemma prom_inj [dest]: "prom B ofr A r I L J C = prom B' ofr' A' r' I' L' J' C' |
|
105 |
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" |
|
106 |
by (auto simp: prom_def) |
|
107 |
||
108 |
lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}" |
|
109 |
by (auto simp: prom_def) |
|
110 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
111 |
definition pro :: "agent => nat => agent => nat => msg => msg => |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
112 |
msg => agent => event" where |
13508 | 113 |
"pro B ofr A r I L J C == Says B C (prom B ofr A r I L J C)" |
114 |
||
115 |
lemma pro_inj [dest]: "pro B ofr A r I L J C = pro B' ofr' A' r' I' L' J' C' |
|
116 |
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" |
|
117 |
by (auto simp: pro_def dest: prom_inj) |
|
118 |
||
119 |
subsubsection{*protocol*} |
|
120 |
||
23746 | 121 |
inductive_set p2 :: "event list set" |
122 |
where |
|
13508 | 123 |
|
23746 | 124 |
Nil: "[]:p2" |
13508 | 125 |
|
23746 | 126 |
| Fake: "[| evsf:p2; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p2" |
13508 | 127 |
|
23746 | 128 |
| Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2" |
13508 | 129 |
|
23746 | 130 |
| Propose: "[| evsp:p2; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; |
131 |
I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); |
|
132 |
Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p2" |
|
13508 | 133 |
|
134 |
subsubsection{*valid offer lists*} |
|
135 |
||
23746 | 136 |
inductive_set |
137 |
valid :: "agent => nat => agent => msg set" |
|
138 |
for A :: agent and n :: nat and B :: agent |
|
139 |
where |
|
140 |
Request [intro]: "cons (anchor A n B) nil:valid A n B" |
|
13508 | 141 |
|
23746 | 142 |
| Propose [intro]: "L:valid A n B |
143 |
==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" |
|
13508 | 144 |
|
145 |
subsubsection{*basic properties of valid*} |
|
146 |
||
147 |
lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'" |
|
148 |
by (erule valid.cases, auto) |
|
149 |
||
150 |
lemma valid_pos_len: "L:valid A n B ==> 0 < len L" |
|
151 |
by (erule valid.induct, auto) |
|
152 |
||
153 |
subsubsection{*list of offers*} |
|
154 |
||
35418 | 155 |
fun offers :: "msg => msg" |
156 |
where |
|
157 |
"offers (cons M L) = cons {|shop M, nonce M|} (offers L)" |
|
158 |
| "offers other = nil" |
|
13508 | 159 |
|
160 |
||
161 |
subsection{*Properties of Protocol P2*} |
|
162 |
||
163 |
text{*same as @{text P1_Prop} except that publicly verifiable forward |
|
164 |
integrity is replaced by forward privacy*} |
|
165 |
||
166 |
subsection{*strong forward integrity: |
|
167 |
except the last one, no offer can be modified*} |
|
168 |
||
169 |
lemma strong_forward_integrity: "ALL L. Suc i < len L |
|
170 |
--> L:valid A n B --> repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)" |
|
171 |
apply (induct i) |
|
172 |
(* i = 0 *) |
|
173 |
apply clarify |
|
174 |
apply (frule len_not_empty, clarsimp) |
|
175 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 176 |
apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a) |
177 |
apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a) |
|
13508 | 178 |
apply (simp add: chain_def) |
179 |
(* i > 0 *) |
|
180 |
apply clarify |
|
181 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 182 |
apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na) |
13508 | 183 |
apply (frule len_not_empty, clarsimp) |
23746 | 184 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
13508 | 185 |
by (drule_tac x=l' in spec, simp, blast) |
186 |
||
187 |
subsection{*insertion resilience: |
|
188 |
except at the beginning, no offer can be inserted*} |
|
189 |
||
190 |
lemma chain_isnt_head [simp]: "L:valid A n B ==> |
|
191 |
head L ~= chain (next_shop (head L)) ofr A L C" |
|
192 |
by (erule valid.induct, auto simp: chain_def sign_def anchor_def) |
|
193 |
||
194 |
lemma insertion_resilience: "ALL L. L:valid A n B --> Suc i < len L |
|
195 |
--> ins (L,Suc i,M) ~:valid A n B" |
|
196 |
apply (induct i) |
|
197 |
(* i = 0 *) |
|
198 |
apply clarify |
|
199 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 200 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp) |
201 |
apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp) |
|
202 |
apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp) |
|
13508 | 203 |
(* i > 0 *) |
204 |
apply clarify |
|
205 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 206 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
13508 | 207 |
apply (frule len_not_empty, clarsimp) |
23746 | 208 |
apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na) |
13508 | 209 |
apply (frule len_not_empty, clarsimp) |
210 |
by (drule_tac x=l' in spec, clarsimp) |
|
211 |
||
212 |
subsection{*truncation resilience: |
|
213 |
only shop i can truncate at offer i*} |
|
214 |
||
215 |
lemma truncation_resilience: "ALL L. L:valid A n B --> Suc i < len L |
|
216 |
--> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))" |
|
217 |
apply (induct i) |
|
218 |
(* i = 0 *) |
|
219 |
apply clarify |
|
220 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 221 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
13508 | 222 |
apply (frule len_not_empty, clarsimp) |
23746 | 223 |
apply (ind_cases "{|M,l'|}:valid A n B" for l') |
13508 | 224 |
apply (frule len_not_empty, clarsimp, simp) |
225 |
(* i > 0 *) |
|
226 |
apply clarify |
|
227 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 228 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
13508 | 229 |
apply (frule len_not_empty, clarsimp) |
230 |
by (drule_tac x=l' in spec, clarsimp) |
|
231 |
||
232 |
subsection{*declarations for tactics*} |
|
233 |
||
234 |
declare knows_Spy_partsEs [elim] |
|
235 |
declare Fake_parts_insert [THEN subsetD, dest] |
|
236 |
declare initState.simps [simp del] |
|
237 |
||
238 |
subsection{*get components of a message*} |
|
239 |
||
240 |
lemma get_ML [dest]: "Says A' B {|A,R,I,M,L|}:set evs ==> |
|
241 |
M:parts (spies evs) & L:parts (spies evs)" |
|
242 |
by blast |
|
243 |
||
244 |
subsection{*general properties of p2*} |
|
245 |
||
246 |
lemma reqm_neq_prom [iff]: |
|
247 |
"reqm A r n I B ~= prom B' ofr A' r' I' (cons M L) J C" |
|
248 |
by (auto simp: reqm_def prom_def) |
|
249 |
||
250 |
lemma prom_neq_reqm [iff]: |
|
251 |
"prom B' ofr A' r' I' (cons M L) J C ~= reqm A r n I B" |
|
252 |
by (auto simp: reqm_def prom_def) |
|
253 |
||
254 |
lemma req_neq_pro [iff]: "req A r n I B ~= pro B' ofr A' r' I' (cons M L) J C" |
|
255 |
by (auto simp: req_def pro_def) |
|
256 |
||
257 |
lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C ~= req A r n I B" |
|
258 |
by (auto simp: req_def pro_def) |
|
259 |
||
260 |
lemma p2_has_no_Gets: "evs:p2 ==> ALL A X. Gets A X ~:set evs" |
|
261 |
by (erule p2.induct, auto simp: req_def pro_def) |
|
262 |
||
263 |
lemma p2_is_Gets_correct [iff]: "Gets_correct p2" |
|
264 |
by (auto simp: Gets_correct_def dest: p2_has_no_Gets) |
|
265 |
||
266 |
lemma p2_is_one_step [iff]: "one_step p2" |
|
23746 | 267 |
by (unfold one_step_def, clarify, ind_cases "ev#evs:p2" for ev evs, auto) |
13508 | 268 |
|
269 |
lemma p2_has_only_Says' [rule_format]: "evs:p2 ==> |
|
270 |
ev:set evs --> (EX A B X. ev=Says A B X)" |
|
271 |
by (erule p2.induct, auto simp: req_def pro_def) |
|
272 |
||
273 |
lemma p2_has_only_Says [iff]: "has_only_Says p2" |
|
274 |
by (auto simp: has_only_Says_def dest: p2_has_only_Says') |
|
275 |
||
276 |
lemma p2_is_regular [iff]: "regular p2" |
|
277 |
apply (simp only: regular_def, clarify) |
|
278 |
apply (erule_tac p2.induct) |
|
279 |
apply (simp_all add: initState.simps knows.simps pro_def prom_def |
|
280 |
req_def reqm_def anchor_def chain_def sign_def) |
|
281 |
by (auto dest: no_Key_in_agl no_Key_in_appdel parts_trans) |
|
282 |
||
283 |
subsection{*private keys are safe*} |
|
284 |
||
285 |
lemma priK_parts_Friend_imp_bad [rule_format,dest]: |
|
286 |
"[| evs:p2; Friend B ~= A |] |
|
287 |
==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)" |
|
288 |
apply (erule p2.induct) |
|
289 |
apply (simp_all add: initState.simps knows.simps pro_def prom_def |
|
17778 | 290 |
req_def reqm_def anchor_def chain_def sign_def) |
13508 | 291 |
apply (blast dest: no_Key_in_agl) |
292 |
apply (auto del: parts_invKey disjE dest: parts_trans |
|
293 |
simp add: no_Key_in_appdel) |
|
294 |
done |
|
295 |
||
296 |
lemma priK_analz_Friend_imp_bad [rule_format,dest]: |
|
297 |
"[| evs:p2; Friend B ~= A |] |
|
298 |
==> (Key (priK A):analz (knows (Friend B) evs)) --> (A:bad)" |
|
299 |
by auto |
|
300 |
||
301 |
lemma priK_notin_knows_max_Friend: |
|
302 |
"[| evs:p2; A ~:bad; A ~= Friend C |] |
|
303 |
==> Key (priK A) ~:analz (knows_max (Friend C) evs)" |
|
304 |
apply (rule not_parts_not_analz, simp add: knows_max_def, safe) |
|
305 |
apply (drule_tac H="spies' evs" in parts_sub) |
|
306 |
apply (rule_tac p=p2 in knows_max'_sub_spies', simp+) |
|
307 |
apply (drule_tac H="spies evs" in parts_sub) |
|
308 |
by (auto dest: knows'_sub_knows [THEN subsetD] priK_notin_initState_Friend) |
|
309 |
||
310 |
subsection{*general guardedness properties*} |
|
311 |
||
312 |
lemma agl_guard [intro]: "I:agl ==> I:guard n Ks" |
|
313 |
by (erule agl.induct, auto) |
|
314 |
||
315 |
lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs; |
|
316 |
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks" |
|
317 |
by (auto dest: Says_to_knows_max') |
|
318 |
||
319 |
lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs; |
|
320 |
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks" |
|
321 |
by (auto dest: Says_from_knows_max') |
|
322 |
||
323 |
lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs; |
|
324 |
Nonce n ~:used evs |] ==> L:guard n Ks" |
|
325 |
by (drule not_used_not_parts, auto) |
|
326 |
||
327 |
subsection{*guardedness of messages*} |
|
328 |
||
329 |
lemma chain_guard [iff]: "chain B ofr A L C:guard n {priK A}" |
|
330 |
by (case_tac "ofr=n", auto simp: chain_def sign_def) |
|
331 |
||
332 |
lemma chain_guard_Nonce_neq [intro]: "n ~= ofr |
|
333 |
==> chain B ofr A' L C:guard n {priK A}" |
|
334 |
by (auto simp: chain_def sign_def) |
|
335 |
||
336 |
lemma anchor_guard [iff]: "anchor A n' B:guard n {priK A}" |
|
337 |
by (case_tac "n'=n", auto simp: anchor_def) |
|
338 |
||
339 |
lemma anchor_guard_Nonce_neq [intro]: "n ~= n' |
|
340 |
==> anchor A' n' B:guard n {priK A}" |
|
341 |
by (auto simp: anchor_def) |
|
342 |
||
343 |
lemma reqm_guard [intro]: "I:agl ==> reqm A r n' I B:guard n {priK A}" |
|
344 |
by (case_tac "n'=n", auto simp: reqm_def) |
|
345 |
||
346 |
lemma reqm_guard_Nonce_neq [intro]: "[| n ~= n'; I:agl |] |
|
347 |
==> reqm A' r n' I B:guard n {priK A}" |
|
348 |
by (auto simp: reqm_def) |
|
349 |
||
350 |
lemma prom_guard [intro]: "[| I:agl; J:agl; L:guard n {priK A} |] |
|
351 |
==> prom B ofr A r I L J C:guard n {priK A}" |
|
352 |
by (auto simp: prom_def) |
|
353 |
||
354 |
lemma prom_guard_Nonce_neq [intro]: "[| n ~= ofr; I:agl; J:agl; |
|
355 |
L:guard n {priK A} |] ==> prom B ofr A' r I L J C:guard n {priK A}" |
|
356 |
by (auto simp: prom_def) |
|
357 |
||
358 |
subsection{*Nonce uniqueness*} |
|
359 |
||
360 |
lemma uniq_Nonce_in_chain [dest]: "Nonce k:parts {chain B ofr A L C} ==> k=ofr" |
|
361 |
by (auto simp: chain_def sign_def) |
|
362 |
||
363 |
lemma uniq_Nonce_in_anchor [dest]: "Nonce k:parts {anchor A n B} ==> k=n" |
|
364 |
by (auto simp: anchor_def chain_def sign_def) |
|
365 |
||
366 |
lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k:parts {reqm A r n I B}; |
|
367 |
I:agl |] ==> k=n" |
|
368 |
by (auto simp: reqm_def dest: no_Nonce_in_agl) |
|
369 |
||
370 |
lemma uniq_Nonce_in_prom [dest]: "[| Nonce k:parts {prom B ofr A r I L J C}; |
|
371 |
I:agl; J:agl; Nonce k ~:parts {L} |] ==> k=ofr" |
|
372 |
by (auto simp: prom_def dest: no_Nonce_in_agl no_Nonce_in_appdel) |
|
373 |
||
374 |
subsection{*requests are guarded*} |
|
375 |
||
376 |
lemma req_imp_Guard [rule_format]: "[| evs:p2; A ~:bad |] ==> |
|
377 |
req A r n I B:set evs --> Guard n {priK A} (spies evs)" |
|
378 |
apply (erule p2.induct, simp) |
|
379 |
apply (simp add: req_def knows.simps, safe) |
|
380 |
apply (erule in_synth_Guard, erule Guard_analz, simp) |
|
381 |
by (auto simp: req_def pro_def dest: Says_imp_knows_Spy) |
|
382 |
||
383 |
lemma req_imp_Guard_Friend: "[| evs:p2; A ~:bad; req A r n I B:set evs |] |
|
384 |
==> Guard n {priK A} (knows_max (Friend C) evs)" |
|
385 |
apply (rule Guard_knows_max') |
|
386 |
apply (rule_tac H="spies evs" in Guard_mono) |
|
387 |
apply (rule req_imp_Guard, simp+) |
|
388 |
apply (rule_tac B="spies' evs" in subset_trans) |
|
389 |
apply (rule_tac p=p2 in knows_max'_sub_spies', simp+) |
|
390 |
by (rule knows'_sub_knows) |
|
391 |
||
392 |
subsection{*propositions are guarded*} |
|
393 |
||
394 |
lemma pro_imp_Guard [rule_format]: "[| evs:p2; B ~:bad; A ~:bad |] ==> |
|
395 |
pro B ofr A r I (cons M L) J C:set evs --> Guard ofr {priK A} (spies evs)" |
|
396 |
apply (erule p2.induct) (* +3 subgoals *) |
|
397 |
(* Nil *) |
|
398 |
apply simp |
|
399 |
(* Fake *) |
|
400 |
apply (simp add: pro_def, safe) (* +4 subgoals *) |
|
401 |
(* 1 *) |
|
402 |
apply (erule in_synth_Guard, drule Guard_analz, simp, simp) |
|
403 |
(* 2 *) |
|
404 |
apply simp |
|
405 |
(* 3 *) |
|
406 |
apply (simp, simp add: req_def pro_def, blast) |
|
407 |
(* 4 *) |
|
408 |
apply (simp add: pro_def) |
|
409 |
apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard) |
|
410 |
(* 5 *) |
|
411 |
apply simp |
|
412 |
apply safe (* +1 subgoal *) |
|
413 |
apply (simp add: pro_def) |
|
414 |
apply (blast dest: prom_inj Says_Nonce_not_used_guard) |
|
415 |
(* 6 *) |
|
416 |
apply (simp add: pro_def) |
|
417 |
apply (blast dest: Says_imp_knows_Spy) |
|
418 |
(* Request *) |
|
419 |
apply (simp add: pro_def) |
|
420 |
apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard) |
|
421 |
(* Propose *) |
|
422 |
apply simp |
|
423 |
apply safe (* +1 subgoal *) |
|
424 |
(* 1 *) |
|
425 |
apply (simp add: pro_def) |
|
426 |
apply (blast dest: prom_inj Says_Nonce_not_used_guard) |
|
427 |
(* 2 *) |
|
428 |
apply (simp add: pro_def) |
|
429 |
by (blast dest: Says_imp_knows_Spy) |
|
430 |
||
431 |
lemma pro_imp_Guard_Friend: "[| evs:p2; B ~:bad; A ~:bad; |
|
432 |
pro B ofr A r I (cons M L) J C:set evs |] |
|
433 |
==> Guard ofr {priK A} (knows_max (Friend D) evs)" |
|
434 |
apply (rule Guard_knows_max') |
|
435 |
apply (rule_tac H="spies evs" in Guard_mono) |
|
436 |
apply (rule pro_imp_Guard, simp+) |
|
437 |
apply (rule_tac B="spies' evs" in subset_trans) |
|
438 |
apply (rule_tac p=p2 in knows_max'_sub_spies', simp+) |
|
439 |
by (rule knows'_sub_knows) |
|
440 |
||
441 |
subsection{*data confidentiality: |
|
442 |
no one other than the originator can decrypt the offers*} |
|
443 |
||
444 |
lemma Nonce_req_notin_spies: "[| evs:p2; req A r n I B:set evs; A ~:bad |] |
|
445 |
==> Nonce n ~:analz (spies evs)" |
|
446 |
by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) |
|
447 |
||
448 |
lemma Nonce_req_notin_knows_max_Friend: "[| evs:p2; req A r n I B:set evs; |
|
449 |
A ~:bad; A ~= Friend C |] ==> Nonce n ~:analz (knows_max (Friend C) evs)" |
|
450 |
apply (clarify, frule_tac C=C in req_imp_Guard_Friend, simp+) |
|
451 |
apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+) |
|
452 |
by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def) |
|
453 |
||
454 |
lemma Nonce_pro_notin_spies: "[| evs:p2; B ~:bad; A ~:bad; |
|
455 |
pro B ofr A r I (cons M L) J C:set evs |] ==> Nonce ofr ~:analz (spies evs)" |
|
456 |
by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) |
|
457 |
||
458 |
lemma Nonce_pro_notin_knows_max_Friend: "[| evs:p2; B ~:bad; A ~:bad; |
|
459 |
A ~= Friend D; pro B ofr A r I (cons M L) J C:set evs |] |
|
460 |
==> Nonce ofr ~:analz (knows_max (Friend D) evs)" |
|
461 |
apply (clarify, frule_tac A=A in pro_imp_Guard_Friend, simp+) |
|
462 |
apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+) |
|
463 |
by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def) |
|
464 |
||
465 |
subsection{*forward privacy: |
|
466 |
only the originator can know the identity of the shops*} |
|
467 |
||
468 |
lemma forward_privacy_Spy: "[| evs:p2; B ~:bad; A ~:bad; |
|
469 |
pro B ofr A r I (cons M L) J C:set evs |] |
|
470 |
==> sign B (Nonce ofr) ~:analz (spies evs)" |
|
471 |
by (auto simp:sign_def dest: Nonce_pro_notin_spies) |
|
472 |
||
473 |
lemma forward_privacy_Friend: "[| evs:p2; B ~:bad; A ~:bad; A ~= Friend D; |
|
474 |
pro B ofr A r I (cons M L) J C:set evs |] |
|
475 |
==> sign B (Nonce ofr) ~:analz (knows_max (Friend D) evs)" |
|
476 |
by (auto simp:sign_def dest:Nonce_pro_notin_knows_max_Friend ) |
|
477 |
||
478 |
subsection{*non repudiability: an offer signed by B has been sent by B*} |
|
479 |
||
480 |
lemma Crypt_reqm: "[| Crypt (priK A) X:parts {reqm A' r n I B}; I:agl |] ==> A=A'" |
|
481 |
by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl) |
|
482 |
||
483 |
lemma Crypt_prom: "[| Crypt (priK A) X:parts {prom B ofr A' r I L J C}; |
|
484 |
I:agl; J:agl |] ==> A=B | Crypt (priK A) X:parts {L}" |
|
485 |
apply (simp add: prom_def anchor_def chain_def sign_def) |
|
486 |
by (blast dest: no_Crypt_in_agl no_Crypt_in_appdel) |
|
487 |
||
488 |
lemma Crypt_safeness: "[| evs:p2; A ~:bad |] ==> Crypt (priK A) X:parts (spies evs) |
|
489 |
--> (EX B Y. Says A B Y:set evs & Crypt (priK A) X:parts {Y})" |
|
490 |
apply (erule p2.induct) |
|
491 |
(* Nil *) |
|
492 |
apply simp |
|
493 |
(* Fake *) |
|
494 |
apply clarsimp |
|
495 |
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) |
|
496 |
apply (erule disjE) |
|
497 |
apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast) |
|
498 |
(* Request *) |
|
499 |
apply (simp add: req_def, clarify) |
|
500 |
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) |
|
501 |
apply (erule disjE) |
|
502 |
apply (frule Crypt_reqm, simp, clarify) |
|
503 |
apply (rule_tac x=B in exI, rule_tac x="reqm A r n I B" in exI, simp, blast) |
|
504 |
(* Propose *) |
|
505 |
apply (simp add: pro_def, clarify) |
|
506 |
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) |
|
507 |
apply (rotate_tac -1, erule disjE) |
|
508 |
apply (frule Crypt_prom, simp, simp) |
|
509 |
apply (rotate_tac -1, erule disjE) |
|
510 |
apply (rule_tac x=C in exI) |
|
511 |
apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI, blast) |
|
512 |
apply (subgoal_tac "cons M L:parts (spies evsp)") |
|
513 |
apply (drule_tac G="{cons M L}" and H="spies evsp" in parts_trans, blast, blast) |
|
514 |
apply (drule Says_imp_spies, rotate_tac -1, drule parts.Inj) |
|
515 |
apply (drule parts.Snd, drule parts.Snd, drule parts.Snd) |
|
516 |
by auto |
|
517 |
||
518 |
lemma Crypt_Hash_imp_sign: "[| evs:p2; A ~:bad |] ==> |
|
519 |
Crypt (priK A) (Hash X):parts (spies evs) |
|
520 |
--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})" |
|
521 |
apply (erule p2.induct) |
|
522 |
(* Nil *) |
|
523 |
apply simp |
|
524 |
(* Fake *) |
|
525 |
apply clarsimp |
|
526 |
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) |
|
527 |
apply simp |
|
528 |
apply (erule disjE) |
|
529 |
apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast) |
|
530 |
(* Request *) |
|
531 |
apply (simp add: req_def, clarify) |
|
532 |
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) |
|
533 |
apply simp |
|
534 |
apply (erule disjE) |
|
535 |
apply (frule Crypt_reqm, simp+) |
|
536 |
apply (rule_tac x=B in exI, rule_tac x="reqm Aa r n I B" in exI) |
|
537 |
apply (simp add: reqm_def sign_def anchor_def no_Crypt_in_agl) |
|
538 |
apply (simp add: chain_def sign_def, blast) |
|
539 |
(* Propose *) |
|
540 |
apply (simp add: pro_def, clarify) |
|
541 |
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) |
|
542 |
apply simp |
|
543 |
apply (rotate_tac -1, erule disjE) |
|
544 |
apply (simp add: prom_def sign_def no_Crypt_in_agl no_Crypt_in_appdel) |
|
545 |
apply (simp add: chain_def sign_def) |
|
546 |
apply (rotate_tac -1, erule disjE) |
|
547 |
apply (rule_tac x=C in exI) |
|
548 |
apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI) |
|
549 |
apply (simp add: prom_def chain_def sign_def) |
|
550 |
apply (erule impE) |
|
551 |
apply (blast dest: get_ML parts_sub) |
|
552 |
apply (blast del: MPair_parts)+ |
|
553 |
done |
|
554 |
||
555 |
lemma sign_safeness: "[| evs:p2; A ~:bad |] ==> sign A X:parts (spies evs) |
|
556 |
--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})" |
|
557 |
apply (clarify, simp add: sign_def, frule parts.Snd) |
|
558 |
apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def]) |
|
559 |
done |
|
560 |
||
561 |
end |