src/HOL/Auth/OtwayReesBella.thy
author wenzelm
Sat Apr 27 20:50:20 2013 +0200 (2013-04-27)
changeset 51798 ad3a241def73
parent 51717 9e7d1c139569
child 58889 5b7a9633cfa8
permissions -rw-r--r--
uniform Proof.context for hyp_subst_tac;
     1 (*  Title:      HOL/Auth/OtwayReesBella.thy
     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 by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
   108 
   109 lemma OR2_analz_knows_Spy: 
   110    "\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk>   
   111     \<Longrightarrow> X \<in> analz (knows Spy evs)"
   112 by (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
   113 
   114 lemma OR4_parts_knows_Spy: 
   115    "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key Kab\<rbrace>\<rbrace>  \<in> set evs; 
   116       evs \<in> orb\<rbrakk>   \<Longrightarrow> X \<in> parts (knows Spy evs)"
   117 by blast
   118 
   119 lemma Oops_parts_knows_Spy: 
   120     "Says Server B \<lbrace>Nonce M, Crypt K' \<lbrace>X, Nonce Nb, K\<rbrace>\<rbrace> \<in> set evs  
   121      \<Longrightarrow> K \<in> parts (knows Spy evs)"
   122 by blast
   123 
   124 lemmas OR2_parts_knows_Spy =
   125     OR2_analz_knows_Spy [THEN analz_into_parts]
   126 
   127 ML
   128 {*
   129 fun parts_explicit_tac i = 
   130     forward_tac [@{thm Oops_parts_knows_Spy}] (i+7) THEN
   131     forward_tac [@{thm OR4_parts_knows_Spy}]  (i+6) THEN
   132     forward_tac [@{thm OR2_parts_knows_Spy}]  (i+4)
   133 *}
   134  
   135 method_setup parts_explicit = {*
   136     Scan.succeed (K (SIMPLE_METHOD' parts_explicit_tac)) *}
   137   "to explicitly state that some message components belong to parts knows Spy"
   138 
   139 
   140 lemma Spy_see_shrK [simp]: 
   141     "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   142 by (erule orb.induct, parts_explicit, simp_all, blast+)
   143 
   144 lemma Spy_analz_shrK [simp]: 
   145 "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   146 by auto
   147 
   148 lemma Spy_see_shrK_D [dest!]:
   149      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> orb|] ==> A \<in> bad"
   150 by (blast dest: Spy_see_shrK)
   151 
   152 lemma new_keys_not_used [simp]:
   153    "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> orb\<rbrakk>  \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))"
   154 apply (erule rev_mp)
   155 apply (erule orb.induct, parts_explicit, simp_all)
   156 apply (force dest!: keysFor_parts_insert)
   157 apply (blast+)
   158 done
   159 
   160 
   161 
   162 subsection{* Proofs involving analz *}
   163 
   164 text{*Describes the form of K and NA when the Server sends this message.  Also
   165   for Oops case.*}
   166 lemma Says_Server_message_form: 
   167 "\<lbrakk>Says Server B  \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
   168      evs \<in> orb\<rbrakk>                                            
   169  \<Longrightarrow> K \<notin> range shrK & (\<exists> A Na. X=(Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
   170 by (erule rev_mp, erule orb.induct, simp_all)
   171 
   172 lemma Says_Server_imp_Gets: 
   173  "\<lbrakk>Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
   174                                              Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;
   175     evs \<in> orb\<rbrakk>
   176   \<Longrightarrow>  Gets Server \<lbrace>Nonce M, Agent A, Agent B, 
   177                    Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>, 
   178                Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
   179          \<in> set evs"
   180 by (erule rev_mp, erule orb.induct, simp_all)
   181 
   182 
   183 lemma A_trusts_OR1: 
   184 "\<lbrakk>Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);  
   185     A \<notin> bad; evs \<in> orb\<rbrakk>                   
   186  \<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"
   187 apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
   188 apply (blast)
   189 done
   190 
   191 
   192 lemma B_trusts_OR2:
   193  "\<lbrakk>Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>  
   194       \<in> parts (knows Spy evs);  B \<notin> bad; evs \<in> orb\<rbrakk>                   
   195   \<Longrightarrow> (\<exists> X. Says B Server \<lbrace>Nonce M, Agent A, Agent B, X,  
   196               Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
   197           \<in> set evs)"
   198 apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
   199 apply (blast+)
   200 done
   201 
   202 
   203 lemma B_trusts_OR3: 
   204 "\<lbrakk>Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace> \<in> parts (knows Spy evs);  
   205    B \<notin> bad; evs \<in> orb\<rbrakk>                   
   206 \<Longrightarrow> \<exists> M. Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> 
   207          \<in> set evs"
   208 apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
   209 apply (blast+)
   210 done
   211 
   212 lemma Gets_Server_message_form: 
   213 "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
   214     evs \<in> orb\<rbrakk>                                              
   215  \<Longrightarrow> (K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>)))    
   216              | X \<in> analz (knows Spy evs)"
   217 by (metis B_trusts_OR3 Crypt_Spy_analz_bad Gets_imp_Says MPair_analz MPair_parts
   218           Says_Server_message_form Says_imp_analz_Spy Says_imp_parts_knows_Spy)
   219 
   220 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;   
   221          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;  
   222     A \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow> B=B' & M=M'"
   223 by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
   224 
   225 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;   
   226          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;   
   227     B \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow>   M=M' & A=A' & X=X'"
   228 by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
   229 
   230 lemma analz_image_freshCryptK_lemma:
   231 "(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow>  
   232         (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)"
   233 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   234 
   235 ML
   236 {*
   237 structure OtwayReesBella =
   238 struct
   239 
   240 val analz_image_freshK_ss =
   241   simpset_of
   242    (@{context} delsimps [image_insert, image_Un]
   243       delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
   244       addsimps @{thms analz_image_freshK_simps})
   245 
   246 end
   247 *}
   248 
   249 method_setup analz_freshCryptK = {*
   250     Scan.succeed (fn ctxt =>
   251      (SIMPLE_METHOD
   252       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   253           REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
   254           ALLGOALS (asm_simp_tac
   255             (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))]))) *}
   256   "for proving useful rewrite rule"
   257 
   258 
   259 method_setup disentangle = {*
   260     Scan.succeed
   261      (fn ctxt => SIMPLE_METHOD
   262       (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
   263                    ORELSE' hyp_subst_tac ctxt))) *}
   264   "for eliminating conjunctions, disjunctions and the like"
   265 
   266 
   267 
   268 lemma analz_image_freshCryptK [rule_format]: 
   269 "evs \<in> orb \<Longrightarrow>                              
   270      Key K \<notin> analz (knows Spy evs) \<longrightarrow>  
   271        (\<forall> KK. KK \<subseteq> - (range shrK) \<longrightarrow>                  
   272              (Crypt K X \<in> analz (Key`KK \<union> (knows Spy evs))) =   
   273              (Crypt K X \<in> analz (knows Spy evs)))"
   274 apply (erule orb.induct)
   275 apply (analz_mono_contra)
   276 apply (frule_tac [7] Gets_Server_message_form)
   277 apply (frule_tac [9] Says_Server_message_form)
   278 apply disentangle
   279 apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN  analz.Snd])
   280 prefer 8 apply clarify
   281 apply (analz_freshCryptK, spy_analz, fastforce)
   282 done
   283 
   284 
   285 
   286 lemma analz_insert_freshCryptK: 
   287 "\<lbrakk>evs \<in> orb;  Key K \<notin> analz (knows Spy evs);  
   288          Seskey \<notin> range shrK\<rbrakk> \<Longrightarrow>   
   289          (Crypt K X \<in> analz (insert (Key Seskey) (knows Spy evs))) =  
   290          (Crypt K X \<in> analz (knows Spy evs))"
   291 by (simp only: analz_image_freshCryptK analz_image_freshK_simps)
   292 
   293 
   294 lemma analz_hard: 
   295 "\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
   296              Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
   297    Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace> \<in> analz (knows Spy evs);  
   298    A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>                   
   299  \<Longrightarrow>  Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs"
   300 apply (erule rev_mp)
   301 apply (erule rev_mp)
   302 apply (erule orb.induct)
   303 apply (frule_tac [7] Gets_Server_message_form)
   304 apply (frule_tac [9] Says_Server_message_form)
   305 apply disentangle
   306 txt{*letting the simplifier solve OR2*}
   307 apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd])
   308 apply (simp_all (no_asm_simp) add: analz_insert_eq pushes split_ifs)
   309 apply (spy_analz)
   310 txt{*OR1*}
   311 apply blast
   312 txt{*Oops*}
   313 prefer 4 apply (blast dest: analz_insert_freshCryptK)
   314 txt{*OR4 - ii*}
   315 prefer 3 apply (blast)
   316 txt{*OR3*}
   317 (*adding Gets_imp_ and Says_imp_ for efficiency*)
   318 apply (blast dest: 
   319        A_trusts_OR1 unique_Na Key_not_used analz_insert_freshCryptK)
   320 txt{*OR4 - i *}
   321 apply clarify
   322 apply (simp add: pushes split_ifs)
   323 apply (case_tac "Aaa\<in>bad")
   324 apply (blast dest: analz_insert_freshCryptK)
   325 apply clarify
   326 apply simp
   327 apply (case_tac "Ba\<in>bad")
   328 apply (frule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Decrypt, THEN analz.Fst] , assumption)
   329 apply (simp (no_asm_simp))
   330 apply clarify
   331 apply (frule Gets_imp_knows_Spy 
   332              [THEN parts.Inj, THEN parts.Snd, THEN B_trusts_OR3],  
   333        assumption, assumption, assumption, erule exE)
   334 apply (frule Says_Server_imp_Gets 
   335             [THEN Gets_imp_knows_Spy, THEN parts.Inj, THEN parts.Snd, 
   336             THEN parts.Snd, THEN parts.Snd, THEN parts.Fst, THEN A_trusts_OR1],
   337        assumption, assumption, assumption, assumption)
   338 apply (blast dest: Says_Server_imp_Gets B_trusts_OR2 unique_Na unique_Nb)
   339 done
   340 
   341 
   342 lemma Gets_Server_message_form': 
   343 "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace>  \<in> set evs;  
   344    B \<notin> bad; evs \<in> orb\<rbrakk>                              
   345   \<Longrightarrow> K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
   346 by (blast dest!: B_trusts_OR3 Says_Server_message_form)
   347 
   348 
   349 lemma OR4_imp_Gets: 
   350 "\<lbrakk>Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;   
   351    B \<notin> bad; evs \<in> orb\<rbrakk>  
   352  \<Longrightarrow> (\<exists> Nb. Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
   353                                              Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs)"
   354 apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
   355 prefer 3 apply (blast dest: Gets_Server_message_form')
   356 apply blast+
   357 done
   358 
   359 
   360 lemma A_keydist_to_B: 
   361 "\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
   362             Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
   363    Gets A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;    
   364    A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>  
   365   \<Longrightarrow> Key K \<in> analz (knows B evs)"
   366 apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
   367 apply (drule analz_hard, assumption, assumption, assumption, assumption)
   368 apply (drule OR4_imp_Gets, assumption, assumption)
   369 apply (fastforce dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
   370 done
   371 
   372 
   373 text{*Other properties as for the original protocol*}
   374 
   375 
   376 end