src/HOL/Auth/Yahalom2.thy
author paulson
Mon May 05 18:22:01 2003 +0200 (2003-05-05)
changeset 13956 8fe7e12290e1
parent 13926 6e62e5357a10
child 14200 d8598e24f8fa
permissions -rw-r--r--
improved presentation of HOL/Auth theories
     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 "\<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 txt{*Fake*}
   141 apply (force dest!: keysFor_parts_insert)
   142 txt{*YM3, YM4*}
   143 apply blast+
   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 text{*The Key K uniquely identifies the Server's  message*}
   184 lemma unique_session_keys:
   185      "[| Says Server A
   186           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
   187         Says Server A'
   188           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \<in> set evs;
   189         evs \<in> yahalom |]
   190      ==> A=A' & B=B' & na=na' & nb=nb'"
   191 apply (erule rev_mp, erule rev_mp)
   192 apply (erule yahalom.induct, simp_all)
   193 txt{*YM3, by freshness*}
   194 apply blast
   195 done
   196 
   197 
   198 subsection{*Crucial Secrecy Property: Spy Does Not See Key @{term KAB}*}
   199 
   200 lemma secrecy_lemma:
   201      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   202       ==> Says Server A
   203             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   204                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   205            \<in> set evs -->
   206           Notes Spy {|na, nb, Key K|} \<notin> set evs -->
   207           Key K \<notin> analz (knows Spy evs)"
   208 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
   209        drule_tac [6] YM4_analz_knows_Spy)
   210 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)
   211 apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
   212 done
   213 
   214 
   215 (*Final version*)
   216 lemma Spy_not_see_encrypted_key:
   217      "[| Says Server A
   218             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   219                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   220          \<in> set evs;
   221          Notes Spy {|na, nb, Key K|} \<notin> set evs;
   222          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   223       ==> Key K \<notin> analz (knows Spy evs)"
   224 by (blast dest: secrecy_lemma Says_Server_message_form)
   225 
   226 
   227 
   228 text{*This form is an immediate consequence of the previous result.  It is 
   229 similar to the assertions established by other methods.  It is equivalent
   230 to the previous result in that the Spy already has @{term analz} and
   231 @{term synth} at his disposal.  However, the conclusion 
   232 @{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
   233 other than Fake are trivial, while Fake requires 
   234 @{term "Key K \<notin> analz (knows Spy evs)"}. *}
   235 lemma Spy_not_know_encrypted_key:
   236      "[| Says Server A
   237             {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   238                   Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   239          \<in> set evs;
   240          Notes Spy {|na, nb, Key K|} \<notin> set evs;
   241          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   242       ==> Key K \<notin> knows Spy evs"
   243 by (blast dest: Spy_not_see_encrypted_key)
   244 
   245 
   246 subsection{*Security Guarantee for A upon receiving YM3*}
   247 
   248 (*If the encrypted message appears then it originated with the Server.
   249   May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   250 lemma A_trusts_YM3:
   251      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   252          A \<notin> bad;  evs \<in> yahalom |]
   253       ==> \<exists>nb. Says Server A
   254                     {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   255                           Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   256                   \<in> set evs"
   257 apply (erule rev_mp)
   258 apply (erule yahalom.induct, force,
   259        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   260 txt{*Fake, YM3*}
   261 apply blast+
   262 done
   263 
   264 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   265 theorem A_gets_good_key:
   266      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   267          \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
   268          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   269       ==> Key K \<notin> analz (knows Spy evs)"
   270 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
   271 
   272 
   273 subsection{*Security Guarantee for B upon receiving YM4*}
   274 
   275 (*B knows, by the first part of A's message, that the Server distributed
   276   the key for A and B, and has associated it with NB.*)
   277 lemma B_trusts_YM4_shrK:
   278      "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   279            \<in> parts (knows Spy evs);
   280          B \<notin> bad;  evs \<in> yahalom |]
   281   ==> \<exists>NA. Says Server A
   282              {|Nonce NB,
   283                Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   284                Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
   285              \<in> set evs"
   286 apply (erule rev_mp)
   287 apply (erule yahalom.induct, force,
   288        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   289 (*Fake, YM3*)
   290 apply blast+
   291 done
   292 
   293 
   294 (*With this protocol variant, we don't need the 2nd part of YM4 at all:
   295   Nonce NB is available in the first part.*)
   296 
   297 (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   298   because we do not have to show that NB is secret. *)
   299 lemma B_trusts_YM4:
   300      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},  X|}
   301            \<in> set evs;
   302          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   303   ==> \<exists>NA. Says Server A
   304              {|Nonce NB,
   305                Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   306                Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
   307             \<in> set evs"
   308 by (blast dest!: B_trusts_YM4_shrK)
   309 
   310 
   311 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   312 theorem B_gets_good_key:
   313      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
   314            \<in> set evs;
   315          \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
   316          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   317       ==> Key K \<notin> analz (knows Spy evs)"
   318 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   319 
   320 
   321 subsection{*Authenticating B to A*}
   322 
   323 (*The encryption in message YM2 tells us it cannot be faked.*)
   324 lemma B_Said_YM2:
   325      "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
   326          B \<notin> bad;  evs \<in> yahalom |]
   327       ==> \<exists>NB. Says B Server {|Agent B, Nonce NB,
   328                                Crypt (shrK B) {|Agent A, Nonce NA|}|}
   329                       \<in> set evs"
   330 apply (erule rev_mp)
   331 apply (erule yahalom.induct, force,
   332        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   333 (*Fake, YM2*)
   334 apply blast+
   335 done
   336 
   337 
   338 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
   339 lemma YM3_auth_B_to_A_lemma:
   340      "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   341            \<in> set evs;
   342          B \<notin> bad;  evs \<in> yahalom |]
   343       ==> \<exists>nb'. Says B Server {|Agent B, nb',
   344                                    Crypt (shrK B) {|Agent A, Nonce NA|}|}
   345                        \<in> set evs"
   346 apply (erule rev_mp)
   347 apply (erule yahalom.induct, simp_all)
   348 (*Fake, YM2, YM3*)
   349 apply (blast dest!: B_Said_YM2)+
   350 done
   351 
   352 text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
   353 theorem YM3_auth_B_to_A:
   354      "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   355            \<in> set evs;
   356          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   357  ==> \<exists>nb'. Says B Server
   358                   {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|}
   359                \<in> set evs"
   360 by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
   361 
   362 
   363 subsection{*Authenticating A to B*}
   364 
   365 text{*using the certificate @{term "Crypt K (Nonce NB)"}*}
   366 
   367 (*Assuming the session key is secure, if both certificates are present then
   368   A has said NB.  We can't be sure about the rest of A's message, but only
   369   NB matters for freshness.  Note that  Key K \<notin> analz (knows Spy evs)  must be
   370   the FIRST antecedent of the induction formula.*)
   371 
   372 (*This lemma allows a use of unique_session_keys in the next proof,
   373   which otherwise is extremely slow.*)
   374 lemma secure_unique_session_keys:
   375      "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
   376          Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
   377          Key K \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
   378      ==> A=A' & B=B'"
   379 by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad)
   380 
   381 
   382 lemma Auth_A_to_B_lemma [rule_format]:
   383      "evs \<in> yahalom
   384       ==> Key K \<notin> analz (knows Spy evs) -->
   385           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   386           Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   387             \<in> parts (knows Spy evs) -->
   388           B \<notin> bad -->
   389           (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
   390 apply (erule yahalom.induct, force,
   391        frule_tac [6] YM4_parts_knows_Spy)
   392 apply (analz_mono_contra, simp_all)
   393 (*Fake*)
   394 apply blast
   395 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   396 apply (force dest!: Crypt_imp_keysFor)
   397 (*YM4: was Crypt K (Nonce NB) the very last message?  If so, apply unicity
   398   of session keys; if not, use ind. hyp.*)
   399 apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
   400 done
   401 
   402 
   403 text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   404   Moreover, A associates K with NB (thus is talking about the same run).
   405   Other premises guarantee secrecy of K.*}
   406 theorem YM4_imp_A_Said_YM3 [rule_format]:
   407      "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
   408                   Crypt K (Nonce NB)|} \<in> set evs;
   409          (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
   410          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   411       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   412 by (blast intro: Auth_A_to_B_lemma
   413           dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)
   414 
   415 end