src/HOL/Auth/Guard/P2.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/Auth/Guard/P2.thy
     2     Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     3     Copyright   2002  University of Cambridge
     4 
     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 *)
     9 
    10 section{*Protocol P2*}
    11 
    12 theory P2 imports Guard_Public List_Msg begin
    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 
    23 definition chain :: "agent => nat => agent => msg => agent => msg" where
    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 
    40 fun shop :: "msg => msg" where
    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 
    48 fun nonce :: "msg => msg" where
    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 
    56 fun next_shop :: "msg => agent" where
    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 
    64 definition anchor :: "agent => nat => agent => msg" where
    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 
    79 definition reqm :: "agent => nat => nat => msg => agent => msg" where
    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 
    90 definition req :: "agent => nat => nat => msg => agent => event" where
    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 
    99 definition prom :: "agent => nat => agent => nat => msg => msg =>
   100 msg => agent => msg" where
   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 
   111 definition pro :: "agent => nat => agent => nat => msg => msg =>
   112                   msg => agent => event" where
   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 
   121 inductive_set p2 :: "event list set"
   122 where
   123 
   124   Nil: "[]:p2"
   125 
   126 | Fake: "[| evsf:p2; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p2"
   127 
   128 | Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2"
   129 
   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"
   133 
   134 subsubsection{*valid offer lists*}
   135 
   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"
   141 
   142 | Propose [intro]: "L:valid A n B
   143   ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B"
   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 
   155 fun offers :: "msg => msg"
   156 where
   157   "offers (cons M L) = cons {|shop M, nonce M|} (offers L)"
   158 | "offers other = nil"
   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)
   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)
   178 apply (simp add: chain_def)
   179 (* i > 0 *)
   180 apply clarify
   181 apply (frule len_not_empty, clarsimp)
   182 apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na)
   183 apply (frule len_not_empty, clarsimp)
   184 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
   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)
   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)
   203 (* i > 0 *)
   204 apply clarify
   205 apply (frule len_not_empty, clarsimp)
   206 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
   207 apply (frule len_not_empty, clarsimp)
   208 apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na)
   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)
   221 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
   222 apply (frule len_not_empty, clarsimp)
   223 apply (ind_cases "{|M,l'|}:valid A n B" for l')
   224 apply (frule len_not_empty, clarsimp, simp)
   225 (* i > 0 *)
   226 apply clarify
   227 apply (frule len_not_empty, clarsimp)
   228 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
   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"
   267 by (unfold one_step_def, clarify, ind_cases "ev#evs:p2" for ev evs, auto)
   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
   290                 req_def reqm_def anchor_def chain_def sign_def) 
   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