1 (******************************************************************************
2 from G. Karjoth, N. Asokan and C. Gulcu
3 "Protecting the computation results of free-roaming agents"
4 Mobiles Agents 1998, LNCS 1477
7 author: Frederic Blanqui
9 webpage: http://www.lri.fr/~blanqui/
11 University of Cambridge, Computer Laboratory
12 William Gates Building, JJ Thomson Avenue
13 Cambridge CB3 0FD, United Kingdom
14 ******************************************************************************)
18 theory P1 imports "../Public" Guard_Public List_Msg begin
20 subsection{*Protocol Definition*}
22 (******************************************************************************
24 the contents of the messages are not completely specified in the paper
25 we assume that the user sends his request and his itinerary in the clear
27 we will adopt the following format for messages: {|A,r,I,L|}
30 I: next shops (agent list)
31 L: collected offers (offer list)
33 in the paper, the authors use nonces r_i to add redundancy in the offer
34 in order to make it safer against dictionary attacks
35 it is not necessary in our modelization since crypto is assumed to be strong
37 ******************************************************************************)
39 subsubsection{*offer chaining:
40 B chains his offer for A with the head offer of L for sending it to C*}
42 definition chain :: "agent => nat => agent => msg => agent => msg" where
44 let m1= Crypt (pubK A) (Nonce ofr) in
45 let m2= Hash {|head L, Agent C|} in
48 declare Let_def [simp]
50 lemma chain_inj [iff]: "(chain B ofr A L C = chain B' ofr' A' L' C')
51 = (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')"
52 by (auto simp: chain_def Let_def)
54 lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}"
55 by (auto simp: chain_def sign_def)
57 subsubsection{*agent whose key is used to sign an offer*}
59 fun shop :: "msg => msg" where
60 "shop {|B,X,Crypt K H|} = Agent (agt K)"
62 lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
63 by (simp add: chain_def sign_def)
65 subsubsection{*nonce used in an offer*}
67 fun nonce :: "msg => msg" where
68 "nonce {|B,{|Crypt K ofr,m2|},CryptH|} = ofr"
70 lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
71 by (simp add: chain_def sign_def)
73 subsubsection{*next shop*}
75 fun next_shop :: "msg => agent" where
76 "next_shop {|B,{|m1,Hash{|headL,Agent C|}|},CryptH|} = C"
78 lemma next_shop_chain [iff]: "next_shop (chain B ofr A L C) = C"
79 by (simp add: chain_def sign_def)
81 subsubsection{*anchor of the offer list*}
83 definition anchor :: "agent => nat => agent => msg" where
84 "anchor A n B == chain A n A (cons nil nil) B"
86 lemma anchor_inj [iff]: "(anchor A n B = anchor A' n' B')
87 = (A=A' & n=n' & B=B')"
88 by (auto simp: anchor_def)
90 lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}"
91 by (auto simp: anchor_def)
93 lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A"
94 by (simp add: anchor_def)
96 lemma nonce_anchor [simp]: "nonce (anchor A n B) = Nonce n"
97 by (simp add: anchor_def)
99 lemma next_shop_anchor [iff]: "next_shop (anchor A n B) = B"
100 by (simp add: anchor_def)
102 subsubsection{*request event*}
104 definition reqm :: "agent => nat => nat => msg => agent => msg" where
105 "reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I),
106 cons (anchor A n B) nil|}"
108 lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B')
109 = (A=A' & r=r' & n=n' & I=I' & B=B')"
110 by (auto simp: reqm_def)
112 lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}"
113 by (auto simp: reqm_def)
115 definition req :: "agent => nat => nat => msg => agent => event" where
116 "req A r n I B == Says A B (reqm A r n I B)"
118 lemma req_inj [iff]: "(req A r n I B = req A' r' n' I' B')
119 = (A=A' & r=r' & n=n' & I=I' & B=B')"
120 by (auto simp: req_def)
122 subsubsection{*propose event*}
124 definition prom :: "agent => nat => agent => nat => msg => msg =>
125 msg => agent => msg" where
126 "prom B ofr A r I L J C == {|Agent A, Number r,
127 app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}"
129 lemma prom_inj [dest]: "prom B ofr A r I L J C
130 = prom B' ofr' A' r' I' L' J' C'
131 ==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
132 by (auto simp: prom_def)
134 lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}"
135 by (auto simp: prom_def)
137 definition pro :: "agent => nat => agent => nat => msg => msg =>
138 msg => agent => event" where
139 "pro B ofr A r I L J C == Says B C (prom B ofr A r I L J C)"
141 lemma pro_inj [dest]: "pro B ofr A r I L J C = pro B' ofr' A' r' I' L' J' C'
142 ==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
143 by (auto simp: pro_def dest: prom_inj)
145 subsubsection{*protocol*}
147 inductive_set p1 :: "event list set"
152 | Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1"
154 | Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1"
156 | Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp;
157 I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
158 Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1"
160 subsubsection{*Composition of Traces*}
163 evs:p1 & (ALL n. Nonce n:used evs' --> Nonce n ~:used evs) -->
165 apply (erule p1.induct, safe)
166 apply (simp_all add: used_ConsI)
167 apply (erule p1.Fake, erule synth_sub, rule analz_mono, rule knows_sub_app)
168 apply (erule p1.Request, safe, simp_all add: req_def, force)
169 apply (erule_tac A'=A' in p1.Propose, simp_all)
170 apply (drule_tac x=ofr in spec, simp add: pro_def, blast)
171 apply (erule_tac A'=A' in p1.Propose, auto simp: pro_def)
174 subsubsection{*Valid Offer Lists*}
177 valid :: "agent => nat => agent => msg set"
178 for A :: agent and n :: nat and B :: agent
180 Request [intro]: "cons (anchor A n B) nil:valid A n B"
182 | Propose [intro]: "L:valid A n B
183 ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B"
185 subsubsection{*basic properties of valid*}
187 lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'"
188 by (erule valid.cases, auto)
190 lemma valid_pos_len: "L:valid A n B ==> 0 < len L"
191 by (erule valid.induct, auto)
193 subsubsection{*offers of an offer list*}
195 definition offer_nonces :: "msg => msg set" where
196 "offer_nonces L == {X. X:parts {L} & (EX n. X = Nonce n)}"
198 subsubsection{*the originator can get the offers*}
200 lemma "L:valid A n B ==> offer_nonces L <= analz (insert L (initState A))"
201 by (erule valid.induct, auto simp: anchor_def chain_def sign_def
202 offer_nonces_def initState.simps)
204 subsubsection{*list of offers*}
206 fun offers :: "msg => msg" where
207 "offers (cons M L) = cons {|shop M, nonce M|} (offers L)" |
210 subsubsection{*list of agents whose keys are used to sign a list of offers*}
212 fun shops :: "msg => msg" where
213 "shops (cons M L) = cons (shop M) (shops L)" |
214 "shops other = other"
216 lemma shops_in_agl: "L:valid A n B ==> shops L:agl"
217 by (erule valid.induct, auto simp: anchor_def chain_def sign_def)
219 subsubsection{*builds a trace from an itinerary*}
221 fun offer_list :: "agent * nat * agent * msg * nat => msg" where
222 "offer_list (A,n,B,nil,ofr) = cons (anchor A n B) nil" |
223 "offer_list (A,n,B,cons (Agent C) I,ofr) = (
224 let L = offer_list (A,n,B,I,Suc ofr) in
225 cons (chain (next_shop (head L)) ofr A L C) L)"
227 lemma "I:agl ==> ALL ofr. offer_list (A,n,B,I,ofr):valid A n B"
228 by (erule agl.induct, auto)
230 fun trace :: "agent * nat * agent * nat * msg * msg * msg
232 "trace (B,ofr,A,r,I,L,nil) = []" |
233 "trace (B,ofr,A,r,I,L,cons (Agent D) K) = (
234 let C = (if K=nil then B else agt_nb (head K)) in
235 let I' = (if K=nil then cons (Agent A) (cons (Agent B) I)
236 else cons (Agent A) (app (I, cons (head K) nil))) in
237 let I'' = app (I, cons (head K) nil) in
238 pro C (Suc ofr) A r I' L nil D
239 # trace (B,Suc ofr,A,r,I'',tail L,K))"
241 definition trace' :: "agent => nat => nat => msg => agent => nat => event list" where
242 "trace' A r n I B ofr == (
243 let AI = cons (Agent A) I in
244 let L = offer_list (A,n,B,AI,ofr) in
245 trace (B,ofr,A,r,nil,L,AI))"
247 declare trace'_def [simp]
249 subsubsection{*there is a trace in which the originator receives a valid answer*}
251 lemma p1_not_empty: "evs:p1 ==> req A r n I B:set evs -->
252 (EX evs'. evs'@evs:p1 & pro B' ofr A r I' L J A:set evs' & L:valid A n B)"
256 subsection{*properties of protocol P1*}
258 text{*publicly verifiable forward integrity:
259 anyone can verify the validity of an offer list*}
261 subsubsection{*strong forward integrity:
262 except the last one, no offer can be modified*}
264 lemma strong_forward_integrity: "ALL L. Suc i < len L
265 --> L:valid A n B & repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)"
269 apply (frule len_not_empty, clarsimp)
270 apply (frule len_not_empty, clarsimp)
271 apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a)
272 apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a)
273 apply (simp add: chain_def)
276 apply (frule len_not_empty, clarsimp)
277 apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na)
278 apply (frule len_not_empty, clarsimp)
279 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
280 by (drule_tac x=l' in spec, simp, blast)
282 subsubsection{*insertion resilience:
283 except at the beginning, no offer can be inserted*}
285 lemma chain_isnt_head [simp]: "L:valid A n B ==>
286 head L ~= chain (next_shop (head L)) ofr A L C"
287 by (erule valid.induct, auto simp: chain_def sign_def anchor_def)
289 lemma insertion_resilience: "ALL L. L:valid A n B --> Suc i < len L
290 --> ins (L,Suc i,M) ~:valid A n B"
294 apply (frule len_not_empty, clarsimp)
295 apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp)
296 apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp)
297 apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp)
300 apply (frule len_not_empty, clarsimp)
301 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
302 apply (frule len_not_empty, clarsimp)
303 apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na)
304 apply (frule len_not_empty, clarsimp)
305 by (drule_tac x=l' in spec, clarsimp)
307 subsubsection{*truncation resilience:
308 only shop i can truncate at offer i*}
310 lemma truncation_resilience: "ALL L. L:valid A n B --> Suc i < len L
311 --> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))"
315 apply (frule len_not_empty, clarsimp)
316 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
317 apply (frule len_not_empty, clarsimp)
318 apply (ind_cases "{|M,l'|}:valid A n B" for l')
319 apply (frule len_not_empty, clarsimp, simp)
322 apply (frule len_not_empty, clarsimp)
323 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
324 apply (frule len_not_empty, clarsimp)
325 by (drule_tac x=l' in spec, clarsimp)
327 subsubsection{*declarations for tactics*}
329 declare knows_Spy_partsEs [elim]
330 declare Fake_parts_insert [THEN subsetD, dest]
331 declare initState.simps [simp del]
333 subsubsection{*get components of a message*}
335 lemma get_ML [dest]: "Says A' B {|A,r,I,M,L|}:set evs ==>
336 M:parts (spies evs) & L:parts (spies evs)"
339 subsubsection{*general properties of p1*}
341 lemma reqm_neq_prom [iff]:
342 "reqm A r n I B ~= prom B' ofr A' r' I' (cons M L) J C"
343 by (auto simp: reqm_def prom_def)
345 lemma prom_neq_reqm [iff]:
346 "prom B' ofr A' r' I' (cons M L) J C ~= reqm A r n I B"
347 by (auto simp: reqm_def prom_def)
349 lemma req_neq_pro [iff]: "req A r n I B ~= pro B' ofr A' r' I' (cons M L) J C"
350 by (auto simp: req_def pro_def)
352 lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C ~= req A r n I B"
353 by (auto simp: req_def pro_def)
355 lemma p1_has_no_Gets: "evs:p1 ==> ALL A X. Gets A X ~:set evs"
356 by (erule p1.induct, auto simp: req_def pro_def)
358 lemma p1_is_Gets_correct [iff]: "Gets_correct p1"
359 by (auto simp: Gets_correct_def dest: p1_has_no_Gets)
361 lemma p1_is_one_step [iff]: "one_step p1"
362 by (unfold one_step_def, clarify, ind_cases "ev#evs:p1" for ev evs, auto)
364 lemma p1_has_only_Says' [rule_format]: "evs:p1 ==>
365 ev:set evs --> (EX A B X. ev=Says A B X)"
366 by (erule p1.induct, auto simp: req_def pro_def)
368 lemma p1_has_only_Says [iff]: "has_only_Says p1"
369 by (auto simp: has_only_Says_def dest: p1_has_only_Says')
371 lemma p1_is_regular [iff]: "regular p1"
372 apply (simp only: regular_def, clarify)
373 apply (erule_tac p1.induct)
374 apply (simp_all add: initState.simps knows.simps pro_def prom_def
375 req_def reqm_def anchor_def chain_def sign_def)
376 by (auto dest: no_Key_in_agl no_Key_in_appdel parts_trans)
378 subsubsection{*private keys are safe*}
380 lemma priK_parts_Friend_imp_bad [rule_format,dest]:
381 "[| evs:p1; Friend B ~= A |]
382 ==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
383 apply (erule p1.induct)
384 apply (simp_all add: initState.simps knows.simps pro_def prom_def
385 req_def reqm_def anchor_def chain_def sign_def)
386 apply (blast dest: no_Key_in_agl)
387 apply (auto del: parts_invKey disjE dest: parts_trans
388 simp add: no_Key_in_appdel)
391 lemma priK_analz_Friend_imp_bad [rule_format,dest]:
392 "[| evs:p1; Friend B ~= A |]
393 ==> (Key (priK A):analz (knows (Friend B) evs)) --> (A:bad)"
396 lemma priK_notin_knows_max_Friend: "[| evs:p1; A ~:bad; A ~= Friend C |]
397 ==> Key (priK A) ~:analz (knows_max (Friend C) evs)"
398 apply (rule not_parts_not_analz, simp add: knows_max_def, safe)
399 apply (drule_tac H="spies' evs" in parts_sub)
400 apply (rule_tac p=p1 in knows_max'_sub_spies', simp+)
401 apply (drule_tac H="spies evs" in parts_sub)
402 by (auto dest: knows'_sub_knows [THEN subsetD] priK_notin_initState_Friend)
404 subsubsection{*general guardedness properties*}
406 lemma agl_guard [intro]: "I:agl ==> I:guard n Ks"
407 by (erule agl.induct, auto)
409 lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs;
410 Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
411 by (auto dest: Says_to_knows_max')
413 lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs;
414 Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
415 by (auto dest: Says_from_knows_max')
417 lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs;
418 Nonce n ~:used evs |] ==> L:guard n Ks"
419 by (drule not_used_not_parts, auto)
421 subsubsection{*guardedness of messages*}
423 lemma chain_guard [iff]: "chain B ofr A L C:guard n {priK A}"
424 by (case_tac "ofr=n", auto simp: chain_def sign_def)
426 lemma chain_guard_Nonce_neq [intro]: "n ~= ofr
427 ==> chain B ofr A' L C:guard n {priK A}"
428 by (auto simp: chain_def sign_def)
430 lemma anchor_guard [iff]: "anchor A n' B:guard n {priK A}"
431 by (case_tac "n'=n", auto simp: anchor_def)
433 lemma anchor_guard_Nonce_neq [intro]: "n ~= n'
434 ==> anchor A' n' B:guard n {priK A}"
435 by (auto simp: anchor_def)
437 lemma reqm_guard [intro]: "I:agl ==> reqm A r n' I B:guard n {priK A}"
438 by (case_tac "n'=n", auto simp: reqm_def)
440 lemma reqm_guard_Nonce_neq [intro]: "[| n ~= n'; I:agl |]
441 ==> reqm A' r n' I B:guard n {priK A}"
442 by (auto simp: reqm_def)
444 lemma prom_guard [intro]: "[| I:agl; J:agl; L:guard n {priK A} |]
445 ==> prom B ofr A r I L J C:guard n {priK A}"
446 by (auto simp: prom_def)
448 lemma prom_guard_Nonce_neq [intro]: "[| n ~= ofr; I:agl; J:agl;
449 L:guard n {priK A} |] ==> prom B ofr A' r I L J C:guard n {priK A}"
450 by (auto simp: prom_def)
452 subsubsection{*Nonce uniqueness*}
454 lemma uniq_Nonce_in_chain [dest]: "Nonce k:parts {chain B ofr A L C} ==> k=ofr"
455 by (auto simp: chain_def sign_def)
457 lemma uniq_Nonce_in_anchor [dest]: "Nonce k:parts {anchor A n B} ==> k=n"
458 by (auto simp: anchor_def chain_def sign_def)
460 lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k:parts {reqm A r n I B};
462 by (auto simp: reqm_def dest: no_Nonce_in_agl)
464 lemma uniq_Nonce_in_prom [dest]: "[| Nonce k:parts {prom B ofr A r I L J C};
465 I:agl; J:agl; Nonce k ~:parts {L} |] ==> k=ofr"
466 by (auto simp: prom_def dest: no_Nonce_in_agl no_Nonce_in_appdel)
468 subsubsection{*requests are guarded*}
470 lemma req_imp_Guard [rule_format]: "[| evs:p1; A ~:bad |] ==>
471 req A r n I B:set evs --> Guard n {priK A} (spies evs)"
472 apply (erule p1.induct, simp)
473 apply (simp add: req_def knows.simps, safe)
474 apply (erule in_synth_Guard, erule Guard_analz, simp)
475 by (auto simp: req_def pro_def dest: Says_imp_knows_Spy)
477 lemma req_imp_Guard_Friend: "[| evs:p1; A ~:bad; req A r n I B:set evs |]
478 ==> Guard n {priK A} (knows_max (Friend C) evs)"
479 apply (rule Guard_knows_max')
480 apply (rule_tac H="spies evs" in Guard_mono)
481 apply (rule req_imp_Guard, simp+)
482 apply (rule_tac B="spies' evs" in subset_trans)
483 apply (rule_tac p=p1 in knows_max'_sub_spies', simp+)
484 by (rule knows'_sub_knows)
486 subsubsection{*propositions are guarded*}
488 lemma pro_imp_Guard [rule_format]: "[| evs:p1; B ~:bad; A ~:bad |] ==>
489 pro B ofr A r I (cons M L) J C:set evs --> Guard ofr {priK A} (spies evs)"
490 apply (erule p1.induct) (* +3 subgoals *)
494 apply (simp add: pro_def, safe) (* +4 subgoals *)
496 apply (erule in_synth_Guard, drule Guard_analz, simp, simp)
500 apply (simp, simp add: req_def pro_def, blast)
502 apply (simp add: pro_def)
503 apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard)
506 apply safe (* +1 subgoal *)
507 apply (simp add: pro_def)
508 apply (blast dest: prom_inj Says_Nonce_not_used_guard)
510 apply (simp add: pro_def)
511 apply (blast dest: Says_imp_knows_Spy)
513 apply (simp add: pro_def)
514 apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard)
517 apply safe (* +1 subgoal *)
519 apply (simp add: pro_def)
520 apply (blast dest: prom_inj Says_Nonce_not_used_guard)
522 apply (simp add: pro_def)
523 by (blast dest: Says_imp_knows_Spy)
525 lemma pro_imp_Guard_Friend: "[| evs:p1; B ~:bad; A ~:bad;
526 pro B ofr A r I (cons M L) J C:set evs |]
527 ==> Guard ofr {priK A} (knows_max (Friend D) evs)"
528 apply (rule Guard_knows_max')
529 apply (rule_tac H="spies evs" in Guard_mono)
530 apply (rule pro_imp_Guard, simp+)
531 apply (rule_tac B="spies' evs" in subset_trans)
532 apply (rule_tac p=p1 in knows_max'_sub_spies', simp+)
533 by (rule knows'_sub_knows)
535 subsubsection{*data confidentiality:
536 no one other than the originator can decrypt the offers*}
538 lemma Nonce_req_notin_spies: "[| evs:p1; req A r n I B:set evs; A ~:bad |]
539 ==> Nonce n ~:analz (spies evs)"
540 by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+)
542 lemma Nonce_req_notin_knows_max_Friend: "[| evs:p1; req A r n I B:set evs;
543 A ~:bad; A ~= Friend C |] ==> Nonce n ~:analz (knows_max (Friend C) evs)"
544 apply (clarify, frule_tac C=C in req_imp_Guard_Friend, simp+)
545 apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+)
546 by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def)
548 lemma Nonce_pro_notin_spies: "[| evs:p1; B ~:bad; A ~:bad;
549 pro B ofr A r I (cons M L) J C:set evs |] ==> Nonce ofr ~:analz (spies evs)"
550 by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+)
552 lemma Nonce_pro_notin_knows_max_Friend: "[| evs:p1; B ~:bad; A ~:bad;
553 A ~= Friend D; pro B ofr A r I (cons M L) J C:set evs |]
554 ==> Nonce ofr ~:analz (knows_max (Friend D) evs)"
555 apply (clarify, frule_tac A=A in pro_imp_Guard_Friend, simp+)
556 apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+)
557 by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def)
559 subsubsection{*non repudiability:
560 an offer signed by B has been sent by B*}
562 lemma Crypt_reqm: "[| Crypt (priK A) X:parts {reqm A' r n I B}; I:agl |] ==> A=A'"
563 by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl)
565 lemma Crypt_prom: "[| Crypt (priK A) X:parts {prom B ofr A' r I L J C};
566 I:agl; J:agl |] ==> A=B | Crypt (priK A) X:parts {L}"
567 apply (simp add: prom_def anchor_def chain_def sign_def)
568 by (blast dest: no_Crypt_in_agl no_Crypt_in_appdel)
570 lemma Crypt_safeness: "[| evs:p1; A ~:bad |] ==> Crypt (priK A) X:parts (spies evs)
571 --> (EX B Y. Says A B Y:set evs & Crypt (priK A) X:parts {Y})"
572 apply (erule p1.induct)
577 apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
579 apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast)
581 apply (simp add: req_def, clarify)
582 apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
584 apply (frule Crypt_reqm, simp, clarify)
585 apply (rule_tac x=B in exI, rule_tac x="reqm A r n I B" in exI, simp, blast)
587 apply (simp add: pro_def, clarify)
588 apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
589 apply (rotate_tac -1, erule disjE)
590 apply (frule Crypt_prom, simp, simp)
591 apply (rotate_tac -1, erule disjE)
592 apply (rule_tac x=C in exI)
593 apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI, blast)
594 apply (subgoal_tac "cons M L:parts (spies evsp)")
595 apply (drule_tac G="{cons M L}" and H="spies evsp" in parts_trans, blast, blast)
596 apply (drule Says_imp_spies, rotate_tac -1, drule parts.Inj)
597 apply (drule parts.Snd, drule parts.Snd, drule parts.Snd)
600 lemma Crypt_Hash_imp_sign: "[| evs:p1; A ~:bad |] ==>
601 Crypt (priK A) (Hash X):parts (spies evs)
602 --> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})"
603 apply (erule p1.induct)
608 apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
611 apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast)
613 apply (simp add: req_def, clarify)
614 apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
617 apply (frule Crypt_reqm, simp+)
618 apply (rule_tac x=B in exI, rule_tac x="reqm Aa r n I B" in exI)
619 apply (simp add: reqm_def sign_def anchor_def no_Crypt_in_agl)
620 apply (simp add: chain_def sign_def, blast)
622 apply (simp add: pro_def, clarify)
623 apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
625 apply (rotate_tac -1, erule disjE)
626 apply (simp add: prom_def sign_def no_Crypt_in_agl no_Crypt_in_appdel)
627 apply (simp add: chain_def sign_def)
628 apply (rotate_tac -1, erule disjE)
629 apply (rule_tac x=C in exI)
630 apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI)
631 apply (simp add: prom_def chain_def sign_def)
633 apply (blast dest: get_ML parts_sub)
634 apply (blast del: MPair_parts)+
637 lemma sign_safeness: "[| evs:p1; A ~:bad |] ==> sign A X:parts (spies evs)
638 --> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})"
639 apply (clarify, simp add: sign_def, frule parts.Snd)
640 apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def])