src/HOL/Auth/Yahalom2.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 16417 9bc16273c2d4
child 23746 a455e69c31cc
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     1 (*  Title:      HOL/Auth/Yahalom2
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 *)
     6 
     7 header{*The Yahalom Protocol, Variant 2*}
     8 
     9 theory Yahalom2 imports Public begin
    10 
    11 text{*
    12 This version trades encryption of NB for additional explicitness in YM3.
    13 Also in YM3, care is taken to make the two certificates distinct.
    14 
    15 From page 259 of
    16   Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    17   Proc. Royal Soc. 426
    18 
    19 This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
    20 *}
    21 
    22 consts  yahalom   :: "event list set"
    23 inductive "yahalom"
    24   intros
    25          (*Initial trace is empty*)
    26    Nil:  "[] \<in> yahalom"
    27 
    28          (*The spy MAY say anything he CAN say.  We do not expect him to
    29            invent new nonces here, but he can also use NS1.  Common to
    30            all similar protocols.*)
    31    Fake: "[| evsf \<in> yahalom;  X \<in> synth (analz (knows Spy evsf)) |]
    32           ==> Says Spy B X  # evsf \<in> yahalom"
    33 
    34          (*A message that has been sent can be received by the
    35            intended recipient.*)
    36    Reception: "[| evsr \<in> yahalom;  Says A B X \<in> set evsr |]
    37                ==> Gets B X # evsr \<in> yahalom"
    38 
    39          (*Alice initiates a protocol run*)
    40    YM1:  "[| evs1 \<in> yahalom;  Nonce NA \<notin> used evs1 |]
    41           ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
    42 
    43          (*Bob's response to Alice's message.*)
    44    YM2:  "[| evs2 \<in> yahalom;  Nonce NB \<notin> used evs2;
    45              Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
    46           ==> Says B Server
    47                   {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    48                 # evs2 \<in> yahalom"
    49 
    50          (*The Server receives Bob's message.  He responds by sending a
    51            new session key to Alice, with a certificate for forwarding to Bob.
    52            Both agents are quoted in the 2nd certificate to prevent attacks!*)
    53    YM3:  "[| evs3 \<in> yahalom;  Key KAB \<notin> used evs3;
    54              Gets Server {|Agent B, Nonce NB,
    55 			   Crypt (shrK B) {|Agent A, Nonce NA|}|}
    56                \<in> set evs3 |]
    57           ==> Says Server A
    58                {|Nonce NB,
    59                  Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
    60                  Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|}
    61                  # evs3 \<in> yahalom"
    62 
    63          (*Alice receives the Server's (?) message, checks her Nonce, and
    64            uses the new session key to send Bob his Nonce.*)
    65    YM4:  "[| evs4 \<in> yahalom;
    66              Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    67                       X|}  \<in> set evs4;
    68              Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
    69           ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
    70 
    71          (*This message models possible leaks of session keys.  The nonces
    72            identify the protocol run.  Quoting Server here ensures they are
    73            correct. *)
    74    Oops: "[| evso \<in> yahalom;
    75              Says Server A {|Nonce NB,
    76                              Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    77                              X|}  \<in> set evso |]
    78           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
    79 
    80 
    81 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    82 declare parts.Body  [dest]
    83 declare Fake_parts_insert_in_Un  [dest]
    84 declare analz_into_parts [dest]
    85 
    86 text{*A "possibility property": there are traces that reach the end*}
    87 lemma "Key K \<notin> used []
    88        ==> \<exists>X NB. \<exists>evs \<in> yahalom.
    89              Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
    90 apply (intro exI bexI)
    91 apply (rule_tac [2] yahalom.Nil
    92                     [THEN yahalom.YM1, THEN yahalom.Reception,
    93                      THEN yahalom.YM2, THEN yahalom.Reception,
    94                      THEN yahalom.YM3, THEN yahalom.Reception,
    95                      THEN yahalom.YM4])
    96 apply (possibility, simp add: used_Cons)
    97 done
    98 
    99 lemma Gets_imp_Says:
   100      "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
   101 by (erule rev_mp, erule yahalom.induct, auto)
   102 
   103 text{*Must be proved separately for each protocol*}
   104 lemma Gets_imp_knows_Spy:
   105      "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
   106 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   107 
   108 declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
   109 
   110 
   111 subsection{*Inductive Proofs*}
   112 
   113 text{*Result for reasoning about the encrypted portion of messages.
   114 Lets us treat YM4 using a similar argument as for the Fake case.*}
   115 lemma YM4_analz_knows_Spy:
   116      "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
   117       ==> X \<in> analz (knows Spy evs)"
   118 by blast
   119 
   120 lemmas YM4_parts_knows_Spy =
   121        YM4_analz_knows_Spy [THEN analz_into_parts, standard]
   122 
   123 
   124 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
   125     sends messages containing X! **)
   126 
   127 text{*Spy never sees a good agent's shared key!*}
   128 lemma Spy_see_shrK [simp]:
   129      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   130 by (erule yahalom.induct, force,
   131     drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
   132 
   133 lemma Spy_analz_shrK [simp]:
   134      "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   135 by auto
   136 
   137 lemma Spy_see_shrK_D [dest!]:
   138      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> yahalom|] ==> A \<in> bad"
   139 by (blast dest: Spy_see_shrK)
   140 
   141 text{*Nobody can have used non-existent keys!  
   142     Needed to apply @{text analz_insert_Key}*}
   143 lemma new_keys_not_used [simp]:
   144     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|]
   145      ==> K \<notin> keysFor (parts (spies evs))"
   146 apply (erule rev_mp)
   147 apply (erule yahalom.induct, force,
   148        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   149 txt{*Fake*}
   150 apply (force dest!: keysFor_parts_insert)
   151 txt{*YM3*}
   152 apply blast
   153 txt{*YM4*}
   154 apply auto
   155 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj])
   156 done
   157 
   158 
   159 text{*Describes the form of K when the Server sends this message.  Useful for
   160   Oops as well as main secrecy property.*}
   161 lemma Says_Server_message_form:
   162      "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|}
   163           \<in> set evs;  evs \<in> yahalom |]
   164       ==> K \<notin> range shrK"
   165 by (erule rev_mp, erule yahalom.induct, simp_all)
   166 
   167 
   168 (****
   169  The following is to prove theorems of the form
   170 
   171           Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
   172           Key K \<in> analz (knows Spy evs)
   173 
   174  A more general formula must be proved inductively.
   175 ****)
   176 
   177 (** Session keys are not used to encrypt other session keys **)
   178 
   179 lemma analz_image_freshK [rule_format]:
   180  "evs \<in> yahalom ==>
   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 yahalom.induct)
   185 apply (frule_tac [8] Says_Server_message_form)
   186 apply (drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
   187 done
   188 
   189 lemma analz_insert_freshK:
   190      "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
   191       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   192       (K = KAB | Key K \<in> analz (knows Spy evs))"
   193 by (simp only: analz_image_freshK analz_image_freshK_simps)
   194 
   195 
   196 text{*The Key K uniquely identifies the Server's  message*}
   197 lemma unique_session_keys:
   198      "[| Says Server A
   199           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
   200         Says Server A'
   201           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \<in> set evs;
   202         evs \<in> yahalom |]
   203      ==> A=A' & B=B' & na=na' & nb=nb'"
   204 apply (erule rev_mp, erule rev_mp)
   205 apply (erule yahalom.induct, simp_all)
   206 txt{*YM3, by freshness*}
   207 apply blast
   208 done
   209 
   210 
   211 subsection{*Crucial Secrecy Property: Spy Does Not See Key @{term KAB}*}
   212 
   213 lemma secrecy_lemma:
   214      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   215       ==> Says Server A
   216             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   217                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   218            \<in> set evs -->
   219           Notes Spy {|na, nb, Key K|} \<notin> set evs -->
   220           Key K \<notin> analz (knows Spy evs)"
   221 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
   222        drule_tac [6] YM4_analz_knows_Spy)
   223 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)
   224 apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
   225 done
   226 
   227 
   228 text{*Final version*}
   229 lemma Spy_not_see_encrypted_key:
   230      "[| Says Server A
   231             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   232                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   233          \<in> set evs;
   234          Notes Spy {|na, nb, Key K|} \<notin> set evs;
   235          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   236       ==> Key K \<notin> analz (knows Spy evs)"
   237 by (blast dest: secrecy_lemma Says_Server_message_form)
   238 
   239 
   240 
   241 text{*This form is an immediate consequence of the previous result.  It is
   242 similar to the assertions established by other methods.  It is equivalent
   243 to the previous result in that the Spy already has @{term analz} and
   244 @{term synth} at his disposal.  However, the conclusion
   245 @{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
   246 other than Fake are trivial, while Fake requires
   247 @{term "Key K \<notin> analz (knows Spy evs)"}. *}
   248 lemma Spy_not_know_encrypted_key:
   249      "[| Says Server A
   250             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   251                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   252          \<in> set evs;
   253          Notes Spy {|na, nb, Key K|} \<notin> set evs;
   254          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   255       ==> Key K \<notin> knows Spy evs"
   256 by (blast dest: Spy_not_see_encrypted_key)
   257 
   258 
   259 subsection{*Security Guarantee for A upon receiving YM3*}
   260 
   261 text{*If the encrypted message appears then it originated with the Server.
   262   May now apply @{text Spy_not_see_encrypted_key}, subject to its conditions.*}
   263 lemma A_trusts_YM3:
   264      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   265          A \<notin> bad;  evs \<in> yahalom |]
   266       ==> \<exists>nb. Says Server A
   267                     {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   268                           Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   269                   \<in> set evs"
   270 apply (erule rev_mp)
   271 apply (erule yahalom.induct, force,
   272        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   273 txt{*Fake, YM3*}
   274 apply blast+
   275 done
   276 
   277 text{*The obvious combination of @{text A_trusts_YM3} with 
   278 @{text Spy_not_see_encrypted_key}*}
   279 theorem A_gets_good_key:
   280      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   281          \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
   282          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   283       ==> Key K \<notin> analz (knows Spy evs)"
   284 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
   285 
   286 
   287 subsection{*Security Guarantee for B upon receiving YM4*}
   288 
   289 text{*B knows, by the first part of A's message, that the Server distributed
   290   the key for A and B, and has associated it with NB.*}
   291 lemma B_trusts_YM4_shrK:
   292      "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   293            \<in> parts (knows Spy evs);
   294          B \<notin> bad;  evs \<in> yahalom |]
   295   ==> \<exists>NA. Says Server A
   296              {|Nonce NB,
   297                Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   298                Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
   299              \<in> set evs"
   300 apply (erule rev_mp)
   301 apply (erule yahalom.induct, force,
   302        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   303 txt{*Fake, YM3*}
   304 apply blast+
   305 done
   306 
   307 
   308 text{*With this protocol variant, we don't need the 2nd part of YM4 at all:
   309   Nonce NB is available in the first part.*}
   310 
   311 text{*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   312   because we do not have to show that NB is secret. *}
   313 lemma B_trusts_YM4:
   314      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},  X|}
   315            \<in> set evs;
   316          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   317   ==> \<exists>NA. Says Server A
   318              {|Nonce NB,
   319                Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   320                Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
   321             \<in> set evs"
   322 by (blast dest!: B_trusts_YM4_shrK)
   323 
   324 
   325 text{*The obvious combination of @{text B_trusts_YM4} with 
   326 @{text Spy_not_see_encrypted_key}*}
   327 theorem B_gets_good_key:
   328      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
   329            \<in> set evs;
   330          \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
   331          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   332       ==> Key K \<notin> analz (knows Spy evs)"
   333 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   334 
   335 
   336 subsection{*Authenticating B to A*}
   337 
   338 text{*The encryption in message YM2 tells us it cannot be faked.*}
   339 lemma B_Said_YM2:
   340      "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
   341          B \<notin> bad;  evs \<in> yahalom |]
   342       ==> \<exists>NB. Says B Server {|Agent B, Nonce NB,
   343                                Crypt (shrK B) {|Agent A, Nonce NA|}|}
   344                       \<in> set evs"
   345 apply (erule rev_mp)
   346 apply (erule yahalom.induct, force,
   347        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   348 txt{*Fake, YM2*}
   349 apply blast+
   350 done
   351 
   352 
   353 text{*If the server sends YM3 then B sent YM2, perhaps with a different NB*}
   354 lemma YM3_auth_B_to_A_lemma:
   355      "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   356            \<in> set evs;
   357          B \<notin> bad;  evs \<in> yahalom |]
   358       ==> \<exists>nb'. Says B Server {|Agent B, nb',
   359                                    Crypt (shrK B) {|Agent A, Nonce NA|}|}
   360                        \<in> set evs"
   361 apply (erule rev_mp)
   362 apply (erule yahalom.induct, simp_all)
   363 txt{*Fake, YM2, YM3*}
   364 apply (blast dest!: B_Said_YM2)+
   365 done
   366 
   367 text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
   368 theorem YM3_auth_B_to_A:
   369      "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   370            \<in> set evs;
   371          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   372  ==> \<exists>nb'. Says B Server
   373                   {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|}
   374                \<in> set evs"
   375 by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
   376 
   377 
   378 subsection{*Authenticating A to B*}
   379 
   380 text{*using the certificate @{term "Crypt K (Nonce NB)"}*}
   381 
   382 text{*Assuming the session key is secure, if both certificates are present then
   383   A has said NB.  We can't be sure about the rest of A's message, but only
   384   NB matters for freshness.  Note that @{term "Key K \<notin> analz (knows Spy evs)"}
   385   must be the FIRST antecedent of the induction formula.*}
   386 
   387 text{*This lemma allows a use of @{text unique_session_keys} in the next proof,
   388   which otherwise is extremely slow.*}
   389 lemma secure_unique_session_keys:
   390      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
   391          Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
   392          Key K \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
   393      ==> A=A' & B=B'"
   394 by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad)
   395 
   396 
   397 lemma Auth_A_to_B_lemma [rule_format]:
   398      "evs \<in> yahalom
   399       ==> Key K \<notin> analz (knows Spy evs) -->
   400           K \<in> symKeys -->
   401           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   402           Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   403             \<in> parts (knows Spy evs) -->
   404           B \<notin> bad -->
   405           (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
   406 apply (erule yahalom.induct, force,
   407        frule_tac [6] YM4_parts_knows_Spy)
   408 apply (analz_mono_contra, simp_all)
   409 txt{*Fake*}
   410 apply blast
   411 txt{*YM3: by @{text new_keys_not_used}, the message
   412    @{term "Crypt K (Nonce NB)"} could not exist*}
   413 apply (force dest!: Crypt_imp_keysFor)
   414 txt{*YM4: was   @{term "Crypt K (Nonce NB)"} the very last message?  If so, 
   415     apply unicity of session keys; if not, use the induction hypothesis*}
   416 apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys)
   417 done
   418 
   419 
   420 text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   421   Moreover, A associates K with NB (thus is talking about the same run).
   422   Other premises guarantee secrecy of K.*}
   423 theorem YM4_imp_A_Said_YM3 [rule_format]:
   424      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
   425                   Crypt K (Nonce NB)|} \<in> set evs;
   426          (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
   427          K \<in> symKeys;  A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   428       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   429 by (blast intro: Auth_A_to_B_lemma
   430           dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)
   431 
   432 end