src/HOL/Auth/Guard/P1.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/P1.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 P1*}
    11 
    12 theory P1 imports "../Public" Guard_Public List_Msg begin
    13 
    14 subsection{*Protocol Definition*}
    15 
    16 (******************************************************************************
    17 
    18 the contents of the messages are not completely specified in the paper
    19 we assume that the user sends his request and his itinerary in the clear
    20 
    21 we will adopt the following format for messages: {|A,r,I,L|}
    22 A: originator (agent)
    23 r: request (number)
    24 I: next shops (agent list)
    25 L: collected offers (offer list)
    26 
    27 in the paper, the authors use nonces r_i to add redundancy in the offer
    28 in order to make it safer against dictionary attacks
    29 it is not necessary in our modelization since crypto is assumed to be strong
    30 (Crypt in injective)
    31 ******************************************************************************)
    32 
    33 subsubsection{*offer chaining:
    34 B chains his offer for A with the head offer of L for sending it to C*}
    35 
    36 definition chain :: "agent => nat => agent => msg => agent => msg" where
    37 "chain B ofr A L C ==
    38 let m1= Crypt (pubK A) (Nonce ofr) in
    39 let m2= Hash {|head L, Agent C|} in
    40 sign B {|m1,m2|}"
    41 
    42 declare Let_def [simp]
    43 
    44 lemma chain_inj [iff]: "(chain B ofr A L C = chain B' ofr' A' L' C')
    45 = (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')"
    46 by (auto simp: chain_def Let_def)
    47 
    48 lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}"
    49 by (auto simp: chain_def sign_def)
    50 
    51 subsubsection{*agent whose key is used to sign an offer*}
    52 
    53 fun shop :: "msg => msg" where
    54 "shop {|B,X,Crypt K H|} = Agent (agt K)"
    55 
    56 lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
    57 by (simp add: chain_def sign_def)
    58 
    59 subsubsection{*nonce used in an offer*}
    60 
    61 fun nonce :: "msg => msg" where
    62 "nonce {|B,{|Crypt K ofr,m2|},CryptH|} = ofr"
    63 
    64 lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
    65 by (simp add: chain_def sign_def)
    66 
    67 subsubsection{*next shop*}
    68 
    69 fun next_shop :: "msg => agent" where
    70 "next_shop {|B,{|m1,Hash{|headL,Agent C|}|},CryptH|} = C"
    71 
    72 lemma next_shop_chain [iff]: "next_shop (chain B ofr A L C) = C"
    73 by (simp add: chain_def sign_def)
    74 
    75 subsubsection{*anchor of the offer list*}
    76 
    77 definition anchor :: "agent => nat => agent => msg" where
    78 "anchor A n B == chain A n A (cons nil nil) B"
    79 
    80 lemma anchor_inj [iff]: "(anchor A n B = anchor A' n' B')
    81 = (A=A' & n=n' & B=B')"
    82 by (auto simp: anchor_def)
    83 
    84 lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}"
    85 by (auto simp: anchor_def)
    86 
    87 lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A"
    88 by (simp add: anchor_def)
    89 
    90 lemma nonce_anchor [simp]: "nonce (anchor A n B) = Nonce n"
    91 by (simp add: anchor_def)
    92 
    93 lemma next_shop_anchor [iff]: "next_shop (anchor A n B) = B"
    94 by (simp add: anchor_def)
    95 
    96 subsubsection{*request event*}
    97 
    98 definition reqm :: "agent => nat => nat => msg => agent => msg" where
    99 "reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I),
   100 cons (anchor A n B) nil|}"
   101 
   102 lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B')
   103 = (A=A' & r=r' & n=n' & I=I' & B=B')"
   104 by (auto simp: reqm_def)
   105 
   106 lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}"
   107 by (auto simp: reqm_def)
   108 
   109 definition req :: "agent => nat => nat => msg => agent => event" where
   110 "req A r n I B == Says A B (reqm A r n I B)"
   111 
   112 lemma req_inj [iff]: "(req A r n I B = req A' r' n' I' B')
   113 = (A=A' & r=r' & n=n' & I=I' & B=B')"
   114 by (auto simp: req_def)
   115 
   116 subsubsection{*propose event*}
   117 
   118 definition prom :: "agent => nat => agent => nat => msg => msg =>
   119 msg => agent => msg" where
   120 "prom B ofr A r I L J C == {|Agent A, Number r,
   121 app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}"
   122 
   123 lemma prom_inj [dest]: "prom B ofr A r I L J C
   124 = prom B' ofr' A' r' I' L' J' C'
   125 ==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
   126 by (auto simp: prom_def)
   127 
   128 lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}"
   129 by (auto simp: prom_def)
   130 
   131 definition pro :: "agent => nat => agent => nat => msg => msg =>
   132 msg => agent => event" where
   133 "pro B ofr A r I L J C == Says B C (prom B ofr A r I L J C)"
   134 
   135 lemma pro_inj [dest]: "pro B ofr A r I L J C = pro B' ofr' A' r' I' L' J' C'
   136 ==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
   137 by (auto simp: pro_def dest: prom_inj)
   138 
   139 subsubsection{*protocol*}
   140 
   141 inductive_set p1 :: "event list set"
   142 where
   143 
   144   Nil: "[]:p1"
   145 
   146 | Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1"
   147 
   148 | Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1"
   149 
   150 | Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp;
   151   I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
   152   Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1"
   153 
   154 subsubsection{*Composition of Traces*}
   155 
   156 lemma "evs':p1 ==> 
   157        evs:p1 & (ALL n. Nonce n:used evs' --> Nonce n ~:used evs) --> 
   158        evs'@evs : p1"
   159 apply (erule p1.induct, safe) 
   160 apply (simp_all add: used_ConsI) 
   161 apply (erule p1.Fake, erule synth_sub, rule analz_mono, rule knows_sub_app)
   162 apply (erule p1.Request, safe, simp_all add: req_def, force) 
   163 apply (erule_tac A'=A' in p1.Propose, simp_all) 
   164 apply (drule_tac x=ofr in spec, simp add: pro_def, blast) 
   165 apply (erule_tac A'=A' in p1.Propose, auto simp: pro_def)
   166 done
   167 
   168 subsubsection{*Valid Offer Lists*}
   169 
   170 inductive_set
   171   valid :: "agent => nat => agent => msg set"
   172   for A :: agent and n :: nat and B :: agent
   173 where
   174   Request [intro]: "cons (anchor A n B) nil:valid A n B"
   175 
   176 | Propose [intro]: "L:valid A n B
   177 ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B"
   178 
   179 subsubsection{*basic properties of valid*}
   180 
   181 lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'"
   182 by (erule valid.cases, auto)
   183 
   184 lemma valid_pos_len: "L:valid A n B ==> 0 < len L"
   185 by (erule valid.induct, auto)
   186 
   187 subsubsection{*offers of an offer list*}
   188 
   189 definition offer_nonces :: "msg => msg set" where
   190 "offer_nonces L == {X. X:parts {L} & (EX n. X = Nonce n)}"
   191 
   192 subsubsection{*the originator can get the offers*}
   193 
   194 lemma "L:valid A n B ==> offer_nonces L <= analz (insert L (initState A))"
   195 by (erule valid.induct, auto simp: anchor_def chain_def sign_def
   196 offer_nonces_def initState.simps)
   197 
   198 subsubsection{*list of offers*}
   199 
   200 fun offers :: "msg => msg" where
   201 "offers (cons M L) = cons {|shop M, nonce M|} (offers L)" |
   202 "offers other = nil"
   203 
   204 subsubsection{*list of agents whose keys are used to sign a list of offers*}
   205 
   206 fun shops :: "msg => msg" where
   207 "shops (cons M L) = cons (shop M) (shops L)" |
   208 "shops other = other"
   209 
   210 lemma shops_in_agl: "L:valid A n B ==> shops L:agl"
   211 by (erule valid.induct, auto simp: anchor_def chain_def sign_def)
   212 
   213 subsubsection{*builds a trace from an itinerary*}
   214 
   215 fun offer_list :: "agent * nat * agent * msg * nat => msg" where
   216 "offer_list (A,n,B,nil,ofr) = cons (anchor A n B) nil" |
   217 "offer_list (A,n,B,cons (Agent C) I,ofr) = (
   218 let L = offer_list (A,n,B,I,Suc ofr) in
   219 cons (chain (next_shop (head L)) ofr A L C) L)"
   220 
   221 lemma "I:agl ==> ALL ofr. offer_list (A,n,B,I,ofr):valid A n B"
   222 by (erule agl.induct, auto)
   223 
   224 fun trace :: "agent * nat * agent * nat * msg * msg * msg
   225 => event list" where
   226 "trace (B,ofr,A,r,I,L,nil) = []" |
   227 "trace (B,ofr,A,r,I,L,cons (Agent D) K) = (
   228 let C = (if K=nil then B else agt_nb (head K)) in
   229 let I' = (if K=nil then cons (Agent A) (cons (Agent B) I)
   230           else cons (Agent A) (app (I, cons (head K) nil))) in
   231 let I'' = app (I, cons (head K) nil) in
   232 pro C (Suc ofr) A r I' L nil D
   233 # trace (B,Suc ofr,A,r,I'',tail L,K))"
   234 
   235 definition trace' :: "agent => nat => nat => msg => agent => nat => event list" where
   236 "trace' A r n I B ofr == (
   237 let AI = cons (Agent A) I in
   238 let L = offer_list (A,n,B,AI,ofr) in
   239 trace (B,ofr,A,r,nil,L,AI))"
   240 
   241 declare trace'_def [simp]
   242 
   243 subsubsection{*there is a trace in which the originator receives a valid answer*}
   244 
   245 lemma p1_not_empty: "evs:p1 ==> req A r n I B:set evs -->
   246 (EX evs'. evs'@evs:p1 & pro B' ofr A r I' L J A:set evs' & L:valid A n B)"
   247 oops
   248 
   249 
   250 subsection{*properties of protocol P1*}
   251 
   252 text{*publicly verifiable forward integrity:
   253 anyone can verify the validity of an offer list*}
   254 
   255 subsubsection{*strong forward integrity:
   256 except the last one, no offer can be modified*}
   257 
   258 lemma strong_forward_integrity: "ALL L. Suc i < len L
   259 --> L:valid A n B & repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)"
   260 apply (induct i)
   261 (* i = 0 *)
   262 apply clarify
   263 apply (frule len_not_empty, clarsimp)
   264 apply (frule len_not_empty, clarsimp)
   265 apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a)
   266 apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a)
   267 apply (simp add: chain_def)
   268 (* i > 0 *)
   269 apply clarify
   270 apply (frule len_not_empty, clarsimp)
   271 apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na)
   272 apply (frule len_not_empty, clarsimp)
   273 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
   274 by (drule_tac x=l' in spec, simp, blast)
   275 
   276 subsubsection{*insertion resilience:
   277 except at the beginning, no offer can be inserted*}
   278 
   279 lemma chain_isnt_head [simp]: "L:valid A n B ==>
   280 head L ~= chain (next_shop (head L)) ofr A L C"
   281 by (erule valid.induct, auto simp: chain_def sign_def anchor_def)
   282 
   283 lemma insertion_resilience: "ALL L. L:valid A n B --> Suc i < len L
   284 --> ins (L,Suc i,M) ~:valid A n B"
   285 apply (induct i)
   286 (* i = 0 *)
   287 apply clarify
   288 apply (frule len_not_empty, clarsimp)
   289 apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp)
   290 apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp)
   291 apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp)
   292 (* i > 0 *)
   293 apply clarify
   294 apply (frule len_not_empty, clarsimp)
   295 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
   296 apply (frule len_not_empty, clarsimp)
   297 apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na)
   298 apply (frule len_not_empty, clarsimp)
   299 by (drule_tac x=l' in spec, clarsimp)
   300 
   301 subsubsection{*truncation resilience:
   302 only shop i can truncate at offer i*}
   303 
   304 lemma truncation_resilience: "ALL L. L:valid A n B --> Suc i < len L
   305 --> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))"
   306 apply (induct i)
   307 (* i = 0 *)
   308 apply clarify
   309 apply (frule len_not_empty, clarsimp)
   310 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
   311 apply (frule len_not_empty, clarsimp)
   312 apply (ind_cases "{|M,l'|}:valid A n B" for l')
   313 apply (frule len_not_empty, clarsimp, simp)
   314 (* i > 0 *)
   315 apply clarify
   316 apply (frule len_not_empty, clarsimp)
   317 apply (ind_cases "{|x,l'|}:valid A n B" for x l')
   318 apply (frule len_not_empty, clarsimp)
   319 by (drule_tac x=l' in spec, clarsimp)
   320 
   321 subsubsection{*declarations for tactics*}
   322 
   323 declare knows_Spy_partsEs [elim]
   324 declare Fake_parts_insert [THEN subsetD, dest]
   325 declare initState.simps [simp del]
   326 
   327 subsubsection{*get components of a message*}
   328 
   329 lemma get_ML [dest]: "Says A' B {|A,r,I,M,L|}:set evs ==>
   330 M:parts (spies evs) & L:parts (spies evs)"
   331 by blast
   332 
   333 subsubsection{*general properties of p1*}
   334 
   335 lemma reqm_neq_prom [iff]:
   336 "reqm A r n I B ~= prom B' ofr A' r' I' (cons M L) J C"
   337 by (auto simp: reqm_def prom_def)
   338 
   339 lemma prom_neq_reqm [iff]:
   340 "prom B' ofr A' r' I' (cons M L) J C ~= reqm A r n I B"
   341 by (auto simp: reqm_def prom_def)
   342 
   343 lemma req_neq_pro [iff]: "req A r n I B ~= pro B' ofr A' r' I' (cons M L) J C"
   344 by (auto simp: req_def pro_def)
   345 
   346 lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C ~= req A r n I B"
   347 by (auto simp: req_def pro_def)
   348 
   349 lemma p1_has_no_Gets: "evs:p1 ==> ALL A X. Gets A X ~:set evs"
   350 by (erule p1.induct, auto simp: req_def pro_def)
   351 
   352 lemma p1_is_Gets_correct [iff]: "Gets_correct p1"
   353 by (auto simp: Gets_correct_def dest: p1_has_no_Gets)
   354 
   355 lemma p1_is_one_step [iff]: "one_step p1"
   356 by (unfold one_step_def, clarify, ind_cases "ev#evs:p1" for ev evs, auto)
   357 
   358 lemma p1_has_only_Says' [rule_format]: "evs:p1 ==>
   359 ev:set evs --> (EX A B X. ev=Says A B X)"
   360 by (erule p1.induct, auto simp: req_def pro_def)
   361 
   362 lemma p1_has_only_Says [iff]: "has_only_Says p1"
   363 by (auto simp: has_only_Says_def dest: p1_has_only_Says')
   364 
   365 lemma p1_is_regular [iff]: "regular p1"
   366 apply (simp only: regular_def, clarify)
   367 apply (erule_tac p1.induct)
   368 apply (simp_all add: initState.simps knows.simps pro_def prom_def
   369                      req_def reqm_def anchor_def chain_def sign_def)
   370 by (auto dest: no_Key_in_agl no_Key_in_appdel parts_trans)
   371 
   372 subsubsection{*private keys are safe*}
   373 
   374 lemma priK_parts_Friend_imp_bad [rule_format,dest]:
   375      "[| evs:p1; Friend B ~= A |]
   376       ==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
   377 apply (erule p1.induct)
   378 apply (simp_all add: initState.simps knows.simps pro_def prom_def
   379                 req_def reqm_def anchor_def chain_def sign_def)
   380 apply (blast dest: no_Key_in_agl)
   381 apply (auto del: parts_invKey disjE  dest: parts_trans
   382             simp add: no_Key_in_appdel)
   383 done
   384 
   385 lemma priK_analz_Friend_imp_bad [rule_format,dest]:
   386      "[| evs:p1; Friend B ~= A |]
   387 ==> (Key (priK A):analz (knows (Friend B) evs)) --> (A:bad)"
   388 by auto
   389 
   390 lemma priK_notin_knows_max_Friend: "[| evs:p1; A ~:bad; A ~= Friend C |]
   391 ==> Key (priK A) ~:analz (knows_max (Friend C) evs)"
   392 apply (rule not_parts_not_analz, simp add: knows_max_def, safe)
   393 apply (drule_tac H="spies' evs" in parts_sub)
   394 apply (rule_tac p=p1 in knows_max'_sub_spies', simp+)
   395 apply (drule_tac H="spies evs" in parts_sub)
   396 by (auto dest: knows'_sub_knows [THEN subsetD] priK_notin_initState_Friend)
   397 
   398 subsubsection{*general guardedness properties*}
   399 
   400 lemma agl_guard [intro]: "I:agl ==> I:guard n Ks"
   401 by (erule agl.induct, auto)
   402 
   403 lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs;
   404 Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
   405 by (auto dest: Says_to_knows_max')
   406 
   407 lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs;
   408 Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
   409 by (auto dest: Says_from_knows_max')
   410 
   411 lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs;
   412 Nonce n ~:used evs |] ==> L:guard n Ks"
   413 by (drule not_used_not_parts, auto)
   414 
   415 subsubsection{*guardedness of messages*}
   416 
   417 lemma chain_guard [iff]: "chain B ofr A L C:guard n {priK A}"
   418 by (case_tac "ofr=n", auto simp: chain_def sign_def)
   419 
   420 lemma chain_guard_Nonce_neq [intro]: "n ~= ofr
   421 ==> chain B ofr A' L C:guard n {priK A}"
   422 by (auto simp: chain_def sign_def)
   423 
   424 lemma anchor_guard [iff]: "anchor A n' B:guard n {priK A}"
   425 by (case_tac "n'=n", auto simp: anchor_def)
   426 
   427 lemma anchor_guard_Nonce_neq [intro]: "n ~= n'
   428 ==> anchor A' n' B:guard n {priK A}"
   429 by (auto simp: anchor_def)
   430 
   431 lemma reqm_guard [intro]: "I:agl ==> reqm A r n' I B:guard n {priK A}"
   432 by (case_tac "n'=n", auto simp: reqm_def)
   433 
   434 lemma reqm_guard_Nonce_neq [intro]: "[| n ~= n'; I:agl |]
   435 ==> reqm A' r n' I B:guard n {priK A}"
   436 by (auto simp: reqm_def)
   437 
   438 lemma prom_guard [intro]: "[| I:agl; J:agl; L:guard n {priK A} |]
   439 ==> prom B ofr A r I L J C:guard n {priK A}"
   440 by (auto simp: prom_def)
   441 
   442 lemma prom_guard_Nonce_neq [intro]: "[| n ~= ofr; I:agl; J:agl;
   443 L:guard n {priK A} |] ==> prom B ofr A' r I L J C:guard n {priK A}"
   444 by (auto simp: prom_def)
   445 
   446 subsubsection{*Nonce uniqueness*}
   447 
   448 lemma uniq_Nonce_in_chain [dest]: "Nonce k:parts {chain B ofr A L C} ==> k=ofr"
   449 by (auto simp: chain_def sign_def)
   450 
   451 lemma uniq_Nonce_in_anchor [dest]: "Nonce k:parts {anchor A n B} ==> k=n"
   452 by (auto simp: anchor_def chain_def sign_def)
   453 
   454 lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k:parts {reqm A r n I B};
   455 I:agl |] ==> k=n"
   456 by (auto simp: reqm_def dest: no_Nonce_in_agl)
   457 
   458 lemma uniq_Nonce_in_prom [dest]: "[| Nonce k:parts {prom B ofr A r I L J C};
   459 I:agl; J:agl; Nonce k ~:parts {L} |] ==> k=ofr"
   460 by (auto simp: prom_def dest: no_Nonce_in_agl no_Nonce_in_appdel)
   461 
   462 subsubsection{*requests are guarded*}
   463 
   464 lemma req_imp_Guard [rule_format]: "[| evs:p1; A ~:bad |] ==>
   465 req A r n I B:set evs --> Guard n {priK A} (spies evs)"
   466 apply (erule p1.induct, simp)
   467 apply (simp add: req_def knows.simps, safe)
   468 apply (erule in_synth_Guard, erule Guard_analz, simp)
   469 by (auto simp: req_def pro_def dest: Says_imp_knows_Spy)
   470 
   471 lemma req_imp_Guard_Friend: "[| evs:p1; A ~:bad; req A r n I B:set evs |]
   472 ==> Guard n {priK A} (knows_max (Friend C) evs)"
   473 apply (rule Guard_knows_max')
   474 apply (rule_tac H="spies evs" in Guard_mono)
   475 apply (rule req_imp_Guard, simp+)
   476 apply (rule_tac B="spies' evs" in subset_trans)
   477 apply (rule_tac p=p1 in knows_max'_sub_spies', simp+)
   478 by (rule knows'_sub_knows)
   479 
   480 subsubsection{*propositions are guarded*}
   481 
   482 lemma pro_imp_Guard [rule_format]: "[| evs:p1; B ~:bad; A ~:bad |] ==>
   483 pro B ofr A r I (cons M L) J C:set evs --> Guard ofr {priK A} (spies evs)"
   484 apply (erule p1.induct) (* +3 subgoals *)
   485 (* Nil *)
   486 apply simp
   487 (* Fake *)
   488 apply (simp add: pro_def, safe) (* +4 subgoals *)
   489 (* 1 *)
   490 apply (erule in_synth_Guard, drule Guard_analz, simp, simp)
   491 (* 2 *)
   492 apply simp
   493 (* 3 *)
   494 apply (simp, simp add: req_def pro_def, blast)
   495 (* 4 *)
   496 apply (simp add: pro_def)
   497 apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard)
   498 (* 5 *)
   499 apply simp
   500 apply safe (* +1 subgoal *)
   501 apply (simp add: pro_def)
   502 apply (blast dest: prom_inj Says_Nonce_not_used_guard)
   503 (* 6 *)
   504 apply (simp add: pro_def)
   505 apply (blast dest: Says_imp_knows_Spy)
   506 (* Request *)
   507 apply (simp add: pro_def)
   508 apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard)
   509 (* Propose *)
   510 apply simp
   511 apply safe (* +1 subgoal *)
   512 (* 1 *)
   513 apply (simp add: pro_def)
   514 apply (blast dest: prom_inj Says_Nonce_not_used_guard)
   515 (* 2 *)
   516 apply (simp add: pro_def)
   517 by (blast dest: Says_imp_knows_Spy)
   518 
   519 lemma pro_imp_Guard_Friend: "[| evs:p1; B ~:bad; A ~:bad;
   520 pro B ofr A r I (cons M L) J C:set evs |]
   521 ==> Guard ofr {priK A} (knows_max (Friend D) evs)"
   522 apply (rule Guard_knows_max')
   523 apply (rule_tac H="spies evs" in Guard_mono)
   524 apply (rule pro_imp_Guard, simp+)
   525 apply (rule_tac B="spies' evs" in subset_trans)
   526 apply (rule_tac p=p1 in knows_max'_sub_spies', simp+)
   527 by (rule knows'_sub_knows)
   528 
   529 subsubsection{*data confidentiality:
   530 no one other than the originator can decrypt the offers*}
   531 
   532 lemma Nonce_req_notin_spies: "[| evs:p1; req A r n I B:set evs; A ~:bad |]
   533 ==> Nonce n ~:analz (spies evs)"
   534 by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+)
   535 
   536 lemma Nonce_req_notin_knows_max_Friend: "[| evs:p1; req A r n I B:set evs;
   537 A ~:bad; A ~= Friend C |] ==> Nonce n ~:analz (knows_max (Friend C) evs)"
   538 apply (clarify, frule_tac C=C in req_imp_Guard_Friend, simp+)
   539 apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+)
   540 by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def)
   541 
   542 lemma Nonce_pro_notin_spies: "[| evs:p1; B ~:bad; A ~:bad;
   543 pro B ofr A r I (cons M L) J C:set evs |] ==> Nonce ofr ~:analz (spies evs)"
   544 by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+)
   545 
   546 lemma Nonce_pro_notin_knows_max_Friend: "[| evs:p1; B ~:bad; A ~:bad;
   547 A ~= Friend D; pro B ofr A r I (cons M L) J C:set evs |]
   548 ==> Nonce ofr ~:analz (knows_max (Friend D) evs)"
   549 apply (clarify, frule_tac A=A in pro_imp_Guard_Friend, simp+)
   550 apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+)
   551 by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def)
   552 
   553 subsubsection{*non repudiability:
   554 an offer signed by B has been sent by B*}
   555 
   556 lemma Crypt_reqm: "[| Crypt (priK A) X:parts {reqm A' r n I B}; I:agl |] ==> A=A'"
   557 by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl)
   558 
   559 lemma Crypt_prom: "[| Crypt (priK A) X:parts {prom B ofr A' r I L J C};
   560 I:agl; J:agl |] ==> A=B | Crypt (priK A) X:parts {L}"
   561 apply (simp add: prom_def anchor_def chain_def sign_def)
   562 by (blast dest: no_Crypt_in_agl no_Crypt_in_appdel)
   563 
   564 lemma Crypt_safeness: "[| evs:p1; A ~:bad |] ==> Crypt (priK A) X:parts (spies evs)
   565 --> (EX B Y. Says A B Y:set evs & Crypt (priK A) X:parts {Y})"
   566 apply (erule p1.induct)
   567 (* Nil *)
   568 apply simp
   569 (* Fake *)
   570 apply clarsimp
   571 apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
   572 apply (erule disjE)
   573 apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast)
   574 (* Request *)
   575 apply (simp add: req_def, clarify)
   576 apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
   577 apply (erule disjE)
   578 apply (frule Crypt_reqm, simp, clarify)
   579 apply (rule_tac x=B in exI, rule_tac x="reqm A r n I B" in exI, simp, blast)
   580 (* Propose *)
   581 apply (simp add: pro_def, clarify)
   582 apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
   583 apply (rotate_tac -1, erule disjE)
   584 apply (frule Crypt_prom, simp, simp)
   585 apply (rotate_tac -1, erule disjE)
   586 apply (rule_tac x=C in exI)
   587 apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI, blast)
   588 apply (subgoal_tac "cons M L:parts (spies evsp)")
   589 apply (drule_tac G="{cons M L}" and H="spies evsp" in parts_trans, blast, blast)
   590 apply (drule Says_imp_spies, rotate_tac -1, drule parts.Inj)
   591 apply (drule parts.Snd, drule parts.Snd, drule parts.Snd)
   592 by auto
   593 
   594 lemma Crypt_Hash_imp_sign: "[| evs:p1; A ~:bad |] ==>
   595 Crypt (priK A) (Hash X):parts (spies evs)
   596 --> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})"
   597 apply (erule p1.induct)
   598 (* Nil *)
   599 apply simp
   600 (* Fake *)
   601 apply clarsimp
   602 apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
   603 apply simp
   604 apply (erule disjE)
   605 apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast)
   606 (* Request *)
   607 apply (simp add: req_def, clarify)
   608 apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
   609 apply simp
   610 apply (erule disjE)
   611 apply (frule Crypt_reqm, simp+)
   612 apply (rule_tac x=B in exI, rule_tac x="reqm Aa r n I B" in exI)
   613 apply (simp add: reqm_def sign_def anchor_def no_Crypt_in_agl)
   614 apply (simp add: chain_def sign_def, blast)
   615 (* Propose *)
   616 apply (simp add: pro_def, clarify)
   617 apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
   618 apply simp
   619 apply (rotate_tac -1, erule disjE)
   620 apply (simp add: prom_def sign_def no_Crypt_in_agl no_Crypt_in_appdel)
   621 apply (simp add: chain_def sign_def)
   622 apply (rotate_tac -1, erule disjE)
   623 apply (rule_tac x=C in exI)
   624 apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI)
   625 apply (simp add: prom_def chain_def sign_def)
   626 apply (erule impE) 
   627 apply (blast dest: get_ML parts_sub) 
   628 apply (blast del: MPair_parts)+
   629 done
   630 
   631 lemma sign_safeness: "[| evs:p1; A ~:bad |] ==> sign A X:parts (spies evs)
   632 --> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})"
   633 apply (clarify, simp add: sign_def, frule parts.Snd)
   634 apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def])
   635 done
   636 
   637 end