src/HOL/Auth/Yahalom2.thy
author wenzelm
Wed Oct 03 20:54:16 2001 +0200 (2001-10-03)
changeset 11655 923e4d0d36d5
parent 11251 a6816d47f41d
child 13507 febb8e5d2a9d
permissions -rw-r--r--
tuned parentheses in relational expressions;
     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 Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
     7 
     8 This version trades encryption of NB for additional explicitness in YM3.
     9 Also in YM3, care is taken to make the two certificates distinct.
    10 
    11 From page 259 of
    12   Burrows, Abadi and Needham.  A Logic of Authentication.
    13   Proc. Royal Soc. 426 (1989)
    14 *)
    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 (*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])
    91 apply possibility
    92 done
    93 
    94 lemma Gets_imp_Says:
    95      "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
    96 by (erule rev_mp, erule yahalom.induct, auto)
    97 
    98 (*Must be proved separately for each protocol*)
    99 lemma Gets_imp_knows_Spy:
   100      "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
   101 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   102 
   103 declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
   104 
   105 
   106 (**** Inductive proofs about yahalom ****)
   107 
   108 (** For reasoning about the encrypted portion of messages **)
   109 
   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 (*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 apply (erule yahalom.induct, force,
   127        drule_tac [6] YM4_parts_knows_Spy, simp_all)
   128 apply blast+
   129 done
   130 
   131 lemma Spy_analz_shrK [simp]:
   132      "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   133 by auto
   134 
   135 lemma Spy_see_shrK_D [dest!]:
   136      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> yahalom|] ==> A \<in> bad"
   137 by (blast dest: Spy_see_shrK)
   138 
   139 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   140 lemma new_keys_not_used [rule_format, simp]:
   141  "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
   142 apply (erule yahalom.induct, force,
   143        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   144 (*Fake, YM3, YM4*)
   145 apply (blast dest!: keysFor_parts_insert)+
   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)
   176 apply analz_freshK
   177 apply spy_analz
   178 done
   179 
   180 lemma analz_insert_freshK:
   181      "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
   182       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   183       (K = KAB | Key K \<in> analz (knows Spy evs))"
   184 by (simp only: analz_image_freshK analz_image_freshK_simps)
   185 
   186 
   187 (*** The Key K uniquely identifies the Server's  message. **)
   188 
   189 lemma unique_session_keys:
   190      "[| Says Server A
   191           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
   192         Says Server A'
   193           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \<in> set evs;
   194         evs \<in> yahalom |]
   195      ==> A=A' & B=B' & na=na' & nb=nb'"
   196 apply (erule rev_mp, erule rev_mp)
   197 apply (erule yahalom.induct, simp_all)
   198 (*YM3, by freshness*)
   199 apply blast
   200 done
   201 
   202 
   203 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   204 
   205 lemma secrecy_lemma:
   206      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   207       ==> Says Server A
   208             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   209                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   210            \<in> set evs -->
   211           Notes Spy {|na, nb, Key K|} \<notin> set evs -->
   212           Key K \<notin> analz (knows Spy evs)"
   213 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
   214        drule_tac [6] YM4_analz_knows_Spy)
   215 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
   216 apply spy_analz  (*Fake*)
   217 apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
   218 done
   219 
   220 
   221 (*Final version*)
   222 lemma Spy_not_see_encrypted_key:
   223      "[| Says Server A
   224             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   225                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   226          \<in> set evs;
   227          Notes Spy {|na, nb, Key K|} \<notin> set evs;
   228          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   229       ==> Key K \<notin> analz (knows Spy evs)"
   230 by (blast dest: secrecy_lemma Says_Server_message_form)
   231 
   232 
   233 (** Security Guarantee for A upon receiving YM3 **)
   234 
   235 (*If the encrypted message appears then it originated with the Server.
   236   May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   237 lemma A_trusts_YM3:
   238      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   239          A \<notin> bad;  evs \<in> yahalom |]
   240       ==> \<exists>nb. Says Server A
   241                     {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   242                           Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   243                   \<in> set evs"
   244 apply (erule rev_mp)
   245 apply (erule yahalom.induct, force,
   246        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   247 (*Fake, YM3*)
   248 apply blast+
   249 done
   250 
   251 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   252 lemma A_gets_good_key:
   253      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   254          \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
   255          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   256       ==> Key K \<notin> analz (knows Spy evs)"
   257 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
   258 
   259 
   260 (** Security Guarantee for B upon receiving YM4 **)
   261 
   262 (*B knows, by the first part of A's message, that the Server distributed
   263   the key for A and B, and has associated it with NB.*)
   264 lemma B_trusts_YM4_shrK:
   265      "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   266            \<in> parts (knows Spy evs);
   267          B \<notin> bad;  evs \<in> yahalom |]
   268   ==> \<exists>NA. Says Server A
   269              {|Nonce NB,
   270                Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   271                Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
   272              \<in> set evs"
   273 apply (erule rev_mp)
   274 apply (erule yahalom.induct, force,
   275        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   276 (*Fake, YM3*)
   277 apply blast+
   278 done
   279 
   280 
   281 (*With this protocol variant, we don't need the 2nd part of YM4 at all:
   282   Nonce NB is available in the first part.*)
   283 
   284 (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   285   because we do not have to show that NB is secret. *)
   286 lemma B_trusts_YM4:
   287      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},  X|}
   288            \<in> set evs;
   289          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   290   ==> \<exists>NA. Says Server A
   291              {|Nonce NB,
   292                Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   293                Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
   294             \<in> set evs"
   295 by (blast dest!: B_trusts_YM4_shrK)
   296 
   297 
   298 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   299 lemma B_gets_good_key:
   300      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
   301            \<in> set evs;
   302          \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
   303          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   304       ==> Key K \<notin> analz (knows Spy evs)"
   305 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   306 
   307 
   308 (*** Authenticating B to A ***)
   309 
   310 (*The encryption in message YM2 tells us it cannot be faked.*)
   311 lemma B_Said_YM2:
   312      "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
   313          B \<notin> bad;  evs \<in> yahalom |]
   314       ==> \<exists>NB. Says B Server {|Agent B, Nonce NB,
   315                                Crypt (shrK B) {|Agent A, Nonce NA|}|}
   316                       \<in> set evs"
   317 apply (erule rev_mp)
   318 apply (erule yahalom.induct, force,
   319        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   320 (*Fake, YM2*)
   321 apply blast+
   322 done
   323 
   324 
   325 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
   326 lemma YM3_auth_B_to_A_lemma:
   327      "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   328            \<in> set evs;
   329          B \<notin> bad;  evs \<in> yahalom |]
   330       ==> \<exists>nb'. Says B Server {|Agent B, nb',
   331                                    Crypt (shrK B) {|Agent A, Nonce NA|}|}
   332                        \<in> set evs"
   333 apply (erule rev_mp)
   334 apply (erule yahalom.induct, simp_all)
   335 (*Fake, YM2, YM3*)
   336 apply (blast dest!: B_Said_YM2)+
   337 done
   338 
   339 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   340 lemma YM3_auth_B_to_A:
   341      "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   342            \<in> set evs;
   343          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   344  ==> \<exists>nb'. Says B Server
   345                   {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|}
   346                \<in> set evs"
   347 by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
   348 
   349 
   350 
   351 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   352 
   353 (*Assuming the session key is secure, if both certificates are present then
   354   A has said NB.  We can't be sure about the rest of A's message, but only
   355   NB matters for freshness.  Note that  Key K \<notin> analz (knows Spy evs)  must be
   356   the FIRST antecedent of the induction formula.*)
   357 
   358 (*This lemma allows a use of unique_session_keys in the next proof,
   359   which otherwise is extremely slow.*)
   360 lemma secure_unique_session_keys:
   361      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
   362          Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
   363          Key K \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
   364      ==> A=A' & B=B'"
   365 by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad)
   366 
   367 
   368 lemma Auth_A_to_B_lemma [rule_format]:
   369      "evs \<in> yahalom
   370       ==> Key K \<notin> analz (knows Spy evs) -->
   371           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   372           Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   373             \<in> parts (knows Spy evs) -->
   374           B \<notin> bad -->
   375           (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
   376 apply (erule yahalom.induct, force,
   377        frule_tac [6] YM4_parts_knows_Spy)
   378 apply (analz_mono_contra, simp_all)
   379 (*Fake*)
   380 apply blast
   381 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   382 apply (force dest!: Crypt_imp_keysFor)
   383 (*YM4: was Crypt K (Nonce NB) the very last message?  If so, apply unicity
   384   of session keys; if not, use ind. hyp.*)
   385 apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys  )
   386 done
   387 
   388 
   389 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   390   Moreover, A associates K with NB (thus is talking about the same run).
   391   Other premises guarantee secrecy of K.*)
   392 lemma YM4_imp_A_Said_YM3 [rule_format]:
   393      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
   394                   Crypt K (Nonce NB)|} \<in> set evs;
   395          (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
   396          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   397       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   398 by (blast intro: Auth_A_to_B_lemma
   399           dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)
   400 
   401 end