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