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