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