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