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