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