src/HOL/Auth/OtwayRees.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61956 38b73f7940af
child 63975 6728b5007ad0
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/Auth/OtwayRees.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1996  University of Cambridge
     4 *)
     5 
     6 section\<open>The Original Otway-Rees Protocol\<close>
     7 
     8 theory OtwayRees imports Public begin
     9 
    10 text\<open>From page 244 of
    11   Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    12   Proc. Royal Soc. 426
    13 
    14 This is the original version, which encrypts Nonce NB.\<close>
    15 
    16 inductive_set otway :: "event list set"
    17   where
    18          (*Initial trace is empty*)
    19    Nil:  "[] \<in> otway"
    20 
    21          (*The spy MAY say anything he CAN say.  We do not expect him to
    22            invent new nonces here, but he can also use NS1.  Common to
    23            all similar protocols.*)
    24  | Fake: "[| evsf \<in> otway;  X \<in> synth (analz (knows Spy evsf)) |]
    25           ==> Says Spy B X  # evsf \<in> otway"
    26 
    27          (*A message that has been sent can be received by the
    28            intended recipient.*)
    29  | Reception: "[| evsr \<in> otway;  Says A B X \<in>set evsr |]
    30                ==> Gets B X # evsr \<in> otway"
    31 
    32          (*Alice initiates a protocol run*)
    33  | OR1:  "[| evs1 \<in> otway;  Nonce NA \<notin> used evs1 |]
    34           ==> Says A B \<lbrace>Nonce NA, Agent A, Agent B,
    35                          Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace> \<rbrace>
    36                  # evs1 : otway"
    37 
    38          (*Bob's response to Alice's message.  Note that NB is encrypted.*)
    39  | OR2:  "[| evs2 \<in> otway;  Nonce NB \<notin> used evs2;
    40              Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> : set evs2 |]
    41           ==> Says B Server
    42                   \<lbrace>Nonce NA, Agent A, Agent B, X,
    43                     Crypt (shrK B)
    44                       \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
    45                  # evs2 : otway"
    46 
    47          (*The Server receives Bob's message and checks that the three NAs
    48            match.  Then he sends a new session key to Bob with a packet for
    49            forwarding to Alice.*)
    50  | OR3:  "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
    51              Gets Server
    52                   \<lbrace>Nonce NA, Agent A, Agent B,
    53                     Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>,
    54                     Crypt (shrK B) \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
    55                : set evs3 |]
    56           ==> Says Server B
    57                   \<lbrace>Nonce NA,
    58                     Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
    59                     Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace>
    60                  # evs3 : otway"
    61 
    62          (*Bob receives the Server's (?) message and compares the Nonces with
    63            those in the message he previously sent the Server.
    64            Need B \<noteq> Server because we allow messages to self.*)
    65  | OR4:  "[| evs4 \<in> otway;  B \<noteq> Server;
    66              Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X',
    67                              Crypt (shrK B)
    68                                    \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
    69                : set evs4;
    70              Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
    71                : set evs4 |]
    72           ==> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 : otway"
    73 
    74          (*This message models possible leaks of session keys.  The nonces
    75            identify the protocol run.*)
    76  | Oops: "[| evso \<in> otway;
    77              Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
    78                : set evso |]
    79           ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso : otway"
    80 
    81 
    82 declare Says_imp_analz_Spy [dest]
    83 declare parts.Body  [dest]
    84 declare analz_into_parts [dest]
    85 declare Fake_parts_insert_in_Un  [dest]
    86 
    87 
    88 text\<open>A "possibility property": there are traces that reach the end\<close>
    89 lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
    90       ==> \<exists>evs \<in> otway.
    91              Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace>
    92                \<in> set evs"
    93 apply (intro exI bexI)
    94 apply (rule_tac [2] otway.Nil
    95                     [THEN otway.OR1, THEN otway.Reception,
    96                      THEN otway.OR2, THEN otway.Reception,
    97                      THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) 
    98 apply (possibility, simp add: used_Cons) 
    99 done
   100 
   101 lemma Gets_imp_Says [dest!]:
   102      "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
   103 apply (erule rev_mp)
   104 apply (erule otway.induct, auto)
   105 done
   106 
   107 
   108 (** For reasoning about the encrypted portion of messages **)
   109 
   110 lemma OR2_analz_knows_Spy:
   111      "[| Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs;  evs \<in> otway |]
   112       ==> X \<in> analz (knows Spy evs)"
   113 by blast
   114 
   115 lemma OR4_analz_knows_Spy:
   116      "[| Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs;  evs \<in> otway |]
   117       ==> X \<in> analz (knows Spy evs)"
   118 by blast
   119 
   120 (*These lemmas assist simplification by removing forwarded X-variables.
   121   We can replace them by rewriting with parts_insert2 and proving using
   122   dest: parts_cut, but the proofs become more difficult.*)
   123 lemmas OR2_parts_knows_Spy =
   124     OR2_analz_knows_Spy [THEN analz_into_parts]
   125 
   126 (*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for
   127   some reason proofs work without them!*)
   128 
   129 
   130 text\<open>Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
   131 NOBODY sends messages containing X!\<close>
   132 
   133 text\<open>Spy never sees a good agent's shared key!\<close>
   134 lemma Spy_see_shrK [simp]:
   135      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   136 by (erule otway.induct, force,
   137     drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   138 
   139 
   140 lemma Spy_analz_shrK [simp]:
   141      "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   142 by auto
   143 
   144 lemma Spy_see_shrK_D [dest!]:
   145      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> otway|] ==> A \<in> bad"
   146 by (blast dest: Spy_see_shrK)
   147 
   148 
   149 subsection\<open>Towards Secrecy: Proofs Involving @{term analz}\<close>
   150 
   151 (*Describes the form of K and NA when the Server sends this message.  Also
   152   for Oops case.*)
   153 lemma Says_Server_message_form:
   154      "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
   155          evs \<in> otway |]
   156       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
   157 by (erule rev_mp, erule otway.induct, simp_all)
   158 
   159 
   160 (****
   161  The following is to prove theorems of the form
   162 
   163   Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
   164   Key K \<in> analz (knows Spy evs)
   165 
   166  A more general formula must be proved inductively.
   167 ****)
   168 
   169 
   170 text\<open>Session keys are not used to encrypt other session keys\<close>
   171 
   172 text\<open>The equality makes the induction hypothesis easier to apply\<close>
   173 lemma analz_image_freshK [rule_format]:
   174  "evs \<in> otway ==>
   175    \<forall>K KK. KK <= -(range shrK) -->
   176           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   177           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   178 apply (erule otway.induct)
   179 apply (frule_tac [8] Says_Server_message_form)
   180 apply (drule_tac [7] OR4_analz_knows_Spy)
   181 apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) 
   182 done
   183 
   184 lemma analz_insert_freshK:
   185   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
   186       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   187       (K = KAB | Key K \<in> analz (knows Spy evs))"
   188 by (simp only: analz_image_freshK analz_image_freshK_simps)
   189 
   190 
   191 text\<open>The Key K uniquely identifies the Server's  message.\<close>
   192 lemma unique_session_keys:
   193      "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace>   \<in> set evs;
   194          Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs;
   195          evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
   196 apply (erule rev_mp)
   197 apply (erule rev_mp)
   198 apply (erule otway.induct, simp_all)
   199 apply blast+  \<comment>\<open>OR3 and OR4\<close>
   200 done
   201 
   202 
   203 subsection\<open>Authenticity properties relating to NA\<close>
   204 
   205 text\<open>Only OR1 can have caused such a part of a message to appear.\<close>
   206 lemma Crypt_imp_OR1 [rule_format]:
   207  "[| A \<notin> bad;  evs \<in> otway |]
   208   ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) -->
   209       Says A B \<lbrace>NA, Agent A, Agent B,
   210                  Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
   211         \<in> set evs"
   212 by (erule otway.induct, force,
   213     drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   214 
   215 lemma Crypt_imp_OR1_Gets:
   216      "[| Gets B \<lbrace>NA, Agent A, Agent B,
   217                   Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
   218          A \<notin> bad; evs \<in> otway |]
   219        ==> Says A B \<lbrace>NA, Agent A, Agent B,
   220                       Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
   221              \<in> set evs"
   222 by (blast dest: Crypt_imp_OR1)
   223 
   224 
   225 text\<open>The Nonce NA uniquely identifies A's message\<close>
   226 lemma unique_NA:
   227      "[| Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
   228          Crypt (shrK A) \<lbrace>NA, Agent A, Agent C\<rbrace> \<in> parts (knows Spy evs);
   229          evs \<in> otway;  A \<notin> bad |]
   230       ==> B = C"
   231 apply (erule rev_mp, erule rev_mp)
   232 apply (erule otway.induct, force,
   233        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   234 done
   235 
   236 
   237 text\<open>It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   238   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   239   over-simplified version of this protocol: see \<open>OtwayRees_Bad\<close>.\<close>
   240 lemma no_nonce_OR1_OR2:
   241    "[| Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
   242        A \<notin> bad;  evs \<in> otway |]
   243     ==> Crypt (shrK A) \<lbrace>NA', NA, Agent A', Agent A\<rbrace> \<notin> parts (knows Spy evs)"
   244 apply (erule rev_mp)
   245 apply (erule otway.induct, force,
   246        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   247 done
   248 
   249 text\<open>Crucial property: If the encrypted message appears, and A has used NA
   250   to start a run, then it originated with the Server!\<close>
   251 lemma NA_Crypt_imp_Server_msg [rule_format]:
   252      "[| A \<notin> bad;  evs \<in> otway |]
   253       ==> Says A B \<lbrace>NA, Agent A, Agent B,
   254                      Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs -->
   255           Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs)
   256           --> (\<exists>NB. Says Server B
   257                          \<lbrace>NA,
   258                            Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
   259                            Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)"
   260 apply (erule otway.induct, force,
   261        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
   262 apply blast  \<comment>\<open>OR1: by freshness\<close>
   263 apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA)  \<comment>\<open>OR3\<close>
   264 apply (blast intro!: Crypt_imp_OR1)  \<comment>\<open>OR4\<close>
   265 done
   266 
   267 
   268 text\<open>Corollary: if A receives B's OR4 message and the nonce NA agrees
   269   then the key really did come from the Server!  CANNOT prove this of the
   270   bad form of this protocol, even though we can prove
   271   \<open>Spy_not_see_encrypted_key\<close>\<close>
   272 lemma A_trusts_OR4:
   273      "[| Says A  B \<lbrace>NA, Agent A, Agent B,
   274                      Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
   275          Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
   276      A \<notin> bad;  evs \<in> otway |]
   277   ==> \<exists>NB. Says Server B
   278                \<lbrace>NA,
   279                  Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
   280                  Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
   281                  \<in> set evs"
   282 by (blast intro!: NA_Crypt_imp_Server_msg)
   283 
   284 
   285 text\<open>Crucial secrecy property: Spy does not see the keys sent in msg OR3
   286     Does not in itself guarantee security: an attack could violate
   287     the premises, e.g. by having @{term "A=Spy"}\<close>
   288 lemma secrecy_lemma:
   289  "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   290   ==> Says Server B
   291         \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
   292           Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs -->
   293       Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
   294       Key K \<notin> analz (knows Spy evs)"
   295 apply (erule otway.induct, force)
   296 apply (frule_tac [7] Says_Server_message_form)
   297 apply (drule_tac [6] OR4_analz_knows_Spy)
   298 apply (drule_tac [4] OR2_analz_knows_Spy)
   299 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
   300 apply spy_analz  \<comment>\<open>Fake\<close>
   301 apply (blast dest: unique_session_keys)+  \<comment>\<open>OR3, OR4, Oops\<close>
   302 done
   303 
   304 theorem Spy_not_see_encrypted_key:
   305      "[| Says Server B
   306           \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
   307                 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
   308          Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   309          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   310       ==> Key K \<notin> analz (knows Spy evs)"
   311 by (blast dest: Says_Server_message_form secrecy_lemma)
   312 
   313 text\<open>This form is an immediate consequence of the previous result.  It is 
   314 similar to the assertions established by other methods.  It is equivalent
   315 to the previous result in that the Spy already has @{term analz} and
   316 @{term synth} at his disposal.  However, the conclusion 
   317 @{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
   318 other than Fake are trivial, while Fake requires 
   319 @{term "Key K \<notin> analz (knows Spy evs)"}.\<close>
   320 lemma Spy_not_know_encrypted_key:
   321      "[| Says Server B
   322           \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
   323                 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
   324          Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   325          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   326       ==> Key K \<notin> knows Spy evs"
   327 by (blast dest: Spy_not_see_encrypted_key)
   328 
   329 
   330 text\<open>A's guarantee.  The Oops premise quantifies over NB because A cannot know
   331   what it is.\<close>
   332 lemma A_gets_good_key:
   333      "[| Says A  B \<lbrace>NA, Agent A, Agent B,
   334                      Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
   335          Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
   336          \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   337          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   338       ==> Key K \<notin> analz (knows Spy evs)"
   339 by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
   340 
   341 
   342 subsection\<open>Authenticity properties relating to NB\<close>
   343 
   344 text\<open>Only OR2 can have caused such a part of a message to appear.  We do not
   345   know anything about X: it does NOT have to have the right form.\<close>
   346 lemma Crypt_imp_OR2:
   347      "[| Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
   348          B \<notin> bad;  evs \<in> otway |]
   349       ==> \<exists>X. Says B Server
   350                  \<lbrace>NA, Agent A, Agent B, X,
   351                    Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
   352                  \<in> set evs"
   353 apply (erule rev_mp)
   354 apply (erule otway.induct, force,
   355        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   356 done
   357 
   358 
   359 text\<open>The Nonce NB uniquely identifies B's  message\<close>
   360 lemma unique_NB:
   361      "[| Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts(knows Spy evs);
   362          Crypt (shrK B) \<lbrace>NC, NB, Agent C, Agent B\<rbrace> \<in> parts(knows Spy evs);
   363            evs \<in> otway;  B \<notin> bad |]
   364          ==> NC = NA & C = A"
   365 apply (erule rev_mp, erule rev_mp)
   366 apply (erule otway.induct, force,
   367        drule_tac [4] OR2_parts_knows_Spy, simp_all)
   368 apply blast+  \<comment>\<open>Fake, OR2\<close>
   369 done
   370 
   371 text\<open>If the encrypted message appears, and B has used Nonce NB,
   372   then it originated with the Server!  Quite messy proof.\<close>
   373 lemma NB_Crypt_imp_Server_msg [rule_format]:
   374  "[| B \<notin> bad;  evs \<in> otway |]
   375   ==> Crypt (shrK B) \<lbrace>NB, Key K\<rbrace> \<in> parts (knows Spy evs)
   376       --> (\<forall>X'. Says B Server
   377                      \<lbrace>NA, Agent A, Agent B, X',
   378                        Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
   379            \<in> set evs
   380            --> Says Server B
   381                 \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
   382                       Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
   383                     \<in> set evs)"
   384 apply simp
   385 apply (erule otway.induct, force,
   386        drule_tac [4] OR2_parts_knows_Spy, simp_all)
   387 apply blast  \<comment>\<open>Fake\<close>
   388 apply blast  \<comment>\<open>OR2\<close>
   389 apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2)  \<comment>\<open>OR3\<close>
   390 apply (blast dest!: Crypt_imp_OR2)  \<comment>\<open>OR4\<close>
   391 done
   392 
   393 
   394 text\<open>Guarantee for B: if it gets a message with matching NB then the Server
   395   has sent the correct message.\<close>
   396 theorem B_trusts_OR3:
   397      "[| Says B Server \<lbrace>NA, Agent A, Agent B, X',
   398                          Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
   399            \<in> set evs;
   400          Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
   401          B \<notin> bad;  evs \<in> otway |]
   402       ==> Says Server B
   403                \<lbrace>NA,
   404                  Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
   405                  Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
   406                  \<in> set evs"
   407 by (blast intro!: NB_Crypt_imp_Server_msg)
   408 
   409 
   410 text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with 
   411       \<open>Spy_not_see_encrypted_key\<close>\<close>
   412 lemma B_gets_good_key:
   413      "[| Says B Server \<lbrace>NA, Agent A, Agent B, X',
   414                          Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
   415            \<in> set evs;
   416          Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
   417          Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   418          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   419       ==> Key K \<notin> analz (knows Spy evs)"
   420 by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key)
   421 
   422 
   423 lemma OR3_imp_OR2:
   424      "[| Says Server B
   425               \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
   426                 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
   427          B \<notin> bad;  evs \<in> otway |]
   428   ==> \<exists>X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
   429                             Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
   430               \<in> set evs"
   431 apply (erule rev_mp)
   432 apply (erule otway.induct, simp_all)
   433 apply (blast dest!: Crypt_imp_OR2)+
   434 done
   435 
   436 
   437 text\<open>After getting and checking OR4, agent A can trust that B has been active.
   438   We could probably prove that X has the expected form, but that is not
   439   strictly necessary for authentication.\<close>
   440 theorem A_auths_B:
   441      "[| Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
   442          Says A  B \<lbrace>NA, Agent A, Agent B,
   443                      Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
   444          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   445   ==> \<exists>NB X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
   446                                Crypt (shrK B)  \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
   447                  \<in> set evs"
   448 by (blast dest!: A_trusts_OR4 OR3_imp_OR2)
   449 
   450 end