1(* Title: HOL/Auth/OtwayRees_AN.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4*) 5 6section\<open>The Otway-Rees Protocol as Modified by Abadi and Needham\<close> 7 8theory OtwayRees_AN imports Public begin 9 10text\<open> 11This simplified version has minimal encryption and explicit messages. 12 13Note that the formalization does not even assume that nonces are fresh. 14This is because the protocol does not rely on uniqueness of nonces for 15security, only for freshness, and the proof script does not prove freshness 16properties. 17 18From page 11 of 19 Abadi and Needham (1996). 20 Prudent Engineering Practice for Cryptographic Protocols. 21 IEEE Trans. SE 22 (1) 22\<close> 23 24inductive_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>\<open>B \<noteq> Server\<close> 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 79declare Says_imp_knows_Spy [THEN analz.Inj, dest] 80declare parts.Body [dest] 81declare analz_into_parts [dest] 82declare Fake_parts_insert_in_Un [dest] 83 84 85text\<open>A "possibility property": there are traces that reach the end\<close> 86lemma "[| 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" 90apply (intro exI bexI) 91apply (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]) 95apply (possibility, simp add: used_Cons) 96done 97 98lemma Gets_imp_Says [dest!]: 99 "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" 100by (erule rev_mp, erule otway.induct, auto) 101 102 103 104text\<open>For reasoning about the encrypted portion of messages\<close> 105 106lemma 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)" 109by blast 110 111 112text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (spies evs)\<close> imply that 113NOBODY sends messages containing X!\<close> 114 115text\<open>Spy never sees a good agent's shared key!\<close> 116lemma Spy_see_shrK [simp]: 117 "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 118by (erule otway.induct, simp_all, blast+) 119 120lemma Spy_analz_shrK [simp]: 121 "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 122by auto 123 124lemma Spy_see_shrK_D [dest!]: 125 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad" 126by (blast dest: Spy_see_shrK) 127 128 129subsection\<open>Proofs involving analz\<close> 130 131text\<open>Describes the form of K and NA when the Server sends this message.\<close> 132lemma 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 \<and> (\<exists>i. NA = Nonce i) \<and> (\<exists>j. NB = Nonce j)" 139apply (erule rev_mp) 140apply (erule otway.induct, auto) 141done 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 155text\<open>Session keys are not used to encrypt other session keys\<close> 156 157text\<open>The equality makes the induction hypothesis easier to apply\<close> 158lemma analz_image_freshK [rule_format]: 159 "evs \<in> otway ==> 160 \<forall>K KK. KK \<subseteq> -(range shrK) \<longrightarrow> 161 (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) = 162 (K \<in> KK | Key K \<in> analz (knows Spy evs))" 163apply (erule otway.induct) 164apply (frule_tac [8] Says_Server_message_form) 165apply (drule_tac [7] OR4_analz_knows_Spy, analz_freshK, spy_analz, auto) 166done 167 168lemma 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))" 172by (simp only: analz_image_freshK analz_image_freshK_simps) 173 174 175text\<open>The Key K uniquely identifies the Server's message.\<close> 176lemma 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' \<and> B=B' \<and> NA=NA' \<and> NB=NB'" 187apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all) 188apply blast+ \<comment> \<open>OR3 and OR4\<close> 189done 190 191 192subsection\<open>Authenticity properties relating to NA\<close> 193 194text\<open>If the encrypted message appears then it originated with the Server!\<close> 195lemma 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 \<longrightarrow> (\<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)" 202apply (erule otway.induct, force) 203apply (simp_all add: ex_disj_distrib) 204apply blast+ \<comment> \<open>Fake, OR3\<close> 205done 206 207 208text\<open>Corollary: if A receives B's OR4 message then it originated with the 209 Server. Freshness may be inferred from nonce NA.\<close> 210lemma 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" 217by (blast intro!: NA_Crypt_imp_Server_msg) 218 219 220text\<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>\<open>A=Spy\<close>\<close> 223lemma 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 \<longrightarrow> 229 Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs \<longrightarrow> 230 Key K \<notin> analz (knows Spy evs)" 231apply (erule otway.induct, force) 232apply (frule_tac [7] Says_Server_message_form) 233apply (drule_tac [6] OR4_analz_knows_Spy) 234apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) 235apply spy_analz \<comment> \<open>Fake\<close> 236apply (blast dest: unique_session_keys)+ \<comment> \<open>OR3, OR4, Oops\<close> 237done 238 239 240lemma 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 251text\<open>A's guarantee. The Oops premise quantifies over NB because A cannot know 252 what it is.\<close> 253lemma 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 262subsection\<open>Authenticity properties relating to NB\<close> 263 264text\<open>If the encrypted message appears then it originated with the Server!\<close> 265lemma 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 \<longrightarrow> (\<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)" 272apply (erule otway.induct, force, simp_all add: ex_disj_distrib) 273apply blast+ \<comment> \<open>Fake, OR3\<close> 274done 275 276 277 278text\<open>Guarantee for B: if it gets a well-formed certificate then the Server 279 has sent the correct message in round 3.\<close> 280lemma 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" 288by (blast intro!: NB_Crypt_imp_Server_msg) 289 290 291text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with 292 \<open>Spy_not_see_encrypted_key\<close>\<close> 293lemma 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)" 299by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key) 300 301end 302