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