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