src/HOL/Auth/OtwayReesBella.thy
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 24122 fc7f857d33c8
child 30510 4120fc59dd85
permissions -rw-r--r--
named code theorem for Fract_norm
     1 (*  ID:         $Id$
     2     Author:     Giampaolo Bella, Catania University
     3 *)
     4 
     5 header{*Bella's version of the Otway-Rees protocol*}
     6 
     7 
     8 theory OtwayReesBella imports Public begin
     9 
    10 text{*Bella's modifications to a version of the Otway-Rees protocol taken from
    11 the BAN paper only concern message 7. The updated protocol makes the goal of
    12 key distribution of the session key available to A. Investigating the
    13 principle of Goal Availability undermines the BAN claim about the original
    14 protocol, that "this protocol does not make use of Kab as an encryption key,
    15 so neither principal can know whether the key is known to the other". The
    16 updated protocol makes no use of the session key to encrypt but informs A that
    17 B knows it.*}
    18 
    19 inductive_set orb :: "event list set"
    20  where
    21 
    22   Nil:  "[]\<in> orb"
    23 
    24 | Fake: "\<lbrakk>evsa\<in> orb;  X\<in> synth (analz (knows Spy evsa))\<rbrakk>
    25  	 \<Longrightarrow> Says Spy B X  # evsa \<in> orb"
    26 
    27 | Reception: "\<lbrakk>evsr\<in> orb;  Says A B X \<in> set evsr\<rbrakk>
    28 	      \<Longrightarrow> Gets B X # evsr \<in> orb"
    29 
    30 | OR1:  "\<lbrakk>evs1\<in> orb;  Nonce NA \<notin> used evs1\<rbrakk>
    31 	 \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, 
    32 		   Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
    33 	       # evs1 \<in> orb"
    34 
    35 | OR2:  "\<lbrakk>evs2\<in> orb;  Nonce NB \<notin> used evs2;
    36 	   Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk>
    37 	\<Longrightarrow> Says B Server 
    38 		\<lbrace>Nonce M, Agent A, Agent B, X, 
    39 	   Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
    40 	       # evs2 \<in> orb"
    41 
    42 | OR3:  "\<lbrakk>evs3\<in> orb;  Key KAB \<notin> used evs3;
    43 	  Gets Server 
    44 	     \<lbrace>Nonce M, Agent A, Agent B, 
    45 	       Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>, 
    46 	       Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
    47 	  \<in> set evs3\<rbrakk>
    48 	\<Longrightarrow> Says Server B \<lbrace>Nonce M,
    49 		    Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
    50 				      Nonce NB, Key KAB\<rbrace>\<rbrace>
    51 	       # evs3 \<in> orb"
    52 
    53   (*B can only check that the message he is bouncing is a ciphertext*)
    54   (*Sending M back is omitted*)   
    55 | OR4:  "\<lbrakk>evs4\<in> orb; B \<noteq> Server; \<forall> p q. X \<noteq> \<lbrace>p, q\<rbrace>; 
    56 	  Says B Server \<lbrace>Nonce M, Agent A, Agent B, X', 
    57 		Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
    58 	    \<in> set evs4;
    59 	  Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce NB, Key KAB\<rbrace>\<rbrace>
    60 	    \<in> set evs4\<rbrakk>
    61 	\<Longrightarrow> Says B A \<lbrace>Nonce M, X\<rbrace> # evs4 \<in> orb"
    62 
    63 
    64 | Oops: "\<lbrakk>evso\<in> orb;  
    65 	   Says Server B \<lbrace>Nonce M,
    66 		    Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
    67 				      Nonce NB, Key KAB\<rbrace>\<rbrace> 
    68 	     \<in> set evso\<rbrakk>
    69  \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB, Key KAB\<rbrace> # evso 
    70      \<in> orb"
    71 
    72 
    73 
    74 declare knows_Spy_partsEs [elim]
    75 declare analz_into_parts [dest]
    76 declare Fake_parts_insert_in_Un  [dest]
    77 
    78 
    79 text{*Fragile proof, with backtracking in the possibility call.*}
    80 lemma possibility_thm: "\<lbrakk>A \<noteq> Server; B \<noteq> Server; Key K \<notin> used[]\<rbrakk>    
    81       \<Longrightarrow>   \<exists> evs \<in> orb.           
    82      Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs"
    83 apply (intro exI bexI)
    84 apply (rule_tac [2] orb.Nil
    85                     [THEN orb.OR1, THEN orb.Reception,
    86                      THEN orb.OR2, THEN orb.Reception,
    87                      THEN orb.OR3, THEN orb.Reception, THEN orb.OR4]) 
    88 apply (possibility, simp add: used_Cons)  
    89 done
    90 
    91 
    92 lemma Gets_imp_Says :
    93      "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
    94 apply (erule rev_mp)
    95 apply (erule orb.induct)
    96 apply auto
    97 done
    98 
    99 lemma Gets_imp_knows_Spy: 
   100      "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk>  \<Longrightarrow> X \<in> knows Spy evs"
   101 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   102 
   103 declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
   104 
   105 lemma Gets_imp_knows:
   106      "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk>  \<Longrightarrow> X \<in> knows B evs"
   107 apply (case_tac "B = Spy")
   108 apply (blast dest!: Gets_imp_knows_Spy)
   109 apply (blast dest!: Gets_imp_knows_agents)
   110 done
   111 
   112 
   113 lemma OR2_analz_knows_Spy: 
   114    "\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk>   
   115     \<Longrightarrow> X \<in> analz (knows Spy evs)"
   116 by (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
   117 
   118 lemma OR4_parts_knows_Spy: 
   119    "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key Kab\<rbrace>\<rbrace>  \<in> set evs; 
   120       evs \<in> orb\<rbrakk>   \<Longrightarrow> X \<in> parts (knows Spy evs)"
   121 by blast
   122 
   123 lemma Oops_parts_knows_Spy: 
   124     "Says Server B \<lbrace>Nonce M, Crypt K' \<lbrace>X, Nonce Nb, K\<rbrace>\<rbrace> \<in> set evs  
   125      \<Longrightarrow> K \<in> parts (knows Spy evs)"
   126 by blast
   127 
   128 lemmas OR2_parts_knows_Spy =
   129     OR2_analz_knows_Spy [THEN analz_into_parts, standard]
   130 
   131 ML
   132 {*
   133 fun parts_explicit_tac i = 
   134     forward_tac [@{thm Oops_parts_knows_Spy}] (i+7) THEN
   135     forward_tac [@{thm OR4_parts_knows_Spy}]  (i+6) THEN
   136     forward_tac [@{thm OR2_parts_knows_Spy}]  (i+4)
   137 *}
   138  
   139 method_setup parts_explicit = {*
   140     Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
   141   "to explicitly state that some message components belong to parts knows Spy"
   142 
   143 
   144 lemma Spy_see_shrK [simp]: 
   145     "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   146 by (erule orb.induct, parts_explicit, simp_all, blast+)
   147 
   148 lemma Spy_analz_shrK [simp]: 
   149 "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   150 by auto
   151 
   152 lemma Spy_see_shrK_D [dest!]:
   153      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> orb|] ==> A \<in> bad"
   154 by (blast dest: Spy_see_shrK)
   155 
   156 lemma new_keys_not_used [simp]:
   157    "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> orb\<rbrakk>  \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))"
   158 apply (erule rev_mp)
   159 apply (erule orb.induct, parts_explicit, simp_all)
   160 apply (force dest!: keysFor_parts_insert)
   161 apply (blast+)
   162 done
   163 
   164 
   165 
   166 subsection{* Proofs involving analz *}
   167 
   168 text{*Describes the form of K and NA when the Server sends this message.  Also
   169   for Oops case.*}
   170 lemma Says_Server_message_form: 
   171 "\<lbrakk>Says Server B  \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
   172      evs \<in> orb\<rbrakk>                                            
   173  \<Longrightarrow> K \<notin> range shrK & (\<exists> A Na. X=(Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
   174 by (erule rev_mp, erule orb.induct, simp_all)
   175 
   176 lemma Says_Server_imp_Gets: 
   177  "\<lbrakk>Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
   178                                              Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;
   179     evs \<in> orb\<rbrakk>
   180   \<Longrightarrow>  Gets Server \<lbrace>Nonce M, Agent A, Agent B, 
   181                    Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>, 
   182                Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
   183          \<in> set evs"
   184 by (erule rev_mp, erule orb.induct, simp_all)
   185 
   186 
   187 lemma A_trusts_OR1: 
   188 "\<lbrakk>Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);  
   189     A \<notin> bad; evs \<in> orb\<rbrakk>                   
   190  \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs"
   191 apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
   192 apply (blast)
   193 done
   194 
   195 
   196 lemma B_trusts_OR2:
   197  "\<lbrakk>Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>  
   198       \<in> parts (knows Spy evs);  B \<notin> bad; evs \<in> orb\<rbrakk>                   
   199   \<Longrightarrow> (\<exists> X. Says B Server \<lbrace>Nonce M, Agent A, Agent B, X,  
   200               Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
   201           \<in> set evs)"
   202 apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
   203 apply (blast+)
   204 done
   205 
   206 
   207 lemma B_trusts_OR3: 
   208 "\<lbrakk>Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace> \<in> parts (knows Spy evs);  
   209    B \<notin> bad; evs \<in> orb\<rbrakk>                   
   210 \<Longrightarrow> \<exists> M. Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> 
   211          \<in> set evs"
   212 apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
   213 apply (blast+)
   214 done
   215 
   216 lemma Gets_Server_message_form: 
   217 "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
   218     evs \<in> orb\<rbrakk>                                              
   219  \<Longrightarrow> (K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>)))    
   220              | X \<in> analz (knows Spy evs)"
   221 apply (case_tac "B \<in> bad")
   222 apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, 
   223                                  THEN analz.Decrypt, THEN analz.Fst])
   224 prefer 3 apply blast
   225 prefer 3 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN 
   226                                                  parts.Snd, THEN B_trusts_OR3]
   227                              Says_Server_message_form)
   228 apply simp_all                                    
   229 done
   230 
   231 lemma unique_Na: "\<lbrakk>Says A B  \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;   
   232          Says A B' \<lbrace>Nonce M', Agent A, Agent B', Crypt (shrK A) \<lbrace>Nonce Na, Nonce M', Agent A, Agent B'\<rbrace>\<rbrace> \<in> set evs;  
   233     A \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow> B=B' & M=M'"
   234 by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
   235 
   236 lemma unique_Nb: "\<lbrakk>Says B Server \<lbrace>Nonce M, Agent A, Agent B, X, Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;   
   237          Says B Server \<lbrace>Nonce M', Agent A', Agent B, X', Crypt (shrK B) \<lbrace>Nonce Nb,Nonce M', Nonce M', Agent A', Agent B\<rbrace>\<rbrace> \<in> set evs;   
   238     B \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow>   M=M' & A=A' & X=X'"
   239 by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
   240 
   241 lemma analz_image_freshCryptK_lemma:
   242 "(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow>  
   243         (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)";
   244 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   245 
   246 ML
   247 {*
   248 structure OtwayReesBella =
   249 struct
   250 
   251 val analz_image_freshK_ss = 
   252   @{simpset} delsimps [image_insert, image_Un]
   253       delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
   254       addsimps @{thms analz_image_freshK_simps}
   255 
   256 end
   257 *}
   258 
   259 method_setup analz_freshCryptK = {*
   260     Method.ctxt_args (fn ctxt =>
   261      (Method.SIMPLE_METHOD
   262       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   263           REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
   264           ALLGOALS (asm_simp_tac
   265             (Simplifier.context ctxt OtwayReesBella.analz_image_freshK_ss))]))) *}
   266   "for proving useful rewrite rule"
   267 
   268 
   269 method_setup disentangle = {*
   270     Method.no_args
   271      (Method.SIMPLE_METHOD
   272       (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
   273                    ORELSE' hyp_subst_tac))) *}
   274   "for eliminating conjunctions, disjunctions and the like"
   275 
   276 
   277 
   278 lemma analz_image_freshCryptK [rule_format]: 
   279 "evs \<in> orb \<Longrightarrow>                              
   280      Key K \<notin> analz (knows Spy evs) \<longrightarrow>  
   281        (\<forall> KK. KK \<subseteq> - (range shrK) \<longrightarrow>                  
   282              (Crypt K X \<in> analz (Key`KK \<union> (knows Spy evs))) =   
   283              (Crypt K X \<in> analz (knows Spy evs)))"
   284 apply (erule orb.induct)
   285 apply (analz_mono_contra)
   286 apply (frule_tac [7] Gets_Server_message_form)
   287 apply (frule_tac [9] Says_Server_message_form)
   288 apply disentangle
   289 apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN  analz.Snd])
   290 prefer 8 apply clarify
   291 apply (analz_freshCryptK, spy_analz, fastsimp)
   292 done
   293 
   294 
   295 
   296 lemma analz_insert_freshCryptK: 
   297 "\<lbrakk>evs \<in> orb;  Key K \<notin> analz (knows Spy evs);  
   298          Seskey \<notin> range shrK\<rbrakk> \<Longrightarrow>   
   299          (Crypt K X \<in> analz (insert (Key Seskey) (knows Spy evs))) =  
   300          (Crypt K X \<in> analz (knows Spy evs))"
   301 by (simp only: analz_image_freshCryptK analz_image_freshK_simps)
   302 
   303 
   304 lemma analz_hard: 
   305 "\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
   306              Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
   307    Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace> \<in> analz (knows Spy evs);  
   308    A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>                   
   309  \<Longrightarrow>  Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs"
   310 apply (erule rev_mp)
   311 apply (erule rev_mp)
   312 apply (erule orb.induct)
   313 apply (frule_tac [7] Gets_Server_message_form)
   314 apply (frule_tac [9] Says_Server_message_form)
   315 apply disentangle
   316 txt{*letting the simplifier solve OR2*}
   317 apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd])
   318 apply (simp_all (no_asm_simp) add: analz_insert_eq pushes split_ifs)
   319 apply (spy_analz)
   320 txt{*OR1*}
   321 apply blast
   322 txt{*Oops*}
   323 prefer 4 apply (blast dest: analz_insert_freshCryptK)
   324 txt{*OR4 - ii*}
   325 prefer 3 apply (blast)
   326 txt{*OR3*}
   327 (*adding Gets_imp_ and Says_imp_ for efficiency*)
   328 apply (blast dest: 
   329        A_trusts_OR1 unique_Na Key_not_used analz_insert_freshCryptK)
   330 txt{*OR4 - i *}
   331 apply clarify
   332 apply (simp add: pushes split_ifs)
   333 apply (case_tac "Aaa\<in>bad")
   334 apply (blast dest: analz_insert_freshCryptK)
   335 apply clarify
   336 apply simp
   337 apply (case_tac "Ba\<in>bad")
   338 apply (frule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Decrypt, THEN analz.Fst] , assumption)
   339 apply (simp (no_asm_simp))
   340 apply clarify
   341 apply (frule Gets_imp_knows_Spy 
   342              [THEN parts.Inj, THEN parts.Snd, THEN B_trusts_OR3],  
   343        assumption, assumption, assumption, erule exE)
   344 apply (frule Says_Server_imp_Gets 
   345             [THEN Gets_imp_knows_Spy, THEN parts.Inj, THEN parts.Snd, 
   346             THEN parts.Snd, THEN parts.Snd, THEN parts.Fst, THEN A_trusts_OR1],
   347        assumption, assumption, assumption, assumption)
   348 apply (blast dest: Says_Server_imp_Gets B_trusts_OR2 unique_Na unique_Nb)
   349 done
   350 
   351 
   352 lemma Gets_Server_message_form': 
   353 "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace>  \<in> set evs;  
   354    B \<notin> bad; evs \<in> orb\<rbrakk>                              
   355   \<Longrightarrow> K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
   356 by (blast dest!: B_trusts_OR3 Says_Server_message_form)
   357 
   358 
   359 lemma OR4_imp_Gets: 
   360 "\<lbrakk>Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;   
   361    B \<notin> bad; evs \<in> orb\<rbrakk>  
   362  \<Longrightarrow> (\<exists> Nb. Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
   363                                              Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs)"
   364 apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
   365 prefer 3 apply (blast dest: Gets_Server_message_form')
   366 apply blast+
   367 done
   368 
   369 
   370 lemma A_keydist_to_B: 
   371 "\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
   372             Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
   373    Gets A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;    
   374    A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>  
   375   \<Longrightarrow> Key K \<in> analz (knows B evs)"
   376 apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
   377 apply (drule analz_hard, assumption, assumption, assumption, assumption)
   378 apply (drule OR4_imp_Gets, assumption, assumption)
   379 apply (erule exE)
   380 (*blast doesn't do because it can't infer that Key (shrK P) \<in> (knows P evs)*)
   381 apply (fastsimp dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
   382 done
   383 
   384 
   385 text{*Other properties as for the original protocol*}
   386 
   387 
   388 end