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