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