|
1 % $Id$ |
|
2 \chapter{Case Study: Verifying a Cryptographic Protocol} |
|
3 \label{chap:crypto} |
|
4 |
|
5 %crypto primitives FIXME: GET RID OF MANY |
|
6 \def\lbb{\mathopen{\{\kern-.30em|}} |
|
7 \def\rbb{\mathclose{|\kern-.32em\}}} |
|
8 \def\comp#1{\lbb#1\rbb} |
|
9 |
|
10 Communications security is an ancient art. Julius Caesar is said to have |
|
11 encrypted his messages, shifting each letter three places along the |
|
12 alphabet. Mary Queen of Scots was convicted of treason after a cipher used |
|
13 in her letters was broken. Today's postal system incorporates security |
|
14 features. The envelope provides a degree of |
|
15 \emph{secrecy}. The signature provides \emph{authenticity} (proof of |
|
16 origin), as do departmental stamps and letterheads. |
|
17 |
|
18 Networks are vulnerable: messages pass through many computers, any of which |
|
19 might be controlled an adversary, who thus can capture or redirect |
|
20 messages. People who wish to communicate securely over such a network can |
|
21 use cryptography, but if they are to understand each other, they need to |
|
22 follow a |
|
23 \emph{protocol}: a pre-arranged sequence of message formats. |
|
24 |
|
25 Protocols can be attacked in many ways, even if encryption is unbreakable. |
|
26 A \emph{splicing attack} involves an adversary's sending a message composed |
|
27 of parts of several old messages. This fake message may have the correct |
|
28 format, fooling an honest party. The adversary might be able to masquerade |
|
29 as somebody else, or he might obtain a secret key. |
|
30 |
|
31 \emph{Nonces} help prevent splicing attacks. A typical nonce is a 20-byte |
|
32 random number. Each message that requires a reply incorporates a nonce. The |
|
33 reply must include a copy of that nonce, to prove that it is not a replay of |
|
34 a past message. Nonces must be cryptographically protected, since |
|
35 otherwise an adversary could easily generate fakes. You should be starting |
|
36 to see that protocol design is tricky! |
|
37 |
|
38 Researchers are developing methods for proving the correctness of security |
|
39 protocols. The Needham-Schroeder public-key |
|
40 protocol~\cite{needham-schroeder} has become a standard test case. |
|
41 Proposed in 1978, it was found to be defective nearly two decades |
|
42 later~\cite{lowe-fdr}. This toy protocol will be useful in demonstrating |
|
43 how to verify protocols using Isabelle. |
|
44 |
|
45 |
|
46 \section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol} |
|
47 |
|
48 This protocol uses public-key cryptography. Each person has a private key, known only to |
|
49 himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she |
|
50 encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the |
|
51 matching private key, which is needed in order to decrypt Alice's message. |
|
52 |
|
53 The core of the Needham-Schroeder protocol consists of three messages: |
|
54 \begin{alignat*}{2} |
|
55 &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ |
|
56 &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ |
|
57 &3.&\quad A\to B &: \comp{Nb}\sb{Kb} |
|
58 \end{alignat*} |
|
59 First, let's understand the notation. In the first message, Alice |
|
60 sends Bob a message consisting of a nonce generated by Alice~($Na$) |
|
61 paired with Alice's name~($A$) and encrypted using Bob's public |
|
62 key~($Kb$). In the second message, Bob sends Alice a message |
|
63 consisting of $Na$ paired with a nonce generated by Bob~($Nb$), |
|
64 encrypted using Alice's public key~($Ka$). In the last message, Alice |
|
65 returns $Nb$ to Bob, encrypted using his public key. |
|
66 |
|
67 When Alice receives Message~2, she knows that Bob has acted on her |
|
68 message, since only he could have decrypted |
|
69 $\comp{Na,A}\sb{Kb}$ and extracted~$Na$. That is precisely what |
|
70 nonces are for. Similarly, message~3 assures Bob that Alice is |
|
71 active. But the protocol was widely believed~\cite{ban89} to satisfy a |
|
72 further property: that |
|
73 $Na$ and~$Nb$ were secrets shared by Alice and Bob. (Many |
|
74 protocols generate such shared secrets, which can be used |
|
75 to lessen the reliance on slow public-key operations.) Lowe found this |
|
76 claim to be false: if Alice runs the protocol with someone untrustworthy |
|
77 (Charlie say), then he can start a new run with another agent (Bob say). |
|
78 Charlie uses Alice as an oracle, masquerading as |
|
79 Alice to Bob~\cite{lowe-fdr}. |
|
80 \begin{alignat*}{4} |
|
81 &1.&\quad A\to C &: \comp{Na,A}\sb{Kc} & |
|
82 \qquad 1'.&\quad C\to B &: \comp{Na,A}\sb{Kb} \\ |
|
83 &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ |
|
84 &3.&\quad A\to C &: \comp{Nb}\sb{Kc} & |
|
85 3'.&\quad A\to B &: \comp{Nb}\sb{Kb} |
|
86 \end{alignat*} |
|
87 In messages~1 and~3, Charlie removes the encryption using his private |
|
88 key and re-encrypts Alice's messages using Bob's public key. Bob is |
|
89 left thinking he has run the protocol with Alice, which was not |
|
90 Alice's intention, and Bob is unaware that the ``secret'' nonces are |
|
91 known to Charlie. This is a typical man-in-the-middle attack launched |
|
92 by an insider. |
|
93 |
|
94 Lowe also suggested a fix, namely to include Bob's name in message~2: |
|
95 \begin{alignat*}{2} |
|
96 &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ |
|
97 &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ |
|
98 &3.&\quad A\to B &: \comp{Nb}\sb{Kb} |
|
99 \end{alignat*} |
|
100 If Charlie tries the same attack, Alice will receive the message |
|
101 $\comp{Na,Nb,B}\sb{Ka}$ when she was expecting to receive |
|
102 $\comp{Na,Nb,C}\sb{Ka}$. She will abandon the run, and eventually so |
|
103 will Bob. |
|
104 |
|
105 In ground-breaking work, Lowe~\cite{lowe-fdr} showed how such attacks |
|
106 could be found automatically using a model checker. An alternative, |
|
107 which we shall examine below, is to prove protocols correct. Proofs |
|
108 can be done under more realistic assumptions because our model does |
|
109 not have to be finite. The strategy is to formalize the operational |
|
110 semantics of the system and to prove security properties using rule |
|
111 induction. |
|
112 |
|
113 |
|
114 \section{Agents and Messages} |
|
115 |
|
116 All protocol specifications refer to a syntactic theory of messages. |
|
117 Datatype |
|
118 \isa{agent} introduces the constant \isa{Server} (a trusted central |
|
119 machine, needed for some protocols), an infinite population of ``friendly'' |
|
120 agents, and the~\isa{Spy}: |
|
121 \begin{isabelle} |
|
122 \isacommand{datatype}\ agent\ =\ Server\ |\ Friend\ nat\ |\ Spy |
|
123 \end{isabelle} |
|
124 % |
|
125 Keys are just natural numbers. Function \isa{invKey} maps a public key to |
|
126 the matching private key, and vice versa: |
|
127 \begin{isabelle} |
|
128 \isacommand{types}\ key\ =\ nat\isanewline |
|
129 \isacommand{consts}\ invKey\ ::\ "key=>key" |
|
130 \end{isabelle} |
|
131 Datatype |
|
132 \isa{msg} introduces the message forms, which include agent names, nonces, |
|
133 keys, compound messages, and encryptions. |
|
134 \begin{isabelle} |
|
135 \isacommand{datatype}\isanewline |
|
136 \ \ \ \ \ msg\ =\ Agent\ \ agent\ \ \ \ \ \isanewline |
|
137 \ \ \ \ \ \ \ \ \ |\ Nonce\ \ nat\ \ \ \ \ \ \ \isanewline |
|
138 \ \ \ \ \ \ \ \ \ |\ Key\ \ \ \ key\ \ \ \ \ \ \ \isanewline |
|
139 \ \ \ \ \ \ \ \ \ |\ MPair\ \ msg\ msg\ \ \ \isanewline |
|
140 \ \ \ \ \ \ \ \ \ |\ Crypt\ \ key\ msg\ \ \ \isanewline |
|
141 \end{isabelle} |
|
142 % |
|
143 The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ |
|
144 abbreviates |
|
145 $\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. |
|
146 |
|
147 Since datatype constructors are injective, we have the theorem |
|
148 \begin{isabelle} |
|
149 Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand X=X'. |
|
150 \end{isabelle} |
|
151 A ciphertext can be decrypted using only one key and |
|
152 can yield only one plaintext. This assumption is realistic if encryption |
|
153 includes some built-in redundancy. |
|
154 |
|
155 |
|
156 \section{Modelling the Adversary} |
|
157 |
|
158 The spy is part of the system and must be built into the model. He is |
|
159 a malicious user who does not have to follow the protocol. He |
|
160 watches the network and uses any keys he knows to decrypt messages, |
|
161 perhaps learning additional keys and nonces. He uses the items he has |
|
162 accumulated to compose new messages, which he may send to anybody. |
|
163 |
|
164 Two functions enable us to formalize this behaviour: \isa{analz} and |
|
165 \isa{synth}. Each function maps a sets of messages to another set of |
|
166 messages. The set \isa{analz H} formalizes what the adversary can learn |
|
167 from the set of messages~$H$. The closure properties of this set are |
|
168 defined inductively. |
|
169 \begin{isabelle} |
|
170 \isacommand{consts}\ \ analz\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline |
|
171 \isacommand{inductive}\ "analz\ H"\isanewline |
|
172 \ \ \isakeyword{intros}\ \isanewline |
|
173 \ \ \ \ Inj\ [intro,simp]\ :\ \ \ "X\ \isasymin \ H\ |
|
174 \isasymLongrightarrow\ X\ |
|
175 \isasymin |
|
176 \ analz\ H"\isanewline |
|
177 \ \ \ \ Fst:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\ |
|
178 \isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline |
|
179 \ \ \ \ Snd:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\ |
|
180 \isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline |
|
181 \ \ \ \ Decrypt\ [dest]:\ \isanewline |
|
182 \ \ \ \ \ \ \ \ \ \ \ \ \ "[|Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\ |
|
183 K):\ analz\ H|]\isanewline |
|
184 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ X\ \isasymin \ analz\ H" |
|
185 \end{isabelle} |
|
186 % |
|
187 Note the \isa{Decrypt} rule: the spy can decrypt a |
|
188 message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. |
|
189 Properties proved by rule induction include the following: |
|
190 \begin{isabelle} |
|
191 G\isasymsubseteq H\ \isasymLongrightarrow\ analz(G)\ \isasymsubseteq\ |
|
192 analz(H) |
|
193 \rulename{analz_mono}\isanewline |
|
194 analz (analz H) = analz H |
|
195 \rulename{analz_idem} |
|
196 \end{isabelle} |
|
197 |
|
198 The set of fake messages that an intruder could invent |
|
199 starting from~\isa{H} is \isa{synth(analz~H)}, where \isa{synth H} |
|
200 formalizes what the adversary can build from the set of messages~$H$. |
|
201 \begin{isabelle} |
|
202 \isacommand{consts}\ \ synth\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline |
|
203 \isacommand{inductive}\ "synth\ H"\isanewline |
|
204 \ \ \isakeyword{intros}\ \isanewline |
|
205 \ \ \ \ Inj\ \ \ [intro]:\ "X\ \isasymin \ H\ \isasymLongrightarrow\ |
|
206 X\ \isasymin \ synth\ H"\isanewline |
|
207 \ \ \ \ Agent\ [intro]:\ "Agent\ agt\ \isasymin \ synth\ H"\isanewline |
|
208 \ \ \ \ MPair\ [intro]:\isanewline |
|
209 \ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Y\ \isasymin |
|
210 \ synth\ H|]\ \isasymLongrightarrow\ |
|
211 \isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ synth\ H"\isanewline |
|
212 \ \ \ \ Crypt\ [intro]:\isanewline |
|
213 \ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Key K\ |
|
214 \isasymin \ H|]\ \isasymLongrightarrow\ Crypt\ K\ X\ |
|
215 \isasymin \ synth\ H" |
|
216 \end{isabelle} |
|
217 The set includes all agent names. Nonces and keys are assumed to be |
|
218 unguessable, so none are included beyond those already in~$H$. Two |
|
219 elements of \isa{synth H} can be combined, and an element can be encrypted |
|
220 using a key present in~$H$. |
|
221 |
|
222 Like \isa{analz}, this set operator is monotone and idempotent. It also |
|
223 satisfies an interesting equation involving \isa{analz}: |
|
224 \begin{isabelle} |
|
225 analz (synth H)\ =\ analz H\ \isasymunion\ synth H |
|
226 \rulename{analz_synth} |
|
227 \end{isabelle} |
|
228 % |
|
229 Rule inversion plays a major role in reasoning about \isa{synth}, through |
|
230 declarations such as this one: |
|
231 \begin{isabelle} |
|
232 \isacommand{inductive\_cases}\ Nonce_synth\ [elim!]:\ "Nonce\ n\ \isasymin |
|
233 \ synth\ H" |
|
234 \end{isabelle} |
|
235 % |
|
236 The resulting elimination rule replaces every assumption of the form |
|
237 \isa{Nonce\ n\ \isasymin \ synth\ H} by \isa{Nonce\ n\ |
|
238 \isasymin \ H}, expressing that a nonce cannot be guessed. |
|
239 %The theory also uses rule inversion with constructors \isa{Key}, \isa{Crypt} |
|
240 %and \isa{MPair} (message pairing). |
|
241 |
|
242 % |
|
243 A third operator, \isa{parts}, is useful for stating correctness |
|
244 properties. The set |
|
245 \isa{parts H} consists of the components of elements of~$H$. This set |
|
246 includes~\isa{H} and is closed under the projections from a compound |
|
247 message to its immediate parts. |
|
248 Its definition resembles that of \isa{analz} except in the rule |
|
249 corresponding to the constructor \isa{Crypt}: |
|
250 \begin{isabelle} |
|
251 \ \ \ \ \ Crypt\ K\ X\ \isasymin \ parts\ H\ \isasymLongrightarrow\ X\ |
|
252 \isasymin \ parts\ H |
|
253 \end{isabelle} |
|
254 The body of an encrypted message is always regarded as part of it. We can |
|
255 use \isa{parts} to express general well-formedness properties of a protocol, |
|
256 for example, that an uncompromised agent's private key will never be |
|
257 included as a component of any message. |
|
258 |
|
259 |
|
260 \section{Event Traces}\label{sec:events} |
|
261 |
|
262 The system's behaviour is formalized as a set of traces of |
|
263 \emph{events}. The most important event, \isa{Says~A~B~X}, expresses the |
|
264 attempt by~$A$ to send~$B$ the |
|
265 message~$X$. A trace is simply a list, constructed in reverse |
|
266 using~\isa{\#}. |
|
267 |
|
268 Sometimes the protocol requires an agent to generate a new nonce. The |
|
269 probability that a 20-byte random number has appeared before is effectively |
|
270 zero. To formalize this important property, the set \isa{used evs} |
|
271 denotes the set of all items mentioned in the trace~\isa{evs}. |
|
272 The function \isa{used} has a straightforward |
|
273 recursive definition. Here is the case for \isa{Says} event: |
|
274 \begin{isabelle} |
|
275 \ \ \ \ \ used\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\ \isacharbraceleft |
|
276 X\isacharbraceright \ \isasymunion\ (used\ evs) |
|
277 \end{isabelle} |
|
278 |
|
279 The function \isa{knows} formalizes an agent's knowledge. Mostly we only |
|
280 case about the spy's knowledge, and \isa{knows Spy evs} is the set of items |
|
281 available to the spy in the trace~\isa{evs}. Already in the empty trace, |
|
282 the spy starts with some secrets at his disposal, such as the private keys |
|
283 of compromised users. After each \isa{Says} event, the spy learns the |
|
284 message that was sent. Combinations of functions express other important |
|
285 concepts involving~\isa{evs}: |
|
286 \begin{itemize} |
|
287 \item \isa{analz (knows Spy evs)} is the items that the spy could |
|
288 learn by decryption |
|
289 \item \isa{synth (analz (knows Spy evs))} is the items that the spy |
|
290 could generate |
|
291 \end{itemize} |
|
292 |
|
293 The function |
|
294 \isa{pubK} maps agents to their public keys. The function |
|
295 \isa{priK} maps agents to their private keys, is defined in terms of |
|
296 \isa{invKey} and \isa{pubK} by a translation. |
|
297 \begin{isabelle} |
|
298 \isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline |
|
299 \isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline |
|
300 \isacommand{translations}\ \ \ \ "priK\ x"\ \ ==\ "invKey(pubK\ x)" |
|
301 \end{isabelle} |
|
302 The set \isa{bad} consists of those agents whose private keys are known to |
|
303 the spy. |
|
304 |
|
305 Two axioms are asserted about the public-key cryptosystem. |
|
306 No two agents have the same public key, and no private key equals |
|
307 any public key. |
|
308 \begin{isabelle} |
|
309 \isacommand{axioms}\isanewline |
|
310 \ \ inj_pubK:\ \ \ \ \ \ \ \ "inj\ pubK"\isanewline |
|
311 \ \ priK_neq_pubK:\ \ \ "priK\ A\ \isasymnoteq\ pubK\ B" |
|
312 \end{isabelle} |
|
313 |
|
314 |
|
315 |
|
316 |
|
317 |
|
318 \section{Modelling the Protocol}\label{sec:modelling} |
|
319 |
|
320 Let us formalize the Needham-Schroeder public-key protocol, as corrected by |
|
321 Lowe: |
|
322 \begin{alignat*}{2} |
|
323 &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ |
|
324 &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ |
|
325 &3.&\quad A\to B &: \comp{Nb}\sb{Kb} |
|
326 \end{alignat*} |
|
327 |
|
328 Each protocol step is specified by a rule of an inductive definition. An |
|
329 event trace has type \isa{event list}, so we declare the constant |
|
330 \isa{ns_public} to be a set of such traces. |
|
331 \begin{isabelle} |
|
332 \isacommand{consts}\ \ ns_public\ \ ::\ "event\ list\ set" |
|
333 \end{isabelle} |
|
334 |
|
335 \begin{figure} |
|
336 \begin{isabelle} |
|
337 \isacommand{inductive}\ ns_public\isanewline |
|
338 \ \ \isakeyword{intros}\ \isanewline |
|
339 \ \ \ \ \ \ \ \ \ \isanewline |
|
340 \ \ \ Nil:\ \ "[]\ \isasymin \ ns_public"\isanewline |
|
341 \isanewline |
|
342 \ \ \ \ \ \ \ \ \ \isanewline |
|
343 \ \ \ Fake:\ "\isasymlbrakk evsf\ \isasymin \ ns_public;\ \ X\ \isasymin \ synth\ (analz\ (spies\ evsf))\isasymrbrakk \isanewline |
|
344 \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ Spy\ B\ X\ \ \#\ evsf\ \isasymin \ ns_public"\isanewline |
|
345 \isanewline |
|
346 \ \ \ \ \ \ \ \ \ \isanewline |
|
347 \ \ \ NS1:\ \ "\isasymlbrakk evs1\ \isasymin \ ns_public;\ \ Nonce\ NA\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline |
|
348 \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\isanewline |
|
349 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs1\ \ \isasymin \ \ ns_public"\isanewline |
|
350 \isanewline |
|
351 \ \ \ \ \ \ \ \ \ \isanewline |
|
352 \ \ \ NS2:\ \ "\isasymlbrakk evs2\ \isasymin \ ns_public;\ \ Nonce\ NB\ \isasymnotin \ used\ evs2;\isanewline |
|
353 \ \ \ \ \ \ \ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs2\isasymrbrakk \isanewline |
|
354 \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline |
|
355 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs2\ \ \isasymin \ \ ns_public"\isanewline |
|
356 \isanewline |
|
357 \ \ \ \ \ \ \ \ \ \isanewline |
|
358 \ \ \ NS3:\ \ "\isasymlbrakk evs3\ \isasymin \ ns_public;\isanewline |
|
359 \ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs3;\isanewline |
|
360 \ \ \ \ \ \ \ \ \ \ \ Says\ B'\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline |
|
361 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymin \ set\ evs3\isasymrbrakk \isanewline |
|
362 \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \#\ evs3\ \isasymin \ |
|
363 ns_public" |
|
364 \end{isabelle} |
|
365 \caption{An Inductive Protocol Definition}\label{fig:ns_public} |
|
366 \end{figure} |
|
367 |
|
368 Figure~\ref{fig:ns_public} presents the inductive definition. The |
|
369 \isa{Nil} rule introduces the empty trace. The \isa{Fake} rule models the |
|
370 adversary's sending a message built from components taken from past |
|
371 traffic, expressed using the functions \isa{synth} and |
|
372 \isa{analz}. |
|
373 The next three rules model how honest agents would perform the three |
|
374 protocol steps. |
|
375 |
|
376 Here is a detailed explanation of rule \isa{NS2}. |
|
377 A trace containing an event of the form |
|
378 \begin{isabelle} |
|
379 \ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ |
|
380 NA,\ Agent\ A\isasymrbrace) |
|
381 \end{isabelle} |
|
382 % |
|
383 may be extended by an event of the form |
|
384 \begin{isabelle} |
|
385 \ \ \ \ \ Says\ B\ A\ (Crypt\ (pubK\ A)\ |
|
386 \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace) |
|
387 \end{isabelle} |
|
388 where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ \isasymnotin \ used\ evs2}. |
|
389 Writing the sender as \isa{A'} indicates that \isa{B} does not |
|
390 know who sent the message. Calling the trace variable \isa{evs2} rather |
|
391 than simply \isa{evs} helps us know where we are in a proof after many |
|
392 case-splits: every subgoal mentioning \isa{evs2} involves message~2 of the |
|
393 protocol. |
|
394 |
|
395 Benefits of this approach are simplicity and clarity. The semantic model |
|
396 is set theory, proofs are by induction and the translation from the informal |
|
397 notation to the inductive rules is straightforward. |
|
398 |
|
399 |
|
400 \section{Proving Elementary Properties} |
|
401 |
|
402 Secrecy properties are hard to prove. The conclusion of a typical secrecy |
|
403 theorem is |
|
404 \isa{X\ \isasymnotin\ analz (knows Spy evs)}. The difficulty arises from |
|
405 having to reason about \isa{analz}, or less formally, showing that the spy |
|
406 can never learn~\isa{X}. Much easier is to prove that \isa{X} can never |
|
407 occur at all. Such \emph{regularity} properties are typically expressed |
|
408 using \isa{parts} rather than \isa{analz}. |
|
409 |
|
410 The following lemma states that \isa{A}'s private key is potentially |
|
411 known to the spy if and only if \isa{A} belongs to the set \isa{bad} of |
|
412 compromised agents. The statement uses \isa{parts}: the very presence of |
|
413 her private key in a message, whether protected by encryption or not, is |
|
414 enough to confirm that \isa{A} is compromised. The proof, like nearly all |
|
415 protocol proofs, is by induction over traces. |
|
416 \begin{isabelle} |
|
417 \isacommand{lemma}\ Spy_see_priK\ [simp]:\ \isanewline |
|
418 \ \ \ \ \ \ "evs\ \isasymin \ ns_public\isanewline |
|
419 \ \ \ \ \ \ \ \isasymLongrightarrow \ |
|
420 (Key\ (priK\ A)\ \isasymin \ parts\ (spies\ evs))\ =\ (A\ \isasymin \ |
|
421 bad)"\isanewline |
|
422 \isacommand{apply}\ (erule\ ns_public.induct,\ simp_all) |
|
423 \end{isabelle} |
|
424 % |
|
425 The induction yields five subgoals, one for each rule in the definition of |
|
426 \isa{ns_public}. Informally, the idea is to prove that the protocol |
|
427 property holds initially (rule \isa{Nil}), is preserved by each of the |
|
428 legitimate protocol steps (rules \isa{NS1}--\isa{3}), and even is preserved |
|
429 in the face of anything the spy can do (rule \isa{Fake}). Simplification |
|
430 leaves only the \isa{Fake} case (as indicated by the variable name |
|
431 \isa{evsf}): |
|
432 \begin{isabelle} |
|
433 \ 1.\ \isasymAnd X\ evsf.\isanewline |
|
434 \isaindent{\ 1.\ \ \ \ }\isasymlbrakk evsf\ \isasymin \ ns_public;\isanewline |
|
435 \isaindent{\ 1.\ \ \ \ \ \ \ }(Key\ (priK\ A)\ \isasymin \ parts\ (knows\ Spy\ evsf))\ =\ (A\ \isasymin \ bad);\isanewline |
|
436 \isaindent{\ 1.\ \ \ \ \ \ \ }X\ \isasymin \ synth\ (analz\ (knows\ Spy\ evsf))\isasymrbrakk \isanewline |
|
437 \isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ (Key\ (priK\ A)\ \isasymin \ parts\ (insert\ X\ (knows\ Spy\ evsf)))\ =\isanewline |
|
438 \isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }(A\ \isasymin \ |
|
439 bad)\isanewline |
|
440 \isacommand{by}\ blast |
|
441 \end{isabelle} |
|
442 % |
|
443 The \isa{Fake} case is proved automatically. If |
|
444 \isa{priK~A} is in the extended trace then either (1) it was already in the |
|
445 original trace or (2) it was |
|
446 generated by the spy, and so the spy must have known this key already. |
|
447 Either way, the induction hypothesis applies. If the spy can tell himself |
|
448 something, then he must have known it already. |
|
449 |
|
450 \emph{Unicity} lemmas are regularity lemmas stating that specified items |
|
451 can occur only once in a trace. The following lemma states that a nonce |
|
452 cannot be used both as $Na$ and as $Nb$ unless |
|
453 it is known to the spy. Intuitively, it holds because honest agents |
|
454 always choose fresh values as nonces; only the spy might reuse a value, |
|
455 and he doesn't know this particular value. The proof script is three steps |
|
456 long. |
|
457 \begin{isabelle} |
|
458 \isacommand{lemma}\ no_nonce_NS1_NS2\ [rule_format]:\ \isanewline |
|
459 \ "evs\ \isasymin \ ns_public\ \isanewline |
|
460 \ \ \isasymLongrightarrow \ Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\ NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (spies\ evs)\ \isasymlongrightarrow \isanewline |
|
461 \ \ \ \ \ \ Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace \ \isasymin \ parts\ (spies\ evs)\ \isasymlongrightarrow \ \ \isanewline |
|
462 \ \ \ \ \ \ Nonce\ NA\ \isasymin \ analz\ (spies\ evs)" |
|
463 \end{isabelle} |
|
464 |
|
465 This unicity lemma states that, if \isa{NA} is secret, then its appearance |
|
466 in any instance of message~1 determines the other components. The proof is |
|
467 another easy induction. |
|
468 \begin{isabelle} |
|
469 \isacommand{lemma}\ unique_NA:\ \isanewline |
|
470 \ \ \ \ \ "\isasymlbrakk Crypt(pubK\ B)\ \ \isasymlbrace Nonce\ NA,\ Agent\ A\ \isasymrbrace \ \isasymin \ parts(spies\ evs);\ \ \isanewline |
|
471 \ \ \ \ \ \ \ Crypt(pubK\ B')\ \isasymlbrace Nonce\ NA,\ Agent\ A'\isasymrbrace \ \isasymin \ parts(spies\ evs);\ \ \isanewline |
|
472 \ \ \ \ \ \ \ Nonce\ NA\ \isasymnotin \ analz\ (spies\ evs);\ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline |
|
473 \ \ \ \ \ \ \isasymLongrightarrow \ A=A'\ \isasymand \ B=B'" |
|
474 \end{isabelle} |
|
475 |
|
476 |
|
477 \section{Proving Secrecy Theorems}\label{sec:secrecy} |
|
478 |
|
479 The secrecy theorems for Bob (the second participant) are especially |
|
480 important, since they fail for the original protocol. This theorem states |
|
481 that if Bob sends message~2 to Alice, and both agents are uncompromised, |
|
482 then Bob's nonce will never reach the spy. |
|
483 \begin{isabelle} |
|
484 \isacommand{theorem}\ Spy_not_see_NB\ [dest]:\isanewline |
|
485 \ "\isasymlbrakk Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline |
|
486 \ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline |
|
487 \ \ \isasymLongrightarrow \ Nonce\ NB\ \isasymnotin \ analz\ (spies\ evs)" |
|
488 \end{isabelle} |
|
489 % |
|
490 To prove this, we must formulate the induction properly (one of the |
|
491 assumptions mentions~\isa{evs}), apply induction, and simplify. |
|
492 The proof states are too complicated to present in full. |
|
493 Let's just look |
|
494 at the easiest subgoal, that for message~1: |
|
495 \begin{isabelle} |
|
496 \ 1.\ \isasymAnd Ba\ NAa\ evs1.\isanewline |
|
497 \isaindent{\ 1.\ \ \ \ }\isasymlbrakk A\ \isasymnotin \ bad;\ B\ \isasymnotin \ bad;\ evs1\ \isasymin \ ns_public;\isanewline |
|
498 \isaindent{\ 1.\ \ \ \ \ \ \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline |
|
499 \isaindent{\ 1.\ \ \ \ \ \ \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline |
|
500 \isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NB\ \isasymnotin \ analz\ (knows\ Spy\ evs1);\isanewline |
|
501 \isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NAa\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline |
|
502 \isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Ba\ \isasymin \ bad\ \isasymlongrightarrow \isanewline |
|
503 \isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline |
|
504 \isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline |
|
505 \isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }NB\ \isasymnoteq \ NAa |
|
506 \end{isabelle} |
|
507 This subgoal refers to another protocol run, in which \isa{B} has sent |
|
508 message~1 to somebody called~\isa{Ba}. Agent \isa{Ba} |
|
509 is compromised, and so the spy has learnt the nonce that was just sent, |
|
510 which is called~\isa{NAa}. We need to know that this nonce differs from the |
|
511 one we care about, namely~\isa{NB}\@. They do indeed differ: \isa{NB} was |
|
512 sent earlier, while \isa{NAa} was chosen to be fresh (we have the assumption |
|
513 \isa{Nonce\ NAa\ \isasymnotin \ used\ evs1}). |
|
514 |
|
515 Note that our reasoning concerned \isa{B}'s participation in another |
|
516 run. Agents may engage in several runs concurrently, and some attacks work |
|
517 by interleaving the messages of two runs. With model checking, this |
|
518 possibility can cause a state-space explosion, and for us it |
|
519 certainly complicates proofs. The biggest subgoal concerns message~2. It |
|
520 splits into several cases, some of which are proved by unicity, others by |
|
521 the induction hypothesis. For all those complications, the proofs are |
|
522 automatic by \isa{blast} with the theorem \isa{no_nonce_NS1_NS2}. |
|
523 |
|
524 The remaining proofs are straightforward. This theorem asserts that if |
|
525 \isa{B} has sent an instance of message~2 to~\isa{A} and has received the |
|
526 expected reply, then that reply really came from~\isa{A}. The proof is a |
|
527 simple induction. |
|
528 \begin{isabelle} |
|
529 \isacommand{theorem}\ B_trusts_NS3:\isanewline |
|
530 \ "\isasymlbrakk Says\ B\ A\ \ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline |
|
531 \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ evs;\ \isanewline |
|
532 \ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \ \ \ \ \ \ \ \ \isanewline |
|
533 \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ |
|
534 evs" |
|
535 \end{isabelle} |
|
536 |
|
537 From similar assumptions, we can prove that \isa{A} started the protocol |
|
538 run by sending an instance of message~1 involving the nonce~\isa{NA}. For |
|
539 this theorem, the conclusion is |
|
540 \begin{isabelle} |
|
541 \ \ \ \ \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ |
|
542 A\isasymrbrace )\ \isasymin \ set\ evs |
|
543 \end{isabelle} |
|
544 % |
|
545 Analogous theorems can be proved for~\isa{A}, stating that nonce~\isa{NA} |
|
546 remains secret and that message~2 really originates with~\isa{B}. Even the |
|
547 flawed protocol establishes these properties for~\isa{A}; |
|
548 the flaw only harms the second participant. |
|
549 Detailed information on this technique can be found |
|
550 elsewhere~\cite{paulson-jcs}, including proofs of an Internet |
|
551 protocol~\cite{paulson-tls}. |
|
552 |
|
553 |
|
554 \endinput |