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