src/HOL/Auth/Yahalom_Bad.thy
author berghofe
Wed Jul 11 11:14:51 2007 +0200 (2007-07-11)
changeset 23746 a455e69c31cc
parent 16417 9bc16273c2d4
child 37936 1e4c5015a72e
permissions -rw-r--r--
Adapted to new inductive definition package.
     1 (*  Title:      HOL/Auth/Yahalom
     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: A Flawed Version*}
     8 
     9 theory Yahalom_Bad imports Public begin
    10 
    11 text{*
    12 Demonstrates of why Oops is necessary.  This protocol can be attacked because
    13 it doesn't keep NB secret, but without Oops it can be "verified" anyway.
    14 The issues are discussed in lcp's LICS 2000 invited lecture.
    15 *}
    16 
    17 inductive_set yahalom :: "event list set"
    18   where
    19          (*Initial trace is empty*)
    20    Nil:  "[] \<in> yahalom"
    21 
    22          (*The spy MAY say anything he CAN say.  We do not expect him to
    23            invent new nonces here, but he can also use NS1.  Common to
    24            all similar protocols.*)
    25  | Fake: "[| evsf \<in> yahalom;  X \<in> synth (analz (knows Spy evsf)) |]
    26           ==> Says Spy B X  # evsf \<in> yahalom"
    27 
    28          (*A message that has been sent can be received by the
    29            intended recipient.*)
    30  | Reception: "[| evsr \<in> yahalom;  Says A B X \<in> set evsr |]
    31                ==> Gets B X # evsr \<in> yahalom"
    32 
    33          (*Alice initiates a protocol run*)
    34  | YM1:  "[| evs1 \<in> yahalom;  Nonce NA \<notin> used evs1 |]
    35           ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
    36 
    37          (*Bob's response to Alice's message.*)
    38  | YM2:  "[| evs2 \<in> yahalom;  Nonce NB \<notin> used evs2;
    39              Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
    40           ==> Says B Server
    41                   {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    42                 # evs2 \<in> yahalom"
    43 
    44          (*The Server receives Bob's message.  He responds by sending a
    45             new session key to Alice, with a packet for forwarding to Bob.*)
    46  | YM3:  "[| evs3 \<in> yahalom;  Key KAB \<notin> used evs3;  KAB \<in> symKeys;
    47              Gets Server
    48                   {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    49                \<in> set evs3 |]
    50           ==> Says Server A
    51                    {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
    52                      Crypt (shrK B) {|Agent A, Key KAB|}|}
    53                 # evs3 \<in> yahalom"
    54 
    55          (*Alice receives the Server's (?) message, checks her Nonce, and
    56            uses the new session key to send Bob his Nonce.  The premise
    57            A \<noteq> Server is needed to prove Says_Server_not_range.*)
    58  | YM4:  "[| evs4 \<in> yahalom;  A \<noteq> Server;  K \<in> symKeys;
    59              Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
    60                 \<in> set evs4;
    61              Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
    62           ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
    63 
    64 
    65 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    66 declare parts.Body  [dest]
    67 declare Fake_parts_insert_in_Un  [dest]
    68 declare analz_into_parts [dest]
    69 
    70 
    71 text{*A "possibility property": there are traces that reach the end*}
    72 lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |] 
    73        ==> \<exists>X NB. \<exists>evs \<in> yahalom.
    74               Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
    75 apply (intro exI bexI)
    76 apply (rule_tac [2] yahalom.Nil
    77                     [THEN yahalom.YM1, THEN yahalom.Reception,
    78                      THEN yahalom.YM2, THEN yahalom.Reception,
    79                      THEN yahalom.YM3, THEN yahalom.Reception,
    80                      THEN yahalom.YM4])
    81 apply (possibility, simp add: used_Cons) 
    82 done
    83 
    84 subsection{*Regularity Lemmas for Yahalom*}
    85 
    86 lemma Gets_imp_Says:
    87      "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
    88 by (erule rev_mp, erule yahalom.induct, auto)
    89 
    90 (*Must be proved separately for each protocol*)
    91 lemma Gets_imp_knows_Spy:
    92      "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
    93 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
    94 
    95 declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
    96 
    97 
    98 subsection{* For reasoning about the encrypted portion of messages *}
    99 
   100 text{*Lets us treat YM4 using a similar argument as for the Fake case.*}
   101 lemma YM4_analz_knows_Spy:
   102      "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
   103       ==> X \<in> analz (knows Spy evs)"
   104 by blast
   105 
   106 lemmas YM4_parts_knows_Spy =
   107        YM4_analz_knows_Spy [THEN analz_into_parts, standard]
   108 
   109 
   110 text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
   111             that NOBODY sends messages containing X!*}
   112 
   113 text{*Spy never sees a good agent's shared key!*}
   114 lemma Spy_see_shrK [simp]:
   115      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   116 apply (erule yahalom.induct, force,
   117        drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
   118 done
   119 
   120 lemma Spy_analz_shrK [simp]:
   121      "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   122 by auto
   123 
   124 lemma Spy_see_shrK_D [dest!]:
   125      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> yahalom|] ==> A \<in> bad"
   126 by (blast dest: Spy_see_shrK)
   127 
   128 text{*Nobody can have used non-existent keys!
   129     Needed to apply @{text analz_insert_Key}*}
   130 lemma new_keys_not_used [simp]:
   131     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|]
   132      ==> K \<notin> keysFor (parts (spies evs))"
   133 apply (erule rev_mp)
   134 apply (erule yahalom.induct, force,
   135        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   136 txt{*Fake*}
   137 apply (force dest!: keysFor_parts_insert, auto)
   138 done
   139 
   140 
   141 subsection{*Secrecy Theorems*}
   142 
   143 (****
   144  The following is to prove theorems of the form
   145 
   146   Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
   147   Key K \<in> analz (knows Spy evs)
   148 
   149  A more general formula must be proved inductively.
   150 ****)
   151 
   152 subsection{* Session keys are not used to encrypt other session keys *}
   153 
   154 lemma analz_image_freshK [rule_format]:
   155  "evs \<in> yahalom ==>
   156    \<forall>K KK. KK <= - (range shrK) -->
   157           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   158           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   159 by (erule yahalom.induct, 
   160     drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 
   161 
   162 lemma analz_insert_freshK:
   163      "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
   164       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   165       (K = KAB | Key K \<in> analz (knows Spy evs))"
   166 by (simp only: analz_image_freshK analz_image_freshK_simps)
   167 
   168 
   169 text{*The Key K uniquely identifies the Server's  message.*}
   170 lemma unique_session_keys:
   171      "[| Says Server A
   172           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
   173         Says Server A'
   174           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
   175         evs \<in> yahalom |]
   176      ==> A=A' & B=B' & na=na' & nb=nb'"
   177 apply (erule rev_mp, erule rev_mp)
   178 apply (erule yahalom.induct, simp_all)
   179 txt{*YM3, by freshness, and YM4*}
   180 apply blast+
   181 done
   182 
   183 
   184 text{* Crucial secrecy property: Spy does not see the keys sent in msg YM3 *}
   185 lemma secrecy_lemma:
   186      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   187       ==> Says Server A
   188             {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
   189               Crypt (shrK B) {|Agent A, Key K|}|}
   190            \<in> set evs -->
   191           Key K \<notin> analz (knows Spy evs)"
   192 apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
   193 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
   194 apply (blast dest: unique_session_keys)  (*YM3*)
   195 done
   196 
   197 text{*Final version*}
   198 lemma Spy_not_see_encrypted_key:
   199      "[| Says Server A
   200             {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
   201               Crypt (shrK B) {|Agent A, Key K|}|}
   202            \<in> set evs;
   203          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   204       ==> Key K \<notin> analz (knows Spy evs)"
   205 by (blast dest: secrecy_lemma)
   206 
   207 
   208 subsection{* Security Guarantee for A upon receiving YM3 *}
   209 
   210 text{*If the encrypted message appears then it originated with the Server*}
   211 lemma A_trusts_YM3:
   212      "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
   213          A \<notin> bad;  evs \<in> yahalom |]
   214        ==> Says Server A
   215             {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
   216               Crypt (shrK B) {|Agent A, Key K|}|}
   217            \<in> set evs"
   218 apply (erule rev_mp)
   219 apply (erule yahalom.induct, force,
   220        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   221 txt{*Fake, YM3*}
   222 apply blast+
   223 done
   224 
   225 text{*The obvious combination of @{text A_trusts_YM3} with
   226   @{text Spy_not_see_encrypted_key}*}
   227 lemma A_gets_good_key:
   228      "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
   229          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   230       ==> Key K \<notin> analz (knows Spy evs)"
   231 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
   232 
   233 subsection{* Security Guarantees for B upon receiving YM4 *}
   234 
   235 text{*B knows, by the first part of A's message, that the Server distributed
   236   the key for A and B.  But this part says nothing about nonces.*}
   237 lemma B_trusts_YM4_shrK:
   238      "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
   239          B \<notin> bad;  evs \<in> yahalom |]
   240       ==> \<exists>NA NB. Says Server A
   241                       {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
   242                         Crypt (shrK B) {|Agent A, Key K|}|}
   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 txt{*Fake, YM3*}
   248 apply blast+
   249 done
   250 
   251 subsection{*The Flaw in the Model*}
   252 
   253 text{* Up to now, the reasoning is similar to standard Yahalom.  Now the
   254     doubtful reasoning occurs.  We should not be assuming that an unknown
   255     key is secure, but the model allows us to: there is no Oops rule to
   256     let session keys become compromised.*}
   257 
   258 text{*B knows, by the second part of A's message, that the Server distributed
   259   the key quoting nonce NB.  This part says nothing about agent names.
   260   Secrecy of K is assumed; the valid Yahalom proof uses (and later proves)
   261   the secrecy of NB.*}
   262 lemma B_trusts_YM4_newK [rule_format]:
   263      "[|Key K \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
   264       ==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   265           (\<exists>A B NA. Says Server A
   266                       {|Crypt (shrK A) {|Agent B, Key K,
   267                                 Nonce NA, Nonce NB|},
   268                         Crypt (shrK B) {|Agent A, Key K|}|}
   269                      \<in> set evs)"
   270 apply (erule rev_mp)
   271 apply (erule yahalom.induct, force,
   272        frule_tac [6] YM4_parts_knows_Spy)
   273 apply (analz_mono_contra, simp_all)
   274 txt{*Fake*}
   275 apply blast
   276 txt{*YM3*}
   277 apply blast
   278 txt{*A is uncompromised because NB is secure
   279   A's certificate guarantees the existence of the Server message*}
   280 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
   281              dest: Says_imp_spies
   282                    parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
   283 done
   284 
   285 
   286 text{*B's session key guarantee from YM4.  The two certificates contribute to a
   287   single conclusion about the Server's message. *}
   288 lemma B_trusts_YM4:
   289      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   290                   Crypt K (Nonce NB)|} \<in> set evs;
   291          Says B Server
   292            {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
   293            \<in> set evs;
   294          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   295        ==> \<exists>na nb. Says Server A
   296                    {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
   297                      Crypt (shrK B) {|Agent A, Key K|}|}
   298              \<in> set evs"
   299 by (blast dest: B_trusts_YM4_newK B_trusts_YM4_shrK Spy_not_see_encrypted_key
   300                 unique_session_keys)
   301 
   302 
   303 text{*The obvious combination of @{text B_trusts_YM4} with 
   304   @{text Spy_not_see_encrypted_key}*}
   305 lemma B_gets_good_key:
   306      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   307                   Crypt K (Nonce NB)|} \<in> set evs;
   308          Says B Server
   309            {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
   310            \<in> set evs;
   311          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   312       ==> Key K \<notin> analz (knows Spy evs)"
   313 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   314 
   315 
   316 (*** Authenticating B to A: these proofs are not considered.
   317      They are irrelevant to showing the need for Oops. ***)
   318 
   319 
   320 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   321 
   322 text{*Assuming the session key is secure, if both certificates are present then
   323   A has said NB.  We can't be sure about the rest of A's message, but only
   324   NB matters for freshness.*}
   325 lemma A_Said_YM3_lemma [rule_format]:
   326      "evs \<in> yahalom
   327       ==> Key K \<notin> analz (knows Spy evs) -->
   328           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   329           Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
   330           B \<notin> bad -->
   331           (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
   332 apply (erule yahalom.induct, force,
   333        frule_tac [6] YM4_parts_knows_Spy)
   334 apply (analz_mono_contra, simp_all)
   335 txt{*Fake*}
   336 apply blast
   337 txt{*YM3: by @{text new_keys_not_used}, the message
   338    @{term "Crypt K (Nonce NB)"} could not exist*}
   339 apply (force dest!: Crypt_imp_keysFor)
   340 txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message?
   341     If not, use the induction hypothesis*}
   342 apply (simp add: ex_disj_distrib)
   343 txt{*yes: apply unicity of session keys*}
   344 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
   345                     Crypt_Spy_analz_bad
   346              dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
   347 done
   348 
   349 text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   350   Moreover, A associates K with NB (thus is talking about the same run).
   351   Other premises guarantee secrecy of K.*}
   352 lemma YM4_imp_A_Said_YM3 [rule_format]:
   353      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   354                   Crypt K (Nonce NB)|} \<in> set evs;
   355          Says B Server
   356            {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
   357            \<in> set evs;
   358          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   359       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   360 by (blast intro!: A_Said_YM3_lemma
   361           dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
   362 
   363 end