src/HOL/Auth/OtwayRees_Bad.thy
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 23746 a455e69c31cc
child 32960 69916a850301
permissions -rw-r--r--
named code theorem for Fract_norm
     1 (*  Title:      HOL/Auth/OtwayRees_Bad
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 *)
     6 
     7 
     8 header{*The Otway-Rees Protocol: The Faulty BAN Version*}
     9 
    10 theory OtwayRees_Bad imports Public begin
    11 
    12 text{*The FAULTY version omitting encryption of Nonce NB, as suggested on 
    13 page 247 of
    14   Burrows, Abadi and Needham (1988).  A Logic of Authentication.
    15   Proc. Royal Soc. 426
    16 
    17 This file illustrates the consequences of such errors.  We can still prove
    18 impressive-looking properties such as @{text Spy_not_see_encrypted_key}, yet
    19 the protocol is open to a middleperson attack.  Attempting to prove some key
    20 lemmas indicates the possibility of this attack.*}
    21 
    22 inductive_set otway :: "event list set"
    23   where
    24    Nil: --{*The empty trace*}
    25         "[] \<in> otway"
    26 
    27  | Fake: --{*The Spy may say anything he can say.  The sender field is correct,
    28             but agents don't use that information.*}
    29          "[| evsf \<in> otway;  X \<in> synth (analz (knows Spy evsf)) |]
    30           ==> Says Spy B X  # evsf \<in> otway"
    31 
    32         
    33  | Reception: --{*A message that has been sent can be received by the
    34                   intended recipient.*}
    35 	      "[| evsr \<in> otway;  Says A B X \<in>set evsr |]
    36                ==> Gets B X # evsr \<in> otway"
    37 
    38  | OR1:  --{*Alice initiates a protocol run*}
    39 	 "[| evs1 \<in> otway;  Nonce NA \<notin> used evs1 |]
    40           ==> Says A B {|Nonce NA, Agent A, Agent B,
    41                          Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
    42                  # evs1 \<in> otway"
    43 
    44  | OR2:  --{*Bob's response to Alice's message.
    45              This variant of the protocol does NOT encrypt NB.*}
    46 	 "[| evs2 \<in> otway;  Nonce NB \<notin> used evs2;
    47              Gets B {|Nonce NA, Agent A, Agent B, X|} \<in> set evs2 |]
    48           ==> Says B Server
    49                   {|Nonce NA, Agent A, Agent B, X, Nonce NB,
    50                     Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    51                  # evs2 \<in> otway"
    52 
    53  | OR3:  --{*The Server receives Bob's message and checks that the three NAs
    54            match.  Then he sends a new session key to Bob with a packet for
    55            forwarding to Alice.*}
    56 	 "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
    57              Gets Server
    58                   {|Nonce NA, Agent A, Agent B,
    59                     Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
    60                     Nonce NB,
    61                     Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    62                \<in> set evs3 |]
    63           ==> Says Server B
    64                   {|Nonce NA,
    65                     Crypt (shrK A) {|Nonce NA, Key KAB|},
    66                     Crypt (shrK B) {|Nonce NB, Key KAB|}|}
    67                  # evs3 \<in> otway"
    68 
    69  | OR4:  --{*Bob receives the Server's (?) message and compares the Nonces with
    70 	     those in the message he previously sent the Server.
    71              Need @{term "B \<noteq> Server"} because we allow messages to self.*}
    72 	 "[| evs4 \<in> otway;  B \<noteq> Server;
    73              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
    74                              Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    75                \<in> set evs4;
    76              Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    77                \<in> set evs4 |]
    78           ==> Says B A {|Nonce NA, X|} # evs4 \<in> otway"
    79 
    80  | Oops: --{*This message models possible leaks of session keys.  The nonces
    81              identify the protocol run.*}
    82 	 "[| evso \<in> otway;
    83              Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    84                \<in> set evso |]
    85           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
    86 
    87 
    88 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    89 declare parts.Body  [dest]
    90 declare analz_into_parts [dest]
    91 declare Fake_parts_insert_in_Un  [dest]
    92 
    93 text{*A "possibility property": there are traces that reach the end*}
    94 lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
    95       ==> \<exists>NA. \<exists>evs \<in> otway.
    96             Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
    97               \<in> set evs"
    98 apply (intro exI bexI)
    99 apply (rule_tac [2] otway.Nil
   100                     [THEN otway.OR1, THEN otway.Reception,
   101                      THEN otway.OR2, THEN otway.Reception,
   102                      THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
   103 apply (possibility, simp add: used_Cons) 
   104 done
   105 
   106 lemma Gets_imp_Says [dest!]:
   107      "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
   108 apply (erule rev_mp)
   109 apply (erule otway.induct, auto)
   110 done
   111 
   112 
   113 subsection{*For reasoning about the encrypted portion of messages *}
   114 
   115 lemma OR2_analz_knows_Spy:
   116      "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs;  evs \<in> otway |]
   117       ==> X \<in> analz (knows Spy evs)"
   118 by blast
   119 
   120 lemma OR4_analz_knows_Spy:
   121      "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs;  evs \<in> otway |]
   122       ==> X \<in> analz (knows Spy evs)"
   123 by blast
   124 
   125 lemma Oops_parts_knows_Spy:
   126      "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \<in> set evs
   127       ==> K \<in> parts (knows Spy evs)"
   128 by blast
   129 
   130 text{*Forwarding lemma: see comments in OtwayRees.thy*}
   131 lemmas OR2_parts_knows_Spy =
   132     OR2_analz_knows_Spy [THEN analz_into_parts, standard]
   133 
   134 
   135 text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
   136 NOBODY sends messages containing X! *}
   137 
   138 text{*Spy never sees a good agent's shared key!*}
   139 lemma Spy_see_shrK [simp]:
   140      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   141 by (erule otway.induct, force,
   142     drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   143 
   144 
   145 lemma Spy_analz_shrK [simp]:
   146      "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   147 by auto
   148 
   149 lemma Spy_see_shrK_D [dest!]:
   150      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> otway|] ==> A \<in> bad"
   151 by (blast dest: Spy_see_shrK)
   152 
   153 
   154 subsection{*Proofs involving analz *}
   155 
   156 text{*Describes the form of K and NA when the Server sends this message.  Also
   157   for Oops case.*}
   158 lemma Says_Server_message_form:
   159      "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
   160          evs \<in> otway |]
   161       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
   162 apply (erule rev_mp)
   163 apply (erule otway.induct, simp_all)
   164 done
   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 
   177 text{*Session keys are not used to encrypt other session keys*}
   178 
   179 text{*The equality makes the induction hypothesis easier to apply*}
   180 lemma analz_image_freshK [rule_format]:
   181  "evs \<in> otway ==>
   182    \<forall>K KK. KK <= -(range shrK) -->
   183           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   184           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   185 apply (erule otway.induct)
   186 apply (frule_tac [8] Says_Server_message_form)
   187 apply (drule_tac [7] OR4_analz_knows_Spy)
   188 apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) 
   189 done
   190 
   191 lemma analz_insert_freshK:
   192   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
   193       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   194       (K = KAB | Key K \<in> analz (knows Spy evs))"
   195 by (simp only: analz_image_freshK analz_image_freshK_simps)
   196 
   197 
   198 text{*The Key K uniquely identifies the Server's  message. *}
   199 lemma unique_session_keys:
   200      "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   \<in> set evs;
   201          Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
   202          evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
   203 apply (erule rev_mp)
   204 apply (erule rev_mp)
   205 apply (erule otway.induct, simp_all)
   206 apply blast+  --{*OR3 and OR4*}
   207 done
   208 
   209 
   210 text{*Crucial secrecy property: Spy does not see the keys sent in msg OR3
   211     Does not in itself guarantee security: an attack could violate
   212     the premises, e.g. by having @{term "A=Spy"} *}
   213 lemma secrecy_lemma:
   214  "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   215   ==> Says Server B
   216         {|NA, Crypt (shrK A) {|NA, Key K|},
   217           Crypt (shrK B) {|NB, Key K|}|} \<in> set evs -->
   218       Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
   219       Key K \<notin> analz (knows Spy evs)"
   220 apply (erule otway.induct, force)
   221 apply (frule_tac [7] Says_Server_message_form)
   222 apply (drule_tac [6] OR4_analz_knows_Spy)
   223 apply (drule_tac [4] OR2_analz_knows_Spy)
   224 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
   225 apply spy_analz  --{*Fake*}
   226 apply (blast dest: unique_session_keys)+  --{*OR3, OR4, Oops*}
   227 done
   228 
   229 
   230 lemma Spy_not_see_encrypted_key:
   231      "[| Says Server B
   232           {|NA, Crypt (shrK A) {|NA, Key K|},
   233                 Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
   234          Notes Spy {|NA, NB, Key K|} \<notin> set evs;
   235          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   236       ==> Key K \<notin> analz (knows Spy evs)"
   237 by (blast dest: Says_Server_message_form secrecy_lemma)
   238 
   239 
   240 subsection{*Attempting to prove stronger properties *}
   241 
   242 text{*Only OR1 can have caused such a part of a message to appear. The premise
   243   @{term "A \<noteq> B"} prevents OR2's similar-looking cryptogram from being picked 
   244   up. Original Otway-Rees doesn't need it.*}
   245 lemma Crypt_imp_OR1 [rule_format]:
   246      "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   247       ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
   248           Says A B {|NA, Agent A, Agent B,
   249                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
   250 by (erule otway.induct, force,
   251     drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   252 
   253 
   254 text{*Crucial property: If the encrypted message appears, and A has used NA
   255   to start a run, then it originated with the Server!
   256   The premise @{term "A \<noteq> B"} allows use of @{text Crypt_imp_OR1}*}
   257 text{*Only it is FALSE.  Somebody could make a fake message to Server
   258           substituting some other nonce NA' for NB.*}
   259 lemma "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   260        ==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) -->
   261            Says A B {|NA, Agent A, Agent B,
   262                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}
   263             \<in> set evs -->
   264            (\<exists>B NB. Says Server B
   265                 {|NA,
   266                   Crypt (shrK A) {|NA, Key K|},
   267                   Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
   268 apply (erule otway.induct, force,
   269        drule_tac [4] OR2_parts_knows_Spy, simp_all)
   270 apply blast  --{*Fake*}
   271 apply blast  --{*OR1: it cannot be a new Nonce, contradiction.*}
   272 txt{*OR3 and OR4*}
   273 apply (simp_all add: ex_disj_distrib)
   274  prefer 2 apply (blast intro!: Crypt_imp_OR1)  --{*OR4*}
   275 txt{*OR3*}
   276 apply clarify
   277 (*The hypotheses at this point suggest an attack in which nonce NB is used
   278   in two different roles:
   279           Gets Server
   280            {|Nonce NA, Agent Aa, Agent A,
   281              Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
   282              Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
   283           \<in> set evs3
   284           Says A B
   285            {|Nonce NB, Agent A, Agent B,
   286              Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
   287           \<in> set evs3;
   288 *)
   289 
   290 
   291 (*Thus the key property A_can_trust probably fails too.*)
   292 oops
   293 
   294 end