1(* Title: HOL/Auth/NS_Public.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4 5Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. 6Version incorporating Lowe's fix (inclusion of B's identity in round 2). 7*) 8 9section\<open>Verifying the Needham-Schroeder-Lowe Public-Key Protocol\<close> 10 11theory NS_Public imports Public begin 12 13inductive_set ns_public :: "event list set" 14 where 15 (*Initial trace is empty*) 16 Nil: "[] \<in> ns_public" 17 18 (*The spy MAY say anything he CAN say. We do not expect him to 19 invent new nonces here, but he can also use NS1. Common to 20 all similar protocols.*) 21 | Fake: "\<lbrakk>evsf \<in> ns_public; X \<in> synth (analz (spies evsf))\<rbrakk> 22 \<Longrightarrow> Says Spy B X # evsf \<in> ns_public" 23 24 (*Alice initiates a protocol run, sending a nonce to Bob*) 25 | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> 26 \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) 27 # evs1 \<in> ns_public" 28 29 (*Bob responds to Alice's message with a further nonce*) 30 | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; 31 Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> 32 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) 33 # evs2 \<in> ns_public" 34 35 (*Alice proves her existence by sending NB back to Bob.*) 36 | NS3: "\<lbrakk>evs3 \<in> ns_public; 37 Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; 38 Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) 39 \<in> set evs3\<rbrakk> 40 \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" 41 42declare knows_Spy_partsEs [elim] 43declare knows_Spy_partsEs [elim] 44declare analz_into_parts [dest] 45declare Fake_parts_insert_in_Un [dest] 46 47(*A "possibility property": there are traces that reach the end*) 48lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs" 49apply (intro exI bexI) 50apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, 51 THEN ns_public.NS3], possibility) 52done 53 54(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY 55 sends messages containing X! **) 56 57(*Spy never sees another agent's private key! (unless it's bad at start)*) 58lemma Spy_see_priEK [simp]: 59 "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> parts (spies evs)) = (A \<in> bad)" 60by (erule ns_public.induct, auto) 61 62lemma Spy_analz_priEK [simp]: 63 "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)" 64by auto 65 66subsection\<open>Authenticity properties obtained from NS2\<close> 67 68 69(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce 70 is secret. (Honest users generate fresh nonces.)*) 71lemma no_nonce_NS1_NS2 [rule_format]: 72 "evs \<in> ns_public 73 \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs) \<longrightarrow> 74 Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow> 75 Nonce NA \<in> analz (spies evs)" 76apply (erule ns_public.induct, simp_all) 77apply (blast intro: analz_insertI)+ 78done 79 80(*Unicity for NS1: nonce NA identifies agents A and B*) 81lemma unique_NA: 82 "\<lbrakk>Crypt(pubEK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs); 83 Crypt(pubEK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs); 84 Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk> 85 \<Longrightarrow> A=A' \<and> B=B'" 86apply (erule rev_mp, erule rev_mp, erule rev_mp) 87apply (erule ns_public.induct, simp_all) 88(*Fake, NS1*) 89apply (blast intro: analz_insertI)+ 90done 91 92 93(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure 94 The major premise "Says A B ..." makes it a dest-rule, so we use 95 (erule rev_mp) rather than rule_format. *) 96theorem Spy_not_see_NA: 97 "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; 98 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> 99 \<Longrightarrow> Nonce NA \<notin> analz (spies evs)" 100apply (erule rev_mp) 101apply (erule ns_public.induct, simp_all, spy_analz) 102apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ 103done 104 105 106(*Authentication for A: if she receives message 2 and has used NA 107 to start a run, then B has sent message 2.*) 108lemma A_trusts_NS2_lemma [rule_format]: 109 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> 110 \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs) \<longrightarrow> 111 Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow> 112 Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs" 113apply (erule ns_public.induct, simp_all) 114(*Fake, NS1*) 115apply (blast dest: Spy_not_see_NA)+ 116done 117 118theorem A_trusts_NS2: 119 "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; 120 Says B' A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; 121 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> 122 \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs" 123by (blast intro: A_trusts_NS2_lemma) 124 125 126(*If the encrypted message appears then it originated with Alice in NS1*) 127lemma B_trusts_NS1 [rule_format]: 128 "evs \<in> ns_public 129 \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow> 130 Nonce NA \<notin> analz (spies evs) \<longrightarrow> 131 Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs" 132apply (erule ns_public.induct, simp_all) 133(*Fake*) 134apply (blast intro!: analz_insertI) 135done 136 137 138subsection\<open>Authenticity properties obtained from NS2\<close> 139 140(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 141 [unicity of B makes Lowe's fix work] 142 [proof closely follows that for unique_NA] *) 143 144lemma unique_NB [dest]: 145 "\<lbrakk>Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(spies evs); 146 Crypt(pubEK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(spies evs); 147 Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk> 148 \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B'" 149apply (erule rev_mp, erule rev_mp, erule rev_mp) 150apply (erule ns_public.induct, simp_all) 151(*Fake, NS2*) 152apply (blast intro: analz_insertI)+ 153done 154 155 156(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) 157theorem Spy_not_see_NB [dest]: 158 "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; 159 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> 160 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" 161apply (erule rev_mp) 162apply (erule ns_public.induct, simp_all, spy_analz) 163apply (blast intro: no_nonce_NS1_NS2)+ 164done 165 166 167(*Authentication for B: if he receives message 3 and has used NB 168 in message 2, then A has sent message 3.*) 169lemma B_trusts_NS3_lemma [rule_format]: 170 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> 171 Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow> 172 Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow> 173 Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs" 174by (erule ns_public.induct, auto) 175 176theorem B_trusts_NS3: 177 "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; 178 Says A' B (Crypt (pubEK B) (Nonce NB)) \<in> set evs; 179 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> 180 \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs" 181by (blast intro: B_trusts_NS3_lemma) 182 183subsection\<open>Overall guarantee for B\<close> 184 185(*If NS3 has been sent and the nonce NB agrees with the nonce B joined with 186 NA, then A initiated the run using NA.*) 187theorem B_trusts_protocol: 188 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> 189 Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow> 190 Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow> 191 Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs" 192by (erule ns_public.induct, auto) 193 194end 195