|
1 (* Title: HOL/Auth/NS_Public |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1996 University of Cambridge |
|
4 |
|
5 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. |
|
6 Version incorporating Lowe's fix (inclusion of B's identity in round 2). |
|
7 *)(*<*) |
|
8 theory NS_Public imports Public begin(*>*) |
|
9 |
|
10 section{* Modelling the Protocol \label{sec:modelling} *} |
|
11 |
|
12 text_raw {* |
|
13 \begin{figure} |
|
14 \begin{isabelle} |
|
15 *} |
|
16 |
|
17 inductive_set ns_public :: "event list set" |
|
18 where |
|
19 |
|
20 Nil: "[] \<in> ns_public" |
|
21 |
|
22 |
|
23 | Fake: "\<lbrakk>evsf \<in> ns_public; X \<in> synth (analz (knows Spy evsf))\<rbrakk> |
|
24 \<Longrightarrow> Says Spy B X # evsf \<in> ns_public" |
|
25 |
|
26 |
|
27 | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
|
28 \<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
|
29 # evs1 \<in> ns_public" |
|
30 |
|
31 |
|
32 | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
|
33 Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
|
34 \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) |
|
35 # evs2 \<in> ns_public" |
|
36 |
|
37 |
|
38 | NS3: "\<lbrakk>evs3 \<in> ns_public; |
|
39 Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
|
40 Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) |
|
41 \<in> set evs3\<rbrakk> |
|
42 \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public" |
|
43 |
|
44 text_raw {* |
|
45 \end{isabelle} |
|
46 \caption{An Inductive Protocol Definition}\label{fig:ns_public} |
|
47 \end{figure} |
|
48 *} |
|
49 |
|
50 text {* |
|
51 Let us formalize the Needham-Schroeder public-key protocol, as corrected by |
|
52 Lowe: |
|
53 \begin{alignat*% |
|
54 }{2} |
|
55 &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ |
|
56 &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ |
|
57 &3.&\quad A\to B &: \comp{Nb}\sb{Kb} |
|
58 \end{alignat*% |
|
59 } |
|
60 |
|
61 Each protocol step is specified by a rule of an inductive definition. An |
|
62 event trace has type @{text "event list"}, so we declare the constant |
|
63 @{text ns_public} to be a set of such traces. |
|
64 |
|
65 Figure~\ref{fig:ns_public} presents the inductive definition. The |
|
66 @{text Nil} rule introduces the empty trace. The @{text Fake} rule models the |
|
67 adversary's sending a message built from components taken from past |
|
68 traffic, expressed using the functions @{text synth} and |
|
69 @{text analz}. |
|
70 The next three rules model how honest agents would perform the three |
|
71 protocol steps. |
|
72 |
|
73 Here is a detailed explanation of rule @{text NS2}. |
|
74 A trace containing an event of the form |
|
75 @{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"} |
|
76 may be extended by an event of the form |
|
77 @{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"} |
|
78 where @{text NB} is a fresh nonce: @{term "Nonce NB \<notin> used evs2"}. |
|
79 Writing the sender as @{text A'} indicates that @{text B} does not |
|
80 know who sent the message. Calling the trace variable @{text evs2} rather |
|
81 than simply @{text evs} helps us know where we are in a proof after many |
|
82 case-splits: every subgoal mentioning @{text evs2} involves message~2 of the |
|
83 protocol. |
|
84 |
|
85 Benefits of this approach are simplicity and clarity. The semantic model |
|
86 is set theory, proofs are by induction and the translation from the informal |
|
87 notation to the inductive rules is straightforward. |
|
88 *} |
|
89 |
|
90 section{* Proving Elementary Properties \label{sec:regularity} *} |
|
91 |
|
92 (*<*) |
|
93 declare knows_Spy_partsEs [elim] |
|
94 declare analz_subset_parts [THEN subsetD, dest] |
|
95 declare Fake_parts_insert [THEN subsetD, dest] |
|
96 declare image_eq_UN [simp] (*accelerates proofs involving nested images*) |
|
97 |
|
98 (*A "possibility property": there are traces that reach the end*) |
|
99 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs" |
|
100 apply (intro exI bexI) |
|
101 apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, |
|
102 THEN ns_public.NS3]) |
|
103 by possibility |
|
104 |
|
105 |
|
106 (**** Inductive proofs about ns_public ****) |
|
107 |
|
108 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
|
109 sends messages containing X! **) |
|
110 |
|
111 (*Spy never sees another agent's private key! (unless it's bad at start)*) |
|
112 (*>*) |
|
113 |
|
114 text {* |
|
115 Secrecy properties can be hard to prove. The conclusion of a typical |
|
116 secrecy theorem is |
|
117 @{term "X \<notin> analz (knows Spy evs)"}. The difficulty arises from |
|
118 having to reason about @{text analz}, or less formally, showing that the spy |
|
119 can never learn~@{text X}. Much easier is to prove that @{text X} can never |
|
120 occur at all. Such \emph{regularity} properties are typically expressed |
|
121 using @{text parts} rather than @{text analz}. |
|
122 |
|
123 The following lemma states that @{text A}'s private key is potentially |
|
124 known to the spy if and only if @{text A} belongs to the set @{text bad} of |
|
125 compromised agents. The statement uses @{text parts}: the very presence of |
|
126 @{text A}'s private key in a message, whether protected by encryption or |
|
127 not, is enough to confirm that @{text A} is compromised. The proof, like |
|
128 nearly all protocol proofs, is by induction over traces. |
|
129 *} |
|
130 |
|
131 lemma Spy_see_priK [simp]: |
|
132 "evs \<in> ns_public |
|
133 \<Longrightarrow> (Key (priK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
134 apply (erule ns_public.induct, simp_all) |
|
135 txt {* |
|
136 The induction yields five subgoals, one for each rule in the definition of |
|
137 @{text ns_public}. The idea is to prove that the protocol property holds initially |
|
138 (rule @{text Nil}), is preserved by each of the legitimate protocol steps (rules |
|
139 @{text NS1}--@{text 3}), and even is preserved in the face of anything the |
|
140 spy can do (rule @{text Fake}). |
|
141 |
|
142 The proof is trivial. No legitimate protocol rule sends any keys |
|
143 at all, so only @{text Fake} is relevant. Indeed, simplification leaves |
|
144 only the @{text Fake} case, as indicated by the variable name @{text evsf}: |
|
145 @{subgoals[display,indent=0,margin=65]} |
|
146 *} |
|
147 by blast |
|
148 (*<*) |
|
149 lemma Spy_analz_priK [simp]: |
|
150 "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
151 by auto |
|
152 (*>*) |
|
153 |
|
154 text {* |
|
155 The @{text Fake} case is proved automatically. If |
|
156 @{term "priK A"} is in the extended trace then either (1) it was already in the |
|
157 original trace or (2) it was |
|
158 generated by the spy, who must have known this key already. |
|
159 Either way, the induction hypothesis applies. |
|
160 |
|
161 \emph{Unicity} lemmas are regularity lemmas stating that specified items |
|
162 can occur only once in a trace. The following lemma states that a nonce |
|
163 cannot be used both as $Na$ and as $Nb$ unless |
|
164 it is known to the spy. Intuitively, it holds because honest agents |
|
165 always choose fresh values as nonces; only the spy might reuse a value, |
|
166 and he doesn't know this particular value. The proof script is short: |
|
167 induction, simplification, @{text blast}. The first line uses the rule |
|
168 @{text rev_mp} to prepare the induction by moving two assumptions into the |
|
169 induction formula. |
|
170 *} |
|
171 |
|
172 lemma no_nonce_NS1_NS2: |
|
173 "\<lbrakk>Crypt (pubK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (knows Spy evs); |
|
174 Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (knows Spy evs); |
|
175 evs \<in> ns_public\<rbrakk> |
|
176 \<Longrightarrow> Nonce NA \<in> analz (knows Spy evs)" |
|
177 apply (erule rev_mp, erule rev_mp) |
|
178 apply (erule ns_public.induct, simp_all) |
|
179 apply (blast intro: analz_insertI)+ |
|
180 done |
|
181 |
|
182 text {* |
|
183 The following unicity lemma states that, if \isa{NA} is secret, then its |
|
184 appearance in any instance of message~1 determines the other components. |
|
185 The proof is similar to the previous one. |
|
186 *} |
|
187 |
|
188 lemma unique_NA: |
|
189 "\<lbrakk>Crypt(pubK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(knows Spy evs); |
|
190 Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(knows Spy evs); |
|
191 Nonce NA \<notin> analz (knows Spy evs); evs \<in> ns_public\<rbrakk> |
|
192 \<Longrightarrow> A=A' \<and> B=B'" |
|
193 (*<*) |
|
194 apply (erule rev_mp, erule rev_mp, erule rev_mp) |
|
195 apply (erule ns_public.induct, simp_all) |
|
196 (*Fake, NS1*) |
|
197 apply (blast intro: analz_insertI)+ |
|
198 done |
|
199 (*>*) |
|
200 |
|
201 section{* Proving Secrecy Theorems \label{sec:secrecy} *} |
|
202 |
|
203 (*<*) |
|
204 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure |
|
205 The major premise "Says A B ..." makes it a dest-rule, so we use |
|
206 (erule rev_mp) rather than rule_format. *) |
|
207 theorem Spy_not_see_NA: |
|
208 "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
|
209 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
|
210 \<Longrightarrow> Nonce NA \<notin> analz (knows Spy evs)" |
|
211 apply (erule rev_mp) |
|
212 apply (erule ns_public.induct, simp_all) |
|
213 apply spy_analz |
|
214 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ |
|
215 done |
|
216 |
|
217 |
|
218 (*Authentication for A: if she receives message 2 and has used NA |
|
219 to start a run, then B has sent message 2.*) |
|
220 lemma A_trusts_NS2_lemma [rule_format]: |
|
221 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
|
222 \<Longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> |
|
223 Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow> |
|
224 Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs" |
|
225 apply (erule ns_public.induct, simp_all) |
|
226 (*Fake, NS1*) |
|
227 apply (blast dest: Spy_not_see_NA)+ |
|
228 done |
|
229 |
|
230 theorem A_trusts_NS2: |
|
231 "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
|
232 Says B' A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; |
|
233 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
|
234 \<Longrightarrow> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs" |
|
235 by (blast intro: A_trusts_NS2_lemma) |
|
236 |
|
237 |
|
238 (*If the encrypted message appears then it originated with Alice in NS1*) |
|
239 lemma B_trusts_NS1 [rule_format]: |
|
240 "evs \<in> ns_public |
|
241 \<Longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> |
|
242 Nonce NA \<notin> analz (knows Spy evs) \<longrightarrow> |
|
243 Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs" |
|
244 apply (erule ns_public.induct, simp_all) |
|
245 (*Fake*) |
|
246 apply (blast intro!: analz_insertI) |
|
247 done |
|
248 |
|
249 |
|
250 |
|
251 (*** Authenticity properties obtained from NS2 ***) |
|
252 |
|
253 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B |
|
254 [unicity of B makes Lowe's fix work] |
|
255 [proof closely follows that for unique_NA] *) |
|
256 |
|
257 lemma unique_NB [dest]: |
|
258 "\<lbrakk>Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(knows Spy evs); |
|
259 Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(knows Spy evs); |
|
260 Nonce NB \<notin> analz (knows Spy evs); evs \<in> ns_public\<rbrakk> |
|
261 \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B'" |
|
262 apply (erule rev_mp, erule rev_mp, erule rev_mp) |
|
263 apply (erule ns_public.induct, simp_all) |
|
264 (*Fake, NS2*) |
|
265 apply (blast intro: analz_insertI)+ |
|
266 done |
|
267 (*>*) |
|
268 |
|
269 text {* |
|
270 The secrecy theorems for Bob (the second participant) are especially |
|
271 important because they fail for the original protocol. The following |
|
272 theorem states that if Bob sends message~2 to Alice, and both agents are |
|
273 uncompromised, then Bob's nonce will never reach the spy. |
|
274 *} |
|
275 |
|
276 theorem Spy_not_see_NB [dest]: |
|
277 "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; |
|
278 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
|
279 \<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)" |
|
280 txt {* |
|
281 To prove it, we must formulate the induction properly (one of the |
|
282 assumptions mentions~@{text evs}), apply induction, and simplify: |
|
283 *} |
|
284 |
|
285 apply (erule rev_mp, erule ns_public.induct, simp_all) |
|
286 (*<*) |
|
287 apply spy_analz |
|
288 defer |
|
289 apply (blast intro: no_nonce_NS1_NS2) |
|
290 apply (blast intro: no_nonce_NS1_NS2) |
|
291 (*>*) |
|
292 |
|
293 txt {* |
|
294 The proof states are too complicated to present in full. |
|
295 Let's examine the simplest subgoal, that for message~1. The following |
|
296 event has just occurred: |
|
297 \[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'} \] |
|
298 The variables above have been primed because this step |
|
299 belongs to a different run from that referred to in the theorem |
|
300 statement --- the theorem |
|
301 refers to a past instance of message~2, while this subgoal |
|
302 concerns message~1 being sent just now. |
|
303 In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$ |
|
304 we have @{text Ba} and~@{text NAa}: |
|
305 @{subgoals[display,indent=0]} |
|
306 The simplifier has used a |
|
307 default simplification rule that does a case |
|
308 analysis for each encrypted message on whether or not the decryption key |
|
309 is compromised. |
|
310 @{named_thms [display,indent=0,margin=50] analz_Crypt_if [no_vars] (analz_Crypt_if)} |
|
311 The simplifier has also used @{text Spy_see_priK}, proved in |
|
312 {\S}\ref{sec:regularity} above, to yield @{term "Ba \<in> bad"}. |
|
313 |
|
314 Recall that this subgoal concerns the case |
|
315 where the last message to be sent was |
|
316 \[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'}. \] |
|
317 This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised, |
|
318 allowing the spy to decrypt the message. The Isabelle subgoal says |
|
319 precisely this, if we allow for its choice of variable names. |
|
320 Proving @{term "NB \<noteq> NAa"} is easy: @{text NB} was |
|
321 sent earlier, while @{text NAa} is fresh; formally, we have |
|
322 the assumption @{term "Nonce NAa \<notin> used evs1"}. |
|
323 |
|
324 Note that our reasoning concerned @{text B}'s participation in another |
|
325 run. Agents may engage in several runs concurrently, and some attacks work |
|
326 by interleaving the messages of two runs. With model checking, this |
|
327 possibility can cause a state-space explosion, and for us it |
|
328 certainly complicates proofs. The biggest subgoal concerns message~2. It |
|
329 splits into several cases, such as whether or not the message just sent is |
|
330 the very message mentioned in the theorem statement. |
|
331 Some of the cases are proved by unicity, others by |
|
332 the induction hypothesis. For all those complications, the proofs are |
|
333 automatic by @{text blast} with the theorem @{text no_nonce_NS1_NS2}. |
|
334 |
|
335 The remaining theorems about the protocol are not hard to prove. The |
|
336 following one asserts a form of \emph{authenticity}: if |
|
337 @{text B} has sent an instance of message~2 to~@{text A} and has received the |
|
338 expected reply, then that reply really originated with~@{text A}. The |
|
339 proof is a simple induction. |
|
340 *} |
|
341 |
|
342 (*<*) |
|
343 by (blast intro: no_nonce_NS1_NS2) |
|
344 |
|
345 lemma B_trusts_NS3_lemma [rule_format]: |
|
346 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> |
|
347 Crypt (pubK B) (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> |
|
348 Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow> |
|
349 Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs" |
|
350 by (erule ns_public.induct, auto) |
|
351 (*>*) |
|
352 theorem B_trusts_NS3: |
|
353 "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; |
|
354 Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs; |
|
355 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
|
356 \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs" |
|
357 (*<*) |
|
358 by (blast intro: B_trusts_NS3_lemma) |
|
359 |
|
360 (*** Overall guarantee for B ***) |
|
361 |
|
362 |
|
363 (*If NS3 has been sent and the nonce NB agrees with the nonce B joined with |
|
364 NA, then A initiated the run using NA.*) |
|
365 theorem B_trusts_protocol [rule_format]: |
|
366 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> |
|
367 Crypt (pubK B) (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> |
|
368 Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow> |
|
369 Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs" |
|
370 by (erule ns_public.induct, auto) |
|
371 (*>*) |
|
372 |
|
373 text {* |
|
374 From similar assumptions, we can prove that @{text A} started the protocol |
|
375 run by sending an instance of message~1 involving the nonce~@{text NA}\@. |
|
376 For this theorem, the conclusion is |
|
377 @{thm [display] (concl) B_trusts_protocol [no_vars]} |
|
378 Analogous theorems can be proved for~@{text A}, stating that nonce~@{text NA} |
|
379 remains secret and that message~2 really originates with~@{text B}. Even the |
|
380 flawed protocol establishes these properties for~@{text A}; |
|
381 the flaw only harms the second participant. |
|
382 |
|
383 \medskip |
|
384 |
|
385 Detailed information on this protocol verification technique can be found |
|
386 elsewhere~\cite{paulson-jcs}, including proofs of an Internet |
|
387 protocol~\cite{paulson-tls}. We must stress that the protocol discussed |
|
388 in this chapter is trivial. There are only three messages; no keys are |
|
389 exchanged; we merely have to prove that encrypted data remains secret. |
|
390 Real world protocols are much longer and distribute many secrets to their |
|
391 participants. To be realistic, the model has to include the possibility |
|
392 of keys being lost dynamically due to carelessness. If those keys have |
|
393 been used to encrypt other sensitive information, there may be cascading |
|
394 losses. We may still be able to establish a bound on the losses and to |
|
395 prove that other protocol runs function |
|
396 correctly~\cite{paulson-yahalom}. Proofs of real-world protocols follow |
|
397 the strategy illustrated above, but the subgoals can |
|
398 be much bigger and there are more of them. |
|
399 \index{protocols!security|)} |
|
400 *} |
|
401 |
|
402 (*<*)end(*>*) |