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