1(* Title: HOL/UNITY/Simple/NSP_Bad.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4 5Original file is ../Auth/NS_Public_Bad 6*) 7 8section\<open>Analyzing the Needham-Schroeder Public-Key Protocol in UNITY\<close> 9 10theory NSP_Bad imports "HOL-Auth.Public" "../UNITY_Main" begin 11 12text\<open>This is the flawed version, vulnerable to Lowe's attack. 13From page 260 of 14 Burrows, Abadi and Needham. A Logic of Authentication. 15 Proc. Royal Soc. 426 (1989). 16\<close> 17 18type_synonym state = "event list" 19 20 (*The spy MAY say anything he CAN say. We do not expect him to 21 invent new nonces here, but he can also use NS1. Common to 22 all similar protocols.*) 23definition 24 Fake :: "(state*state) set" 25 where "Fake = {(s,s'). 26 \<exists>B X. s' = Says Spy B X # s 27 & X \<in> synth (analz (spies s))}" 28 29 (*The numeric suffixes on A identify the rule*) 30 31 (*Alice initiates a protocol run, sending a nonce to Bob*) 32definition 33 NS1 :: "(state*state) set" 34 where "NS1 = {(s1,s'). 35 \<exists>A1 B NA. 36 s' = Says A1 B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A1\<rbrace>) # s1 37 & Nonce NA \<notin> used s1}" 38 39 (*Bob responds to Alice's message with a further nonce*) 40definition 41 NS2 :: "(state*state) set" 42 where "NS2 = {(s2,s'). 43 \<exists>A' A2 B NA NB. 44 s' = Says B A2 (Crypt (pubK A2) \<lbrace>Nonce NA, Nonce NB\<rbrace>) # s2 45 & Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A2\<rbrace>) \<in> set s2 46 & Nonce NB \<notin> used s2}" 47 48 (*Alice proves her existence by sending NB back to Bob.*) 49definition 50 NS3 :: "(state*state) set" 51 where "NS3 = {(s3,s'). 52 \<exists>A3 B' B NA NB. 53 s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3 54 & Says A3 B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A3\<rbrace>) \<in> set s3 55 & Says B' A3 (Crypt (pubK A3) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s3}" 56 57 58definition Nprg :: "state program" where 59 (*Initial trace is empty*) 60 "Nprg = mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)" 61 62declare spies_partsEs [elim] 63declare analz_into_parts [dest] 64declare Fake_parts_insert_in_Un [dest] 65 66text\<open>For other theories, e.g. Mutex and Lift, using [iff] slows proofs down. 67 Here, it facilitates re-use of the Auth proofs.\<close> 68 69declare Fake_def [THEN def_act_simp, iff] 70declare NS1_def [THEN def_act_simp, iff] 71declare NS2_def [THEN def_act_simp, iff] 72declare NS3_def [THEN def_act_simp, iff] 73 74declare Nprg_def [THEN def_prg_Init, simp] 75 76 77text\<open>A "possibility property": there are traces that reach the end. 78 Replace by LEADSTO proof!\<close> 79lemma "A \<noteq> B ==> 80 \<exists>NB. \<exists>s \<in> reachable Nprg. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set s" 81apply (intro exI bexI) 82apply (rule_tac [2] act = "totalize_act NS3" in reachable.Acts) 83apply (rule_tac [3] act = "totalize_act NS2" in reachable.Acts) 84apply (rule_tac [4] act = "totalize_act NS1" in reachable.Acts) 85apply (rule_tac [5] reachable.Init) 86apply (simp_all (no_asm_simp) add: Nprg_def totalize_act_def) 87apply auto 88done 89 90 91subsection\<open>Inductive Proofs about \<^term>\<open>ns_public\<close>\<close> 92 93lemma ns_constrainsI: 94 "(!!act s s'. [| act \<in> {Id, Fake, NS1, NS2, NS3}; 95 (s,s') \<in> act; s \<in> A |] ==> s' \<in> A') 96 ==> Nprg \<in> A co A'" 97apply (simp add: Nprg_def mk_total_program_def) 98apply (rule constrainsI, auto) 99done 100 101 102text\<open>This ML code does the inductions directly.\<close> 103ML\<open> 104fun ns_constrains_tac ctxt i = 105 SELECT_GOAL 106 (EVERY 107 [REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1), 108 REPEAT (resolve_tac ctxt [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), 109 resolve_tac ctxt @{thms ns_constrainsI} 1, 110 full_simp_tac ctxt 1, 111 REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])), 112 ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])), 113 REPEAT (FIRSTGOAL (analz_mono_contra_tac ctxt)), 114 ALLGOALS (asm_simp_tac ctxt)]) i; 115 116(*Tactic for proving secrecy theorems*) 117fun ns_induct_tac ctxt = 118 (SELECT_GOAL o EVERY) 119 [resolve_tac ctxt @{thms AlwaysI} 1, 120 force_tac ctxt 1, 121 (*"reachable" gets in here*) 122 resolve_tac ctxt [@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}] 1, 123 ns_constrains_tac ctxt 1]; 124\<close> 125 126method_setup ns_induct = \<open> 127 Scan.succeed (SIMPLE_METHOD' o ns_induct_tac)\<close> 128 "for inductive reasoning about the Needham-Schroeder protocol" 129 130text\<open>Converts invariants into statements about reachable states\<close> 131lemmas Always_Collect_reachableD = 132 Always_includes_reachable [THEN subsetD, THEN CollectD] 133 134text\<open>Spy never sees another agent's private key! (unless it's bad at start)\<close> 135lemma Spy_see_priK: 136 "Nprg \<in> Always {s. (Key (priK A) \<in> parts (spies s)) = (A \<in> bad)}" 137apply ns_induct 138apply blast 139done 140declare Spy_see_priK [THEN Always_Collect_reachableD, simp] 141 142lemma Spy_analz_priK: 143 "Nprg \<in> Always {s. (Key (priK A) \<in> analz (spies s)) = (A \<in> bad)}" 144by (rule Always_reachable [THEN Always_weaken], auto) 145declare Spy_analz_priK [THEN Always_Collect_reachableD, simp] 146 147 148subsection\<open>Authenticity properties obtained from NS2\<close> 149 150text\<open>It is impossible to re-use a nonce in both NS1 and NS2 provided the 151 nonce is secret. (Honest users generate fresh nonces.)\<close> 152lemma no_nonce_NS1_NS2: 153 "Nprg 154 \<in> Always {s. Crypt (pubK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies s) --> 155 Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies s) --> 156 Nonce NA \<in> analz (spies s)}" 157apply ns_induct 158apply (blast intro: analz_insertI)+ 159done 160 161text\<open>Adding it to the claset slows down proofs...\<close> 162lemmas no_nonce_NS1_NS2_reachable = 163 no_nonce_NS1_NS2 [THEN Always_Collect_reachableD, rule_format] 164 165 166text\<open>Unicity for NS1: nonce NA identifies agents A and B\<close> 167lemma unique_NA_lemma: 168 "Nprg 169 \<in> Always {s. Nonce NA \<notin> analz (spies s) --> 170 Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s) --> 171 Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s) --> 172 A=A' & B=B'}" 173apply ns_induct 174apply auto 175txt\<open>Fake, NS1 are non-trivial\<close> 176done 177 178text\<open>Unicity for NS1: nonce NA identifies agents A and B\<close> 179lemma unique_NA: 180 "[| Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s); 181 Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s); 182 Nonce NA \<notin> analz (spies s); 183 s \<in> reachable Nprg |] 184 ==> A=A' & B=B'" 185by (blast dest: unique_NA_lemma [THEN Always_Collect_reachableD]) 186 187 188text\<open>Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure\<close> 189lemma Spy_not_see_NA: 190 "[| A \<notin> bad; B \<notin> bad |] 191 ==> Nprg \<in> Always 192 {s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s 193 --> Nonce NA \<notin> analz (spies s)}" 194apply ns_induct 195txt\<open>NS3\<close> 196prefer 4 apply (blast intro: no_nonce_NS1_NS2_reachable) 197txt\<open>NS2\<close> 198prefer 3 apply (blast dest: unique_NA) 199txt\<open>NS1\<close> 200prefer 2 apply blast 201txt\<open>Fake\<close> 202apply spy_analz 203done 204 205 206text\<open>Authentication for A: if she receives message 2 and has used NA 207 to start a run, then B has sent message 2.\<close> 208lemma A_trusts_NS2: 209 "[| A \<notin> bad; B \<notin> bad |] 210 ==> Nprg \<in> Always 211 {s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s & 212 Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (knows Spy s) 213 --> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s}" 214 (*insert an invariant for use in some of the subgoals*) 215apply (insert Spy_not_see_NA [of A B NA], simp, ns_induct) 216apply (auto dest: unique_NA) 217done 218 219 220text\<open>If the encrypted message appears then it originated with Alice in NS1\<close> 221lemma B_trusts_NS1: 222 "Nprg \<in> Always 223 {s. Nonce NA \<notin> analz (spies s) --> 224 Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies s) 225 --> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s}" 226apply ns_induct 227apply blast 228done 229 230 231subsection\<open>Authenticity properties obtained from NS2\<close> 232 233text\<open>Unicity for NS2: nonce NB identifies nonce NA and agent A. 234 Proof closely follows that of \<open>unique_NA\<close>.\<close> 235lemma unique_NB_lemma: 236 "Nprg 237 \<in> Always {s. Nonce NB \<notin> analz (spies s) --> 238 Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies s) --> 239 Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies s) --> 240 A=A' & NA=NA'}" 241apply ns_induct 242apply auto 243txt\<open>Fake, NS2 are non-trivial\<close> 244done 245 246lemma unique_NB: 247 "[| Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies s); 248 Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies s); 249 Nonce NB \<notin> analz (spies s); 250 s \<in> reachable Nprg |] 251 ==> A=A' & NA=NA'" 252apply (blast dest: unique_NB_lemma [THEN Always_Collect_reachableD]) 253done 254 255 256text\<open>NB remains secret PROVIDED Alice never responds with round 3\<close> 257lemma Spy_not_see_NB: 258 "[| A \<notin> bad; B \<notin> bad |] 259 ==> Nprg \<in> Always 260 {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s & 261 (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set s) 262 --> Nonce NB \<notin> analz (spies s)}" 263apply ns_induct 264apply (simp_all (no_asm_simp) add: all_conj_distrib) 265txt\<open>NS3: because NB determines A\<close> 266prefer 4 apply (blast dest: unique_NB) 267txt\<open>NS2: by freshness and unicity of NB\<close> 268prefer 3 apply (blast intro: no_nonce_NS1_NS2_reachable) 269txt\<open>NS1: by freshness\<close> 270prefer 2 apply blast 271txt\<open>Fake\<close> 272apply spy_analz 273done 274 275 276 277text\<open>Authentication for B: if he receives message 3 and has used NB 278 in message 2, then A has sent message 3--to somebody....\<close> 279lemma B_trusts_NS3: 280 "[| A \<notin> bad; B \<notin> bad |] 281 ==> Nprg \<in> Always 282 {s. Crypt (pubK B) (Nonce NB) \<in> parts (spies s) & 283 Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s 284 --> (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set s)}" 285 (*insert an invariant for use in some of the subgoals*) 286apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct) 287apply (simp_all (no_asm_simp) add: ex_disj_distrib) 288apply auto 289txt\<open>NS3: because NB determines A. This use of \<open>unique_NB\<close> is robust.\<close> 290apply (blast intro: unique_NB [THEN conjunct1]) 291done 292 293 294text\<open>Can we strengthen the secrecy theorem? NO\<close> 295lemma "[| A \<notin> bad; B \<notin> bad |] 296 ==> Nprg \<in> Always 297 {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s 298 --> Nonce NB \<notin> analz (spies s)}" 299apply ns_induct 300apply auto 301txt\<open>Fake\<close> 302apply spy_analz 303txt\<open>NS2: by freshness and unicity of NB\<close> 304 apply (blast intro: no_nonce_NS1_NS2_reachable) 305txt\<open>NS3: unicity of NB identifies A and NA, but not B\<close> 306apply (frule_tac A'=A in Says_imp_spies [THEN parts.Inj, THEN unique_NB]) 307apply (erule Says_imp_spies [THEN parts.Inj], auto) 308apply (rename_tac s B' C) 309txt\<open>This is the attack! 310@{subgoals[display,indent=0,margin=65]} 311\<close> 312oops 313 314 315(* 316THIS IS THE ATTACK! 317[| A \<notin> bad; B \<notin> bad |] 318==> Nprg 319 \<in> Always 320 {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s --> 321 Nonce NB \<notin> analz (knows Spy s)} 322 1. !!s B' C. 323 [| A \<notin> bad; B \<notin> bad; s \<in> reachable Nprg 324 Says A C (Crypt (pubK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s; 325 Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s; 326 C \<in> bad; Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s; 327 Nonce NB \<notin> analz (knows Spy s) |] 328 ==> False 329*) 330 331end 332