src/HOL/Auth/OtwayRees_AN.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
     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 Abadi-Needham simplified version: minimal encryption, explicit messages
     9 
    10 Note that the formalization does not even assume that nonces are fresh.
    11 This is because the protocol does not rely on uniqueness of nonces for
    12 security, only for freshness, and the proof script does not prove freshness
    13 properties.
    14 
    15 From page 11 of
    16   Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    17   IEEE Trans. SE 22 (1), 1996
    18 *)
    19 
    20 theory OtwayRees_AN = Shared:
    21 
    22 consts  otway   :: "event list set"
    23 inductive "otway"
    24   intros
    25          (*Initial trace is empty*)
    26    Nil:  "[] \<in> otway"
    27 
    28          (*The spy MAY say anything he CAN say.  We do not expect him to
    29            invent new nonces here, but he can also use NS1.  Common to
    30            all similar protocols.*)
    31    Fake: "[| evsf \<in> otway;  X \<in> synth (analz (knows Spy evsf)) |]
    32           ==> Says Spy B X  # evsf \<in> otway"
    33 
    34          (*A message that has been sent can be received by the
    35            intended recipient.*)
    36    Reception: "[| evsr \<in> otway;  Says A B X \<in>set evsr |]
    37                ==> Gets B X # evsr \<in> otway"
    38 
    39          (*Alice initiates a protocol run*)
    40    OR1:  "evs1 \<in> otway
    41           ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \<in> otway"
    42 
    43          (*Bob's response to Alice's message.*)
    44    OR2:  "[| evs2 \<in> otway;
    45              Gets B {|Agent A, Agent B, Nonce NA|} \<in>set evs2 |]
    46           ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    47                  # evs2 \<in> otway"
    48 
    49          (*The Server receives Bob's message.  Then he sends a new
    50            session key to Bob with a packet for forwarding to Alice.*)
    51    OR3:  "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
    52              Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    53                \<in>set evs3 |]
    54           ==> Says Server B
    55                {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
    56                  Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
    57               # evs3 \<in> otway"
    58 
    59          (*Bob receives the Server's (?) message and compares the Nonces with
    60 	   those in the message he previously sent the Server.
    61            Need B \<noteq> Server because we allow messages to self.*)
    62    OR4:  "[| evs4 \<in> otway;  B \<noteq> Server;
    63              Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \<in>set evs4;
    64              Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
    65                \<in>set evs4 |]
    66           ==> Says B A X # evs4 \<in> otway"
    67 
    68          (*This message models possible leaks of session keys.  The nonces
    69            identify the protocol run.  B is not assumed to know shrK A.*)
    70    Oops: "[| evso \<in> otway;
    71              Says Server B
    72                       {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
    73                         Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
    74                \<in>set evso |]
    75           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
    76 
    77 
    78 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    79 declare parts.Body  [dest]
    80 declare analz_into_parts [dest]
    81 declare Fake_parts_insert_in_Un  [dest]
    82 
    83 
    84 (*A "possibility property": there are traces that reach the end*)
    85 lemma "B \<noteq> Server
    86       ==> \<exists>K. \<exists>evs \<in> otway.
    87            Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|})
    88              \<in> set evs"
    89 apply (intro exI bexI)
    90 apply (rule_tac [2] otway.Nil
    91                     [THEN otway.OR1, THEN otway.Reception,
    92                      THEN otway.OR2, THEN otway.Reception,
    93                      THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
    94 done
    95 
    96 lemma Gets_imp_Says [dest!]:
    97      "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
    98 by (erule rev_mp, erule otway.induct, auto)
    99 
   100 
   101 (**** Inductive proofs about otway ****)
   102 
   103 (** For reasoning about the encrypted portion of messages **)
   104 
   105 lemma OR4_analz_knows_Spy:
   106      "[| Gets B {|X, Crypt(shrK B) X'|} \<in> set evs;  evs \<in> otway |]
   107       ==> X \<in> analz (knows Spy evs)"
   108 by blast
   109 
   110 
   111 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
   112     sends messages containing X! **)
   113 
   114 (*Spy never sees a good agent's shared key!*)
   115 lemma Spy_see_shrK [simp]:
   116      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   117 apply (erule otway.induct, simp_all, blast+)
   118 done
   119 
   120 lemma Spy_analz_shrK [simp]:
   121      "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   122 by auto
   123 
   124 lemma Spy_see_shrK_D [dest!]:
   125      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> otway|] ==> A \<in> bad"
   126 by (blast dest: Spy_see_shrK)
   127 
   128 
   129 (*** Proofs involving analz ***)
   130 
   131 (*Describes the form of K and NA when the Server sends this message.*)
   132 lemma Says_Server_message_form:
   133      "[| Says Server B
   134             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
   135               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   136            \<in> set evs;
   137          evs \<in> otway |]
   138       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
   139 apply (erule rev_mp)
   140 apply (erule otway.induct, simp_all, blast)
   141 done
   142 
   143 
   144 
   145 (****
   146  The following is to prove theorems of the form
   147 
   148   Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
   149   Key K \<in> analz (knows Spy evs)
   150 
   151  A more general formula must be proved inductively.
   152 ****)
   153 
   154 
   155 (** Session keys are not used to encrypt other session keys **)
   156 
   157 (*The equality makes the induction hypothesis easier to apply*)
   158 lemma analz_image_freshK [rule_format]:
   159  "evs \<in> otway ==>
   160    \<forall>K KK. KK <= -(range shrK) -->
   161           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   162           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   163 apply (erule otway.induct, force)
   164 apply (frule_tac [7] Says_Server_message_form)
   165 apply (drule_tac [6] OR4_analz_knows_Spy, analz_freshK, spy_analz)
   166 done
   167 
   168 lemma analz_insert_freshK:
   169   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
   170       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   171       (K = KAB | Key K \<in> analz (knows Spy evs))"
   172 by (simp only: analz_image_freshK analz_image_freshK_simps)
   173 
   174 
   175 (*** The Key K uniquely identifies the Server's message. **)
   176 
   177 lemma unique_session_keys:
   178      "[| Says Server B
   179           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},
   180             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}
   181          \<in> set evs;
   182         Says Server B'
   183           {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},
   184             Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}
   185          \<in> set evs;
   186         evs \<in> otway |]
   187      ==> A=A' & B=B' & NA=NA' & NB=NB'"
   188 apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all)
   189 (*Remaining cases: OR3 and OR4*)
   190 apply blast+
   191 done
   192 
   193 
   194 (**** Authenticity properties relating to NA ****)
   195 
   196 (*If the encrypted message appears then it originated with the Server!*)
   197 lemma NA_Crypt_imp_Server_msg [rule_format]:
   198     "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   199      ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs)
   200        --> (\<exists>NB. Says Server B
   201                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
   202                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   203                     \<in> set evs)"
   204 apply (erule otway.induct, force)
   205 apply (simp_all add: ex_disj_distrib)
   206 (*Fake, OR3*)
   207 apply blast+
   208 done
   209 
   210 
   211 (*Corollary: if A receives B's OR4 message then it originated with the Server.
   212   Freshness may be inferred from nonce NA.*)
   213 lemma A_trusts_OR4:
   214      "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs;
   215          A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   216       ==> \<exists>NB. Says Server B
   217                   {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
   218                     Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   219                  \<in> set evs"
   220 by (blast intro!: NA_Crypt_imp_Server_msg)
   221 
   222 
   223 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   224     Does not in itself guarantee security: an attack could violate
   225     the premises, e.g. by having A=Spy **)
   226 
   227 lemma secrecy_lemma:
   228      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   229       ==> Says Server B
   230            {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
   231              Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   232           \<in> set evs -->
   233           Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
   234           Key K \<notin> analz (knows Spy evs)"
   235 apply (erule otway.induct, force)
   236 apply (frule_tac [7] Says_Server_message_form)
   237 apply (drule_tac [6] OR4_analz_knows_Spy)
   238 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
   239 (*OR3, OR4, Oops*)
   240 apply (blast dest: unique_session_keys)+
   241 done
   242 
   243 
   244 lemma Spy_not_see_encrypted_key:
   245      "[| Says Server B
   246             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
   247               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   248            \<in> set evs;
   249          Notes Spy {|NA, NB, Key K|} \<notin> set evs;
   250          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   251       ==> Key K \<notin> analz (knows Spy evs)"
   252 by (blast dest: Says_Server_message_form secrecy_lemma)
   253 
   254 
   255 (*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   256   what it is.*)
   257 lemma A_gets_good_key:
   258      "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs;
   259          \<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
   260          A \<notin> bad;  B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   261       ==> Key K \<notin> analz (knows Spy evs)"
   262 by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
   263 
   264 
   265 
   266 (**** Authenticity properties relating to NB ****)
   267 
   268 (*If the encrypted message appears then it originated with the Server!*)
   269 
   270 lemma NB_Crypt_imp_Server_msg [rule_format]:
   271  "[| B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   272   ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs)
   273       --> (\<exists>NA. Says Server B
   274                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
   275                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   276                    \<in> set evs)"
   277 apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
   278 (*Fake, OR3*)
   279 apply blast+
   280 done
   281 
   282 
   283 
   284 (*Guarantee for B: if it gets a well-formed certificate then the Server
   285   has sent the correct message in round 3.*)
   286 lemma B_trusts_OR3:
   287      "[| Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   288            \<in> set evs;
   289          B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   290       ==> \<exists>NA. Says Server B
   291                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
   292                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   293                    \<in> set evs"
   294 by (blast intro!: NB_Crypt_imp_Server_msg)
   295 
   296 
   297 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
   298 lemma B_gets_good_key:
   299      "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
   300           \<in> set evs;
   301          \<forall>NA. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
   302          A \<notin> bad;  B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   303       ==> Key K \<notin> analz (knows Spy evs)"
   304 by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key)
   305 
   306 end