src/HOL/Auth/Yahalom2.thy
author paulson
Wed Apr 09 12:52:45 2003 +0200 (2003-04-09)
changeset 13907 2bc462b99e70
parent 13507 febb8e5d2a9d
child 13926 6e62e5357a10
permissions -rw-r--r--
tidying
     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{*Inductive Analysis of 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 "\<exists>X NB K. \<exists>evs \<in> yahalom.
    84              Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
    85 apply (intro exI bexI)
    86 apply (rule_tac [2] yahalom.Nil
    87                     [THEN yahalom.YM1, THEN yahalom.Reception,
    88                      THEN yahalom.YM2, THEN yahalom.Reception,
    89                      THEN yahalom.YM3, THEN yahalom.Reception,
    90                      THEN yahalom.YM4], possibility)
    91 done
    92 
    93 lemma Gets_imp_Says:
    94      "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
    95 by (erule rev_mp, erule yahalom.induct, auto)
    96 
    97 text{*Must be proved separately for each protocol*}
    98 lemma Gets_imp_knows_Spy:
    99      "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
   100 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   101 
   102 declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
   103 
   104 
   105 subsection{*Inductive Proofs*}
   106 
   107 text{*Result for reasoning about the encrypted portion of messages.
   108 Lets us treat YM4 using a similar argument as for the Fake case.*}
   109 lemma YM4_analz_knows_Spy:
   110      "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
   111       ==> X \<in> analz (knows Spy evs)"
   112 by blast
   113 
   114 lemmas YM4_parts_knows_Spy =
   115        YM4_analz_knows_Spy [THEN analz_into_parts, standard]
   116 
   117 
   118 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
   119     sends messages containing X! **)
   120 
   121 text{*Spy never sees a good agent's shared key!*}
   122 lemma Spy_see_shrK [simp]:
   123      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   124 by (erule yahalom.induct, force,
   125     drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
   126 
   127 lemma Spy_analz_shrK [simp]:
   128      "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   129 by auto
   130 
   131 lemma Spy_see_shrK_D [dest!]:
   132      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> yahalom|] ==> A \<in> bad"
   133 by (blast dest: Spy_see_shrK)
   134 
   135 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   136 lemma new_keys_not_used [rule_format, simp]:
   137  "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
   138 apply (erule yahalom.induct, force,
   139        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   140 (*Fake, YM3, YM4*)
   141 apply (blast dest!: keysFor_parts_insert)+
   142 done
   143 
   144 
   145 (*Describes the form of K when the Server sends this message.  Useful for
   146   Oops as well as main secrecy property.*)
   147 lemma Says_Server_message_form:
   148      "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|}
   149           \<in> set evs;  evs \<in> yahalom |]
   150       ==> K \<notin> range shrK"
   151 by (erule rev_mp, erule yahalom.induct, simp_all)
   152 
   153 
   154 (****
   155  The following is to prove theorems of the form
   156 
   157           Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
   158           Key K \<in> analz (knows Spy evs)
   159 
   160  A more general formula must be proved inductively.
   161 ****)
   162 
   163 (** Session keys are not used to encrypt other session keys **)
   164 
   165 lemma analz_image_freshK [rule_format]:
   166  "evs \<in> yahalom ==>
   167    \<forall>K KK. KK <= - (range shrK) -->
   168           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   169           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   170 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
   171        drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
   172 done
   173 
   174 lemma analz_insert_freshK:
   175      "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
   176       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   177       (K = KAB | Key K \<in> analz (knows Spy evs))"
   178 by (simp only: analz_image_freshK analz_image_freshK_simps)
   179 
   180 
   181 text{*The Key K uniquely identifies the Server's  message*}
   182 lemma unique_session_keys:
   183      "[| Says Server A
   184           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
   185         Says Server A'
   186           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \<in> set evs;
   187         evs \<in> yahalom |]
   188      ==> A=A' & B=B' & na=na' & nb=nb'"
   189 apply (erule rev_mp, erule rev_mp)
   190 apply (erule yahalom.induct, simp_all)
   191 txt{*YM3, by freshness*}
   192 apply blast
   193 done
   194 
   195 
   196 subsection{*Crucial Secrecy Property: Spy Does Not See Key @{term KAB}*}
   197 
   198 lemma secrecy_lemma:
   199      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   200       ==> Says Server A
   201             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   202                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   203            \<in> set evs -->
   204           Notes Spy {|na, nb, Key K|} \<notin> set evs -->
   205           Key K \<notin> analz (knows Spy evs)"
   206 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
   207        drule_tac [6] YM4_analz_knows_Spy)
   208 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)
   209 apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
   210 done
   211 
   212 
   213 (*Final version*)
   214 lemma Spy_not_see_encrypted_key:
   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          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   221       ==> Key K \<notin> analz (knows Spy evs)"
   222 by (blast dest: secrecy_lemma Says_Server_message_form)
   223 
   224 
   225 
   226 text{*This form is an immediate consequence of the previous result.  It is 
   227 similar to the assertions established by other methods.  It is equivalent
   228 to the previous result in that the Spy already has @{term analz} and
   229 @{term synth} at his disposal.  However, the conclusion 
   230 @{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
   231 other than Fake are trivial, while Fake requires 
   232 @{term "Key K \<notin> analz (knows Spy evs)"}. *}
   233 lemma Spy_not_know_encrypted_key:
   234      "[| Says Server A
   235             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   236                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   237          \<in> set evs;
   238          Notes Spy {|na, nb, Key K|} \<notin> set evs;
   239          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   240       ==> Key K \<notin> knows Spy evs"
   241 by (blast dest: Spy_not_see_encrypted_key)
   242 
   243 
   244 subsection{*Security Guarantee for A upon receiving YM3*}
   245 
   246 (*If the encrypted message appears then it originated with the Server.
   247   May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   248 lemma A_trusts_YM3:
   249      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   250          A \<notin> bad;  evs \<in> yahalom |]
   251       ==> \<exists>nb. Says Server A
   252                     {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   253                           Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   254                   \<in> set evs"
   255 apply (erule rev_mp)
   256 apply (erule yahalom.induct, force,
   257        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   258 txt{*Fake, YM3*}
   259 apply blast+
   260 done
   261 
   262 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   263 theorem A_gets_good_key:
   264      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   265          \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
   266          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   267       ==> Key K \<notin> analz (knows Spy evs)"
   268 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
   269 
   270 
   271 subsection{*Security Guarantee for B upon receiving YM4*}
   272 
   273 (*B knows, by the first part of A's message, that the Server distributed
   274   the key for A and B, and has associated it with NB.*)
   275 lemma B_trusts_YM4_shrK:
   276      "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   277            \<in> parts (knows Spy evs);
   278          B \<notin> bad;  evs \<in> yahalom |]
   279   ==> \<exists>NA. Says Server A
   280              {|Nonce NB,
   281                Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   282                Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
   283              \<in> set evs"
   284 apply (erule rev_mp)
   285 apply (erule yahalom.induct, force,
   286        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   287 (*Fake, YM3*)
   288 apply blast+
   289 done
   290 
   291 
   292 (*With this protocol variant, we don't need the 2nd part of YM4 at all:
   293   Nonce NB is available in the first part.*)
   294 
   295 (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   296   because we do not have to show that NB is secret. *)
   297 lemma B_trusts_YM4:
   298      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},  X|}
   299            \<in> set evs;
   300          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   301   ==> \<exists>NA. Says Server A
   302              {|Nonce NB,
   303                Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   304                Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
   305             \<in> set evs"
   306 by (blast dest!: B_trusts_YM4_shrK)
   307 
   308 
   309 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   310 theorem B_gets_good_key:
   311      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
   312            \<in> set evs;
   313          \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
   314          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   315       ==> Key K \<notin> analz (knows Spy evs)"
   316 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   317 
   318 
   319 subsection{*Authenticating B to A*}
   320 
   321 (*The encryption in message YM2 tells us it cannot be faked.*)
   322 lemma B_Said_YM2:
   323      "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
   324          B \<notin> bad;  evs \<in> yahalom |]
   325       ==> \<exists>NB. Says B Server {|Agent B, Nonce NB,
   326                                Crypt (shrK B) {|Agent A, Nonce NA|}|}
   327                       \<in> set evs"
   328 apply (erule rev_mp)
   329 apply (erule yahalom.induct, force,
   330        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   331 (*Fake, YM2*)
   332 apply blast+
   333 done
   334 
   335 
   336 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
   337 lemma YM3_auth_B_to_A_lemma:
   338      "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   339            \<in> set evs;
   340          B \<notin> bad;  evs \<in> yahalom |]
   341       ==> \<exists>nb'. Says B Server {|Agent B, nb',
   342                                    Crypt (shrK B) {|Agent A, Nonce NA|}|}
   343                        \<in> set evs"
   344 apply (erule rev_mp)
   345 apply (erule yahalom.induct, simp_all)
   346 (*Fake, YM2, YM3*)
   347 apply (blast dest!: B_Said_YM2)+
   348 done
   349 
   350 text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
   351 theorem YM3_auth_B_to_A:
   352      "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   353            \<in> set evs;
   354          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   355  ==> \<exists>nb'. Says B Server
   356                   {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|}
   357                \<in> set evs"
   358 by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
   359 
   360 
   361 subsection{*Authenticating A to B*}
   362 
   363 text{*using the certificate @{term "Crypt K (Nonce NB)"}*}
   364 
   365 (*Assuming the session key is secure, if both certificates are present then
   366   A has said NB.  We can't be sure about the rest of A's message, but only
   367   NB matters for freshness.  Note that  Key K \<notin> analz (knows Spy evs)  must be
   368   the FIRST antecedent of the induction formula.*)
   369 
   370 (*This lemma allows a use of unique_session_keys in the next proof,
   371   which otherwise is extremely slow.*)
   372 lemma secure_unique_session_keys:
   373      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
   374          Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
   375          Key K \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
   376      ==> A=A' & B=B'"
   377 by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad)
   378 
   379 
   380 lemma Auth_A_to_B_lemma [rule_format]:
   381      "evs \<in> yahalom
   382       ==> Key K \<notin> analz (knows Spy evs) -->
   383           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   384           Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   385             \<in> parts (knows Spy evs) -->
   386           B \<notin> bad -->
   387           (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
   388 apply (erule yahalom.induct, force,
   389        frule_tac [6] YM4_parts_knows_Spy)
   390 apply (analz_mono_contra, simp_all)
   391 (*Fake*)
   392 apply blast
   393 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   394 apply (force dest!: Crypt_imp_keysFor)
   395 (*YM4: was Crypt K (Nonce NB) the very last message?  If so, apply unicity
   396   of session keys; if not, use ind. hyp.*)
   397 apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys  )
   398 done
   399 
   400 
   401 text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   402   Moreover, A associates K with NB (thus is talking about the same run).
   403   Other premises guarantee secrecy of K.*}
   404 theorem YM4_imp_A_Said_YM3 [rule_format]:
   405      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
   406                   Crypt K (Nonce NB)|} \<in> set evs;
   407          (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
   408          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   409       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   410 by (blast intro: Auth_A_to_B_lemma
   411           dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)
   412 
   413 end