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