src/HOL/Auth/OtwayRees_Bad.thy
author paulson
Sat Aug 17 14:55:08 2002 +0200 (2002-08-17)
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 14200 d8598e24f8fa
permissions -rw-r--r--
tidying of Isar scripts
     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 Inductive relation "otway" for the Otway-Rees protocol.
     7 
     8 The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 
    12 This file illustrates the consequences of such errors.  We can still prove
    13 impressive-looking properties such as Spy_not_see_encrypted_key, yet the
    14 protocol is open to a middleperson attack.  Attempting to prove some key lemmas
    15 indicates the possibility of this attack.
    16 *)
    17 
    18 theory OtwayRees_Bad = Shared:
    19 
    20 consts  otway   :: "event list set"
    21 inductive "otway"
    22   intros
    23          (*Initial trace is empty*)
    24    Nil:  "[] \<in> otway"
    25 
    26          (*The spy MAY say anything he CAN say.  We do not expect him to
    27            invent new nonces here, but he can also use NS1.  Common to
    28            all similar protocols.*)
    29    Fake: "[| evsf \<in> otway;  X \<in> synth (analz (knows Spy evsf)) |]
    30           ==> Says Spy B X  # evsf \<in> otway"
    31 
    32          (*A message that has been sent can be received by the
    33            intended recipient.*)
    34    Reception: "[| evsr \<in> otway;  Says A B X \<in>set evsr |]
    35                ==> Gets B X # evsr \<in> otway"
    36 
    37          (*Alice initiates a protocol run*)
    38    OR1:  "[| 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          (*Bob's response to Alice's message.
    44            This variant of the protocol does NOT encrypt NB.*)
    45    OR2:  "[| 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          (*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    OR3:  "[| 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          (*Bob receives the Server's (?) message and compares the Nonces with
    69 	   those in the message he previously sent the Server.
    70            Need B ~= Server because we allow messages to self.*)
    71    OR4:  "[| evs4 \<in> otway;  B ~= 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          (*This message models possible leaks of session keys.  The nonces
    80            identify the protocol run.*)
    81    Oops: "[| 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 (*A "possibility property": there are traces that reach the end*)
    93 lemma "B \<noteq> Server
    94       ==> \<exists>K. \<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], possibility)
   102 done
   103 
   104 lemma Gets_imp_Says [dest!]:
   105      "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
   106 apply (erule rev_mp)
   107 apply (erule otway.induct, auto)
   108 done
   109 
   110 
   111 (**** Inductive proofs about otway ****)
   112 
   113 
   114 (** For reasoning about the encrypted portion of messages **)
   115 
   116 lemma OR2_analz_knows_Spy:
   117      "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs;  evs \<in> otway |]
   118       ==> X \<in> analz (knows Spy evs)"
   119 by blast
   120 
   121 lemma OR4_analz_knows_Spy:
   122      "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs;  evs \<in> otway |]
   123       ==> X \<in> analz (knows Spy evs)"
   124 by blast
   125 
   126 lemma Oops_parts_knows_Spy:
   127      "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \<in> set evs
   128       ==> K \<in> parts (knows Spy evs)"
   129 by blast
   130 
   131 (*Forwarding lemma: see comments in OtwayRees.thy*)
   132 lemmas OR2_parts_knows_Spy =
   133     OR2_analz_knows_Spy [THEN analz_into_parts, standard]
   134 
   135 
   136 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
   137     sends messages containing X! **)
   138 
   139 (*Spy never sees a good agent's shared key!*)
   140 lemma Spy_see_shrK [simp]:
   141      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   142 apply (erule otway.induct, force,
   143        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   144 done
   145 
   146 lemma Spy_analz_shrK [simp]:
   147      "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   148 by auto
   149 
   150 lemma Spy_see_shrK_D [dest!]:
   151      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> otway|] ==> A \<in> bad"
   152 by (blast dest: Spy_see_shrK)
   153 
   154 
   155 (*** Proofs involving analz ***)
   156 
   157 (*Describes the form of K and NA when the Server sends this message.  Also
   158   for Oops case.*)
   159 lemma Says_Server_message_form:
   160      "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
   161          evs \<in> otway |]
   162       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
   163 apply (erule rev_mp)
   164 apply (erule otway.induct, simp_all, blast)
   165 done
   166 
   167 
   168 (****
   169  The following is to prove theorems of the form
   170 
   171   Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
   172   Key K \<in> analz (knows Spy evs)
   173 
   174  A more general formula must be proved inductively.
   175 ****)
   176 
   177 
   178 (** Session keys are not used to encrypt other session keys **)
   179 
   180 (*The equality makes the induction hypothesis easier to apply*)
   181 lemma analz_image_freshK [rule_format]:
   182  "evs \<in> otway ==>
   183    \<forall>K KK. KK <= -(range shrK) -->
   184           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   185           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   186 apply (erule otway.induct, force)
   187 apply (frule_tac [7] Says_Server_message_form)
   188 apply (drule_tac [6] OR4_analz_knows_Spy)
   189 apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
   190 done
   191 
   192 lemma analz_insert_freshK:
   193   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
   194       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   195       (K = KAB | Key K \<in> analz (knows Spy evs))"
   196 by (simp only: analz_image_freshK analz_image_freshK_simps)
   197 
   198 
   199 (*** The Key K uniquely identifies the Server's  message. **)
   200 
   201 lemma unique_session_keys:
   202      "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   \<in> set evs;
   203          Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
   204          evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
   205 apply (erule rev_mp)
   206 apply (erule rev_mp)
   207 apply (erule otway.induct, simp_all)
   208 (*Remaining cases: OR3 and OR4*)
   209 apply blast+
   210 done
   211 
   212 
   213 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   214     Does not in itself guarantee security: an attack could violate
   215     the premises, e.g. by having A=Spy **)
   216 
   217 lemma secrecy_lemma:
   218  "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   219   ==> Says Server B
   220         {|NA, Crypt (shrK A) {|NA, Key K|},
   221           Crypt (shrK B) {|NB, Key K|}|} \<in> set evs -->
   222       Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
   223       Key K \<notin> analz (knows Spy evs)"
   224 apply (erule otway.induct, force)
   225 apply (frule_tac [7] Says_Server_message_form)
   226 apply (drule_tac [6] OR4_analz_knows_Spy)
   227 apply (drule_tac [4] OR2_analz_knows_Spy)
   228 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
   229 (*OR3, OR4, Oops*)
   230 apply (blast dest: unique_session_keys)+
   231 done
   232 
   233 
   234 lemma Spy_not_see_encrypted_key:
   235      "[| Says Server B
   236           {|NA, Crypt (shrK A) {|NA, Key K|},
   237                 Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
   238          Notes Spy {|NA, NB, Key K|} \<notin> set evs;
   239          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   240       ==> Key K \<notin> analz (knows Spy evs)"
   241 by (blast dest: Says_Server_message_form secrecy_lemma)
   242 
   243 
   244 (*** Attempting to prove stronger properties ***)
   245 
   246 (*Only OR1 can have caused such a part of a message to appear.
   247   The premise A \<noteq> B prevents OR2's similar-looking cryptogram from being
   248   picked up.  Original Otway-Rees doesn't need it.*)
   249 lemma Crypt_imp_OR1 [rule_format]:
   250      "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   251       ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
   252           Says A B {|NA, Agent A, Agent B,
   253                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
   254 apply (erule otway.induct, force,
   255        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   256 done
   257 
   258 
   259 (*Crucial property: If the encrypted message appears, and A has used NA
   260   to start a run, then it originated with the Server!
   261   The premise A \<noteq> B allows use of Crypt_imp_OR1*)
   262 (*Only it is FALSE.  Somebody could make a fake message to Server
   263           substituting some other nonce NA' for NB.*)
   264 lemma "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   265        ==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) -->
   266            Says A B {|NA, Agent A, Agent B,
   267                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}
   268             \<in> set evs -->
   269            (\<exists>B NB. Says Server B
   270                 {|NA,
   271                   Crypt (shrK A) {|NA, Key K|},
   272                   Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
   273 apply (erule otway.induct, force,
   274        drule_tac [4] OR2_parts_knows_Spy, simp_all)
   275 (*Fake*)
   276 apply blast
   277 (*OR1: it cannot be a new Nonce, contradiction.*)
   278 apply blast
   279 (*OR3 and OR4*)
   280 apply (simp_all add: ex_disj_distrib)
   281 (*OR4*)
   282 prefer 2 apply (blast intro!: Crypt_imp_OR1)
   283 (*OR3*)
   284 apply clarify
   285 (*The hypotheses at this point suggest an attack in which nonce NB is used
   286   in two different roles:
   287           Gets Server
   288            {|Nonce NA, Agent Aa, Agent A,
   289              Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
   290              Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
   291           \<in> set evs3
   292           Says A B
   293            {|Nonce NB, Agent A, Agent B,
   294              Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
   295           \<in> set evs3;
   296 *)
   297 
   298 
   299 (*Thus the key property A_can_trust probably fails too.*)
   300 oops
   301 
   302 end