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