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