# HG changeset patch # User paulson # Date 986911766 -7200 # Node ID 7a696a130de27be61073d473935a99044bd9a11b # Parent a9c8861e84a91ee5c708348f57932b9503a122f6 back to Unix format... diff -r a9c8861e84a9 -r 7a696a130de2 doc-src/TutorialI/Protocol/protocol.tex --- a/doc-src/TutorialI/Protocol/protocol.tex Tue Apr 10 16:02:01 2001 +0200 +++ b/doc-src/TutorialI/Protocol/protocol.tex Tue Apr 10 16:09:26 2001 +0200 @@ -1,1 +1,554 @@ -% $Id$ \chapter{Case Study: Verifying a Cryptographic Protocol} \label{chap:crypto} %crypto primitives FIXME: GET RID OF MANY \def\lbb{\mathopen{\{\kern-.30em|}} \def\rbb{\mathclose{|\kern-.32em\}}} \def\comp#1{\lbb#1\rbb} Communications security is an ancient art. Julius Caesar is said to have encrypted his messages, shifting each letter three places along the alphabet. Mary Queen of Scots was convicted of treason after a cipher used in her letters was broken. Today's postal system incorporates security features. The envelope provides a degree of \emph{secrecy}. The signature provides \emph{authenticity} (proof of origin), as do departmental stamps and letterheads. Networks are vulnerable: messages pass through many computers, any of which might be controlled an adversary, who thus can capture or redirect messages. People who wish to communicate securely over such a network can use cryptography, but if they are to understand each other, they need to follow a \emph{protocol}: a pre-arranged sequence of message formats. Protocols can be attacked in many ways, even if encryption is unbreakable. A \emph{splicing attack} involves an adversary's sending a message composed of parts of several old messages. This fake message may have the correct format, fooling an honest party. The adversary might be able to masquerade as somebody else, or he might obtain a secret key. \emph{Nonces} help prevent splicing attacks. A typical nonce is a 20-byte random number. Each message that requires a reply incorporates a nonce. The reply must include a copy of that nonce, to prove that it is not a replay of a past message. Nonces must be cryptographically protected, since otherwise an adversary could easily generate fakes. You should be starting to see that protocol design is tricky! Researchers are developing methods for proving the correctness of security protocols. The Needham-Schroeder public-key protocol~\cite{needham-schroeder} has become a standard test case. Proposed in 1978, it was found to be defective nearly two decades later~\cite{lowe-fdr}. This toy protocol will be useful in demonstrating how to verify protocols using Isabelle. \section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol} This protocol uses public-key cryptography. Each person has a private key, known only to himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the matching private key, which is needed in order to decrypt Alice's message. The core of the Needham-Schroeder protocol consists of three messages: \begin{alignat*}{2} &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ &3.&\quad A\to B &: \comp{Nb}\sb{Kb} \end{alignat*} First, let's understand the notation. In the first message, Alice sends Bob a message consisting of a nonce generated by Alice~($Na$) paired with Alice's name~($A$) and encrypted using Bob's public key~($Kb$). In the second message, Bob sends Alice a message consisting of $Na$ paired with a nonce generated by Bob~($Nb$), encrypted using Alice's public key~($Ka$). In the last message, Alice returns $Nb$ to Bob, encrypted using his public key. When Alice receives Message~2, she knows that Bob has acted on her message, since only he could have decrypted $\comp{Na,A}\sb{Kb}$ and extracted~$Na$. That is precisely what nonces are for. Similarly, message~3 assures Bob that Alice is active. But the protocol was widely believed~\cite{ban89} to satisfy a further property: that $Na$ and~$Nb$ were secrets shared by Alice and Bob. (Many protocols generate such shared secrets, which can be used to lessen the reliance on slow public-key operations.) Lowe found this claim to be false: if Alice runs the protocol with someone untrustworthy (Charlie say), then he can start a new run with another agent (Bob say). Charlie uses Alice as an oracle, masquerading as Alice to Bob~\cite{lowe-fdr}. \begin{alignat*}{4} &1.&\quad A\to C &: \comp{Na,A}\sb{Kc} & \qquad 1'.&\quad C\to B &: \comp{Na,A}\sb{Kb} \\ &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ &3.&\quad A\to C &: \comp{Nb}\sb{Kc} & 3'.&\quad A\to B &: \comp{Nb}\sb{Kb} \end{alignat*} In messages~1 and~3, Charlie removes the encryption using his private key and re-encrypts Alice's messages using Bob's public key. Bob is left thinking he has run the protocol with Alice, which was not Alice's intention, and Bob is unaware that the ``secret'' nonces are known to Charlie. This is a typical man-in-the-middle attack launched by an insider. Lowe also suggested a fix, namely to include Bob's name in message~2: \begin{alignat*}{2} &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ &3.&\quad A\to B &: \comp{Nb}\sb{Kb} \end{alignat*} If Charlie tries the same attack, Alice will receive the message $\comp{Na,Nb,B}\sb{Ka}$ when she was expecting to receive $\comp{Na,Nb,C}\sb{Ka}$. She will abandon the run, and eventually so will Bob. In ground-breaking work, Lowe~\cite{lowe-fdr} showed how such attacks could be found automatically using a model checker. An alternative, which we shall examine below, is to prove protocols correct. Proofs can be done under more realistic assumptions because our model does not have to be finite. The strategy is to formalize the operational semantics of the system and to prove security properties using rule induction. \section{Agents and Messages} All protocol specifications refer to a syntactic theory of messages. Datatype \isa{agent} introduces the constant \isa{Server} (a trusted central machine, needed for some protocols), an infinite population of ``friendly'' agents, and the~\isa{Spy}: \begin{isabelle} \isacommand{datatype}\ agent\ =\ Server\ |\ Friend\ nat\ |\ Spy \end{isabelle} % Keys are just natural numbers. Function \isa{invKey} maps a public key to the matching private key, and vice versa: \begin{isabelle} \isacommand{types}\ key\ =\ nat\isanewline \isacommand{consts}\ invKey\ ::\ "key=>key" \end{isabelle} Datatype \isa{msg} introduces the message forms, which include agent names, nonces, keys, compound messages, and encryptions. \begin{isabelle} \isacommand{datatype}\isanewline \ \ \ \ \ msg\ =\ Agent\ \ agent\ \ \ \ \ \isanewline \ \ \ \ \ \ \ \ \ |\ Nonce\ \ nat\ \ \ \ \ \ \ \isanewline \ \ \ \ \ \ \ \ \ |\ Key\ \ \ \ key\ \ \ \ \ \ \ \isanewline \ \ \ \ \ \ \ \ \ |\ MPair\ \ msg\ msg\ \ \ \isanewline \ \ \ \ \ \ \ \ \ |\ Crypt\ \ key\ msg\ \ \ \isanewline \end{isabelle} % The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ abbreviates $\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. Since datatype constructors are injective, we have the theorem \begin{isabelle} Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand X=X'. \end{isabelle} A ciphertext can be decrypted using only one key and can yield only one plaintext. This assumption is realistic if encryption includes some built-in redundancy. \section{Modelling the Adversary} The spy is part of the system and must be built into the model. He is a malicious user who does not have to follow the protocol. He watches the network and uses any keys he knows to decrypt messages, perhaps learning additional keys and nonces. He uses the items he has accumulated to compose new messages, which he may send to anybody. Two functions enable us to formalize this behaviour: \isa{analz} and \isa{synth}. Each function maps a sets of messages to another set of messages. The set \isa{analz H} formalizes what the adversary can learn from the set of messages~$H$. The closure properties of this set are defined inductively. \begin{isabelle} \isacommand{consts}\ \ analz\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline \isacommand{inductive}\ "analz\ H"\isanewline \ \ \isakeyword{intros}\ \isanewline \ \ \ \ Inj\ [intro,simp]\ :\ \ \ "X\ \isasymin \ H\ \isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline \ \ \ \ Fst:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\ \isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline \ \ \ \ Snd:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\ \isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline \ \ \ \ Decrypt\ [dest]:\ \isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ "[|Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\ K):\ analz\ H|]\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ X\ \isasymin \ analz\ H" \end{isabelle} % Note the \isa{Decrypt} rule: the spy can decrypt a message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. Properties proved by rule induction include the following: \begin{isabelle} G\isasymsubseteq H\ \isasymLongrightarrow\ analz(G)\ \isasymsubseteq\ analz(H) \rulename{analz_mono}\isanewline analz (analz H) = analz H \rulename{analz_idem} \end{isabelle} The set of fake messages that an intruder could invent starting from~\isa{H} is \isa{synth(analz~H)}, where \isa{synth H} formalizes what the adversary can build from the set of messages~$H$. \begin{isabelle} \isacommand{consts}\ \ synth\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline \isacommand{inductive}\ "synth\ H"\isanewline \ \ \isakeyword{intros}\ \isanewline \ \ \ \ Inj\ \ \ [intro]:\ "X\ \isasymin \ H\ \isasymLongrightarrow\ X\ \isasymin \ synth\ H"\isanewline \ \ \ \ Agent\ [intro]:\ "Agent\ agt\ \isasymin \ synth\ H"\isanewline \ \ \ \ MPair\ [intro]:\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Y\ \isasymin \ synth\ H|]\ \isasymLongrightarrow\ \isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ synth\ H"\isanewline \ \ \ \ Crypt\ [intro]:\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Key K\ \isasymin \ H|]\ \isasymLongrightarrow\ Crypt\ K\ X\ \isasymin \ synth\ H" \end{isabelle} The set includes all agent names. Nonces and keys are assumed to be unguessable, so none are included beyond those already in~$H$. Two elements of \isa{synth H} can be combined, and an element can be encrypted using a key present in~$H$. Like \isa{analz}, this set operator is monotone and idempotent. It also satisfies an interesting equation involving \isa{analz}: \begin{isabelle} analz (synth H)\ =\ analz H\ \isasymunion\ synth H \rulename{analz_synth} \end{isabelle} % Rule inversion plays a major role in reasoning about \isa{synth}, through declarations such as this one: \begin{isabelle} \isacommand{inductive\_cases}\ Nonce_synth\ [elim!]:\ "Nonce\ n\ \isasymin \ synth\ H" \end{isabelle} % The resulting elimination rule replaces every assumption of the form \isa{Nonce\ n\ \isasymin \ synth\ H} by \isa{Nonce\ n\ \isasymin \ H}, expressing that a nonce cannot be guessed. %The theory also uses rule inversion with constructors \isa{Key}, \isa{Crypt} %and \isa{MPair} (message pairing). % A third operator, \isa{parts}, is useful for stating correctness properties. The set \isa{parts H} consists of the components of elements of~$H$. This set includes~\isa{H} and is closed under the projections from a compound message to its immediate parts. Its definition resembles that of \isa{analz} except in the rule corresponding to the constructor \isa{Crypt}: \begin{isabelle} \ \ \ \ \ Crypt\ K\ X\ \isasymin \ parts\ H\ \isasymLongrightarrow\ X\ \isasymin \ parts\ H \end{isabelle} The body of an encrypted message is always regarded as part of it. We can use \isa{parts} to express general well-formedness properties of a protocol, for example, that an uncompromised agent's private key will never be included as a component of any message. \section{Event Traces}\label{sec:events} The system's behaviour is formalized as a set of traces of \emph{events}. The most important event, \isa{Says~A~B~X}, expresses the attempt by~$A$ to send~$B$ the message~$X$. A trace is simply a list, constructed in reverse using~\isa{\#}. Sometimes the protocol requires an agent to generate a new nonce. The probability that a 20-byte random number has appeared before is effectively zero. To formalize this important property, the set \isa{used evs} denotes the set of all items mentioned in the trace~\isa{evs}. The function \isa{used} has a straightforward recursive definition. Here is the case for \isa{Says} event: \begin{isabelle} \ \ \ \ \ used\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\ \isacharbraceleft X\isacharbraceright \ \isasymunion\ (used\ evs) \end{isabelle} The function \isa{knows} formalizes an agent's knowledge. Mostly we only case about the spy's knowledge, and \isa{knows Spy evs} is the set of items available to the spy in the trace~\isa{evs}. Already in the empty trace, the spy starts with some secrets at his disposal, such as the private keys of compromised users. After each \isa{Says} event, the spy learns the message that was sent. Combinations of functions express other important concepts involving~\isa{evs}: \begin{itemize} \item \isa{analz (knows Spy evs)} is the items that the spy could learn by decryption \item \isa{synth (analz (knows Spy evs))} is the items that the spy could generate \end{itemize} The function \isa{pubK} maps agents to their public keys. The function \isa{priK} maps agents to their private keys, is defined in terms of \isa{invKey} and \isa{pubK} by a translation. \begin{isabelle} \isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline \isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline \isacommand{translations}\ \ \ \ "priK\ x"\ \ ==\ "invKey(pubK\ x)" \end{isabelle} The set \isa{bad} consists of those agents whose private keys are known to the spy. Two axioms are asserted about the public-key cryptosystem. No two agents have the same public key, and no private key equals any public key. \begin{isabelle} \isacommand{axioms}\isanewline \ \ inj_pubK:\ \ \ \ \ \ \ \ "inj\ pubK"\isanewline \ \ priK_neq_pubK:\ \ \ "priK\ A\ \isasymnoteq\ pubK\ B" \end{isabelle} \section{Modelling the Protocol}\label{sec:modelling} Let us formalize the Needham-Schroeder public-key protocol, as corrected by Lowe: \begin{alignat*}{2} &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ &3.&\quad A\to B &: \comp{Nb}\sb{Kb} \end{alignat*} Each protocol step is specified by a rule of an inductive definition. An event trace has type \isa{event list}, so we declare the constant \isa{ns_public} to be a set of such traces. \begin{isabelle} \isacommand{consts}\ \ ns_public\ \ ::\ "event\ list\ set" \end{isabelle} \begin{figure} \begin{isabelle} \isacommand{inductive}\ ns_public\isanewline \ \ \isakeyword{intros}\ \isanewline \ \ \ \ \ \ \ \ \ \isanewline \ \ \ Nil:\ \ "[]\ \isasymin \ ns_public"\isanewline \isanewline \ \ \ \ \ \ \ \ \ \isanewline \ \ \ Fake:\ "\isasymlbrakk evsf\ \isasymin \ ns_public;\ \ X\ \isasymin \ synth\ (analz\ (spies\ evsf))\isasymrbrakk \isanewline \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ Spy\ B\ X\ \ \#\ evsf\ \isasymin \ ns_public"\isanewline \isanewline \ \ \ \ \ \ \ \ \ \isanewline \ \ \ NS1:\ \ "\isasymlbrakk evs1\ \isasymin \ ns_public;\ \ Nonce\ NA\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs1\ \ \isasymin \ \ ns_public"\isanewline \isanewline \ \ \ \ \ \ \ \ \ \isanewline \ \ \ NS2:\ \ "\isasymlbrakk evs2\ \isasymin \ ns_public;\ \ Nonce\ NB\ \isasymnotin \ used\ evs2;\isanewline \ \ \ \ \ \ \ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs2\isasymrbrakk \isanewline \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs2\ \ \isasymin \ \ ns_public"\isanewline \isanewline \ \ \ \ \ \ \ \ \ \isanewline \ \ \ NS3:\ \ "\isasymlbrakk evs3\ \isasymin \ ns_public;\isanewline \ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs3;\isanewline \ \ \ \ \ \ \ \ \ \ \ Says\ B'\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymin \ set\ evs3\isasymrbrakk \isanewline \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \#\ evs3\ \isasymin \ ns_public" \end{isabelle} \caption{An Inductive Protocol Definition}\label{fig:ns_public} \end{figure} Figure~\ref{fig:ns_public} presents the inductive definition. The \isa{Nil} rule introduces the empty trace. The \isa{Fake} rule models the adversary's sending a message built from components taken from past traffic, expressed using the functions \isa{synth} and \isa{analz}. The next three rules model how honest agents would perform the three protocol steps. Here is a detailed explanation of rule \isa{NS2}. A trace containing an event of the form \begin{isabelle} \ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace) \end{isabelle} % may be extended by an event of the form \begin{isabelle} \ \ \ \ \ Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace) \end{isabelle} where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ \isasymnotin \ used\ evs2}. Writing the sender as \isa{A'} indicates that \isa{B} does not know who sent the message. Calling the trace variable \isa{evs2} rather than simply \isa{evs} helps us know where we are in a proof after many case-splits: every subgoal mentioning \isa{evs2} involves message~2 of the protocol. Benefits of this approach are simplicity and clarity. The semantic model is set theory, proofs are by induction and the translation from the informal notation to the inductive rules is straightforward. \section{Proving Elementary Properties} Secrecy properties are hard to prove. The conclusion of a typical secrecy theorem is \isa{X\ \isasymnotin\ analz (knows Spy evs)}. The difficulty arises from having to reason about \isa{analz}, or less formally, showing that the spy can never learn~\isa{X}. Much easier is to prove that \isa{X} can never occur at all. Such \emph{regularity} properties are typically expressed using \isa{parts} rather than \isa{analz}. The following lemma states that \isa{A}'s private key is potentially known to the spy if and only if \isa{A} belongs to the set \isa{bad} of compromised agents. The statement uses \isa{parts}: the very presence of her private key in a message, whether protected by encryption or not, is enough to confirm that \isa{A} is compromised. The proof, like nearly all protocol proofs, is by induction over traces. \begin{isabelle} \isacommand{lemma}\ Spy_see_priK\ [simp]:\ \isanewline \ \ \ \ \ \ "evs\ \isasymin \ ns_public\isanewline \ \ \ \ \ \ \ \isasymLongrightarrow \ (Key\ (priK\ A)\ \isasymin \ parts\ (spies\ evs))\ =\ (A\ \isasymin \ bad)"\isanewline \isacommand{apply}\ (erule\ ns_public.induct,\ simp_all) \end{isabelle} % The induction yields five subgoals, one for each rule in the definition of \isa{ns_public}. Informally, the idea is to prove that the protocol property holds initially (rule \isa{Nil}), is preserved by each of the legitimate protocol steps (rules \isa{NS1}--\isa{3}), and even is preserved in the face of anything the spy can do (rule \isa{Fake}). Simplification leaves only the \isa{Fake} case (as indicated by the variable name \isa{evsf}): \begin{isabelle} \ 1.\ \isasymAnd X\ evsf.\isanewline \isaindent{\ 1.\ \ \ \ }\isasymlbrakk evsf\ \isasymin \ ns_public;\isanewline \isaindent{\ 1.\ \ \ \ \ \ \ }(Key\ (priK\ A)\ \isasymin \ parts\ (knows\ Spy\ evsf))\ =\ (A\ \isasymin \ bad);\isanewline \isaindent{\ 1.\ \ \ \ \ \ \ }X\ \isasymin \ synth\ (analz\ (knows\ Spy\ evsf))\isasymrbrakk \isanewline \isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ (Key\ (priK\ A)\ \isasymin \ parts\ (insert\ X\ (knows\ Spy\ evsf)))\ =\isanewline \isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }(A\ \isasymin \ bad)\isanewline \isacommand{by}\ blast \end{isabelle} % The \isa{Fake} case is proved automatically. If \isa{priK~A} is in the extended trace then either (1) it was already in the original trace or (2) it was generated by the spy, and so the spy must have known this key already. Either way, the induction hypothesis applies. If the spy can tell himself something, then he must have known it already. \emph{Unicity} lemmas are regularity lemmas stating that specified items can occur only once in a trace. The following lemma states that a nonce cannot be used both as $Na$ and as $Nb$ unless it is known to the spy. Intuitively, it holds because honest agents always choose fresh values as nonces; only the spy might reuse a value, and he doesn't know this particular value. The proof script is three steps long. \begin{isabelle} \isacommand{lemma}\ no_nonce_NS1_NS2\ [rule_format]:\ \isanewline \ "evs\ \isasymin \ ns_public\ \isanewline \ \ \isasymLongrightarrow \ Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\ NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (spies\ evs)\ \isasymlongrightarrow \isanewline \ \ \ \ \ \ Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace \ \isasymin \ parts\ (spies\ evs)\ \isasymlongrightarrow \ \ \isanewline \ \ \ \ \ \ Nonce\ NA\ \isasymin \ analz\ (spies\ evs)" \end{isabelle} This unicity lemma states that, if \isa{NA} is secret, then its appearance in any instance of message~1 determines the other components. The proof is another easy induction. \begin{isabelle} \isacommand{lemma}\ unique_NA:\ \isanewline \ \ \ \ \ "\isasymlbrakk Crypt(pubK\ B)\ \ \isasymlbrace Nonce\ NA,\ Agent\ A\ \isasymrbrace \ \isasymin \ parts(spies\ evs);\ \ \isanewline \ \ \ \ \ \ \ Crypt(pubK\ B')\ \isasymlbrace Nonce\ NA,\ Agent\ A'\isasymrbrace \ \isasymin \ parts(spies\ evs);\ \ \isanewline \ \ \ \ \ \ \ Nonce\ NA\ \isasymnotin \ analz\ (spies\ evs);\ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline \ \ \ \ \ \ \isasymLongrightarrow \ A=A'\ \isasymand \ B=B'" \end{isabelle} \section{Proving Secrecy Theorems}\label{sec:secrecy} The secrecy theorems for Bob (the second participant) are especially important, since they fail for the original protocol. This theorem states that if Bob sends message~2 to Alice, and both agents are uncompromised, then Bob's nonce will never reach the spy. \begin{isabelle} \isacommand{theorem}\ Spy_not_see_NB\ [dest]:\isanewline \ "\isasymlbrakk Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline \ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline \ \ \isasymLongrightarrow \ Nonce\ NB\ \isasymnotin \ analz\ (spies\ evs)" \end{isabelle} % To prove this, we must formulate the induction properly (one of the assumptions mentions~\isa{evs}), apply induction, and simplify. The proof states are too complicated to present in full. Let's just look at the easiest subgoal, that for message~1: \begin{isabelle} \ 1.\ \isasymAnd Ba\ NAa\ evs1.\isanewline \isaindent{\ 1.\ \ \ \ }\isasymlbrakk A\ \isasymnotin \ bad;\ B\ \isasymnotin \ bad;\ evs1\ \isasymin \ ns_public;\isanewline \isaindent{\ 1.\ \ \ \ \ \ \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline \isaindent{\ 1.\ \ \ \ \ \ \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline \isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NB\ \isasymnotin \ analz\ (knows\ Spy\ evs1);\isanewline \isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NAa\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline \isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Ba\ \isasymin \ bad\ \isasymlongrightarrow \isanewline \isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline \isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline \isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }NB\ \isasymnoteq \ NAa \end{isabelle} This subgoal refers to another protocol run, in which \isa{B} has sent message~1 to somebody called~\isa{Ba}. Agent \isa{Ba} is compromised, and so the spy has learnt the nonce that was just sent, which is called~\isa{NAa}. We need to know that this nonce differs from the one we care about, namely~\isa{NB}\@. They do indeed differ: \isa{NB} was sent earlier, while \isa{NAa} was chosen to be fresh (we have the assumption \isa{Nonce\ NAa\ \isasymnotin \ used\ evs1}). Note that our reasoning concerned \isa{B}'s participation in another run. Agents may engage in several runs concurrently, and some attacks work by interleaving the messages of two runs. With model checking, this possibility can cause a state-space explosion, and for us it certainly complicates proofs. The biggest subgoal concerns message~2. It splits into several cases, some of which are proved by unicity, others by the induction hypothesis. For all those complications, the proofs are automatic by \isa{blast} with the theorem \isa{no_nonce_NS1_NS2}. The remaining proofs are straightforward. This theorem asserts that if \isa{B} has sent an instance of message~2 to~\isa{A} and has received the expected reply, then that reply really came from~\isa{A}. The proof is a simple induction. \begin{isabelle} \isacommand{theorem}\ B_trusts_NS3:\isanewline \ "\isasymlbrakk Says\ B\ A\ \ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ evs;\ \isanewline \ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \ \ \ \ \ \ \ \ \isanewline \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ evs" \end{isabelle} From similar assumptions, we can prove that \isa{A} started the protocol run by sending an instance of message~1 involving the nonce~\isa{NA}. For this theorem, the conclusion is \begin{isabelle} \ \ \ \ \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs \end{isabelle} % Analogous theorems can be proved for~\isa{A}, stating that nonce~\isa{NA} remains secret and that message~2 really originates with~\isa{B}. Even the flawed protocol establishes these properties for~\isa{A}; the flaw only harms the second participant. Detailed information on this technique can be found elsewhere~\cite{paulson-jcs}, including proofs of an Internet protocol~\cite{paulson-tls}. \endinput \ No newline at end of file +% $Id$ +\chapter{Case Study: Verifying a Cryptographic Protocol} +\label{chap:crypto} + +%crypto primitives FIXME: GET RID OF MANY +\def\lbb{\mathopen{\{\kern-.30em|}} +\def\rbb{\mathclose{|\kern-.32em\}}} +\def\comp#1{\lbb#1\rbb} + +Communications security is an ancient art. Julius Caesar is said to have +encrypted his messages, shifting each letter three places along the +alphabet. Mary Queen of Scots was convicted of treason after a cipher used +in her letters was broken. Today's postal system incorporates security +features. The envelope provides a degree of +\emph{secrecy}. The signature provides \emph{authenticity} (proof of +origin), as do departmental stamps and letterheads. + +Networks are vulnerable: messages pass through many computers, any of which +might be controlled an adversary, who thus can capture or redirect +messages. People who wish to communicate securely over such a network can +use cryptography, but if they are to understand each other, they need to +follow a +\emph{protocol}: a pre-arranged sequence of message formats. + +Protocols can be attacked in many ways, even if encryption is unbreakable. +A \emph{splicing attack} involves an adversary's sending a message composed +of parts of several old messages. This fake message may have the correct +format, fooling an honest party. The adversary might be able to masquerade +as somebody else, or he might obtain a secret key. + +\emph{Nonces} help prevent splicing attacks. A typical nonce is a 20-byte +random number. Each message that requires a reply incorporates a nonce. The +reply must include a copy of that nonce, to prove that it is not a replay of +a past message. Nonces must be cryptographically protected, since +otherwise an adversary could easily generate fakes. You should be starting +to see that protocol design is tricky! + +Researchers are developing methods for proving the correctness of security +protocols. The Needham-Schroeder public-key +protocol~\cite{needham-schroeder} has become a standard test case. +Proposed in 1978, it was found to be defective nearly two decades +later~\cite{lowe-fdr}. This toy protocol will be useful in demonstrating +how to verify protocols using Isabelle. + + +\section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol} + +This protocol uses public-key cryptography. Each person has a private key, known only to +himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she +encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the +matching private key, which is needed in order to decrypt Alice's message. + +The core of the Needham-Schroeder protocol consists of three messages: +\begin{alignat*}{2} + &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ + &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ + &3.&\quad A\to B &: \comp{Nb}\sb{Kb} +\end{alignat*} +First, let's understand the notation. In the first message, Alice +sends Bob a message consisting of a nonce generated by Alice~($Na$) +paired with Alice's name~($A$) and encrypted using Bob's public +key~($Kb$). In the second message, Bob sends Alice a message +consisting of $Na$ paired with a nonce generated by Bob~($Nb$), +encrypted using Alice's public key~($Ka$). In the last message, Alice +returns $Nb$ to Bob, encrypted using his public key. + +When Alice receives Message~2, she knows that Bob has acted on her +message, since only he could have decrypted +$\comp{Na,A}\sb{Kb}$ and extracted~$Na$. That is precisely what +nonces are for. Similarly, message~3 assures Bob that Alice is +active. But the protocol was widely believed~\cite{ban89} to satisfy a +further property: that +$Na$ and~$Nb$ were secrets shared by Alice and Bob. (Many +protocols generate such shared secrets, which can be used +to lessen the reliance on slow public-key operations.) Lowe found this +claim to be false: if Alice runs the protocol with someone untrustworthy +(Charlie say), then he can start a new run with another agent (Bob say). +Charlie uses Alice as an oracle, masquerading as +Alice to Bob~\cite{lowe-fdr}. +\begin{alignat*}{4} + &1.&\quad A\to C &: \comp{Na,A}\sb{Kc} & + \qquad 1'.&\quad C\to B &: \comp{Na,A}\sb{Kb} \\ + &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ + &3.&\quad A\to C &: \comp{Nb}\sb{Kc} & + 3'.&\quad A\to B &: \comp{Nb}\sb{Kb} +\end{alignat*} +In messages~1 and~3, Charlie removes the encryption using his private +key and re-encrypts Alice's messages using Bob's public key. Bob is +left thinking he has run the protocol with Alice, which was not +Alice's intention, and Bob is unaware that the ``secret'' nonces are +known to Charlie. This is a typical man-in-the-middle attack launched +by an insider. + +Lowe also suggested a fix, namely to include Bob's name in message~2: +\begin{alignat*}{2} + &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ + &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ + &3.&\quad A\to B &: \comp{Nb}\sb{Kb} +\end{alignat*} +If Charlie tries the same attack, Alice will receive the message +$\comp{Na,Nb,B}\sb{Ka}$ when she was expecting to receive +$\comp{Na,Nb,C}\sb{Ka}$. She will abandon the run, and eventually so +will Bob. + +In ground-breaking work, Lowe~\cite{lowe-fdr} showed how such attacks +could be found automatically using a model checker. An alternative, +which we shall examine below, is to prove protocols correct. Proofs +can be done under more realistic assumptions because our model does +not have to be finite. The strategy is to formalize the operational +semantics of the system and to prove security properties using rule +induction. + + +\section{Agents and Messages} + +All protocol specifications refer to a syntactic theory of messages. +Datatype +\isa{agent} introduces the constant \isa{Server} (a trusted central +machine, needed for some protocols), an infinite population of ``friendly'' +agents, and the~\isa{Spy}: +\begin{isabelle} +\isacommand{datatype}\ agent\ =\ Server\ |\ Friend\ nat\ |\ Spy +\end{isabelle} +% +Keys are just natural numbers. Function \isa{invKey} maps a public key to +the matching private key, and vice versa: +\begin{isabelle} +\isacommand{types}\ key\ =\ nat\isanewline +\isacommand{consts}\ invKey\ ::\ "key=>key" +\end{isabelle} +Datatype +\isa{msg} introduces the message forms, which include agent names, nonces, +keys, compound messages, and encryptions. +\begin{isabelle} +\isacommand{datatype}\isanewline +\ \ \ \ \ msg\ =\ Agent\ \ agent\ \ \ \ \ \isanewline +\ \ \ \ \ \ \ \ \ |\ Nonce\ \ nat\ \ \ \ \ \ \ \isanewline +\ \ \ \ \ \ \ \ \ |\ Key\ \ \ \ key\ \ \ \ \ \ \ \isanewline +\ \ \ \ \ \ \ \ \ |\ MPair\ \ msg\ msg\ \ \ \isanewline +\ \ \ \ \ \ \ \ \ |\ Crypt\ \ key\ msg\ \ \ \isanewline +\end{isabelle} +% +The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ +abbreviates +$\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. + +Since datatype constructors are injective, we have the theorem +\begin{isabelle} +Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand X=X'. +\end{isabelle} +A ciphertext can be decrypted using only one key and +can yield only one plaintext. This assumption is realistic if encryption +includes some built-in redundancy. + + +\section{Modelling the Adversary} + +The spy is part of the system and must be built into the model. He is +a malicious user who does not have to follow the protocol. He +watches the network and uses any keys he knows to decrypt messages, +perhaps learning additional keys and nonces. He uses the items he has +accumulated to compose new messages, which he may send to anybody. + +Two functions enable us to formalize this behaviour: \isa{analz} and +\isa{synth}. Each function maps a sets of messages to another set of +messages. The set \isa{analz H} formalizes what the adversary can learn +from the set of messages~$H$. The closure properties of this set are +defined inductively. +\begin{isabelle} +\isacommand{consts}\ \ analz\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline +\isacommand{inductive}\ "analz\ H"\isanewline +\ \ \isakeyword{intros}\ \isanewline +\ \ \ \ Inj\ [intro,simp]\ :\ \ \ "X\ \isasymin \ H\ +\isasymLongrightarrow\ X\ +\isasymin +\ analz\ H"\isanewline +\ \ \ \ Fst:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\ +\isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline +\ \ \ \ Snd:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\ +\isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline +\ \ \ \ Decrypt\ [dest]:\ \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ "[|Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\ +K):\ analz\ H|]\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ X\ \isasymin \ analz\ H" +\end{isabelle} +% +Note the \isa{Decrypt} rule: the spy can decrypt a +message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. +Properties proved by rule induction include the following: +\begin{isabelle} +G\isasymsubseteq H\ \isasymLongrightarrow\ analz(G)\ \isasymsubseteq\ +analz(H) +\rulename{analz_mono}\isanewline +analz (analz H) = analz H +\rulename{analz_idem} +\end{isabelle} + +The set of fake messages that an intruder could invent +starting from~\isa{H} is \isa{synth(analz~H)}, where \isa{synth H} +formalizes what the adversary can build from the set of messages~$H$. +\begin{isabelle} +\isacommand{consts}\ \ synth\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline +\isacommand{inductive}\ "synth\ H"\isanewline +\ \ \isakeyword{intros}\ \isanewline +\ \ \ \ Inj\ \ \ [intro]:\ "X\ \isasymin \ H\ \isasymLongrightarrow\ +X\ \isasymin \ synth\ H"\isanewline +\ \ \ \ Agent\ [intro]:\ "Agent\ agt\ \isasymin \ synth\ H"\isanewline +\ \ \ \ MPair\ [intro]:\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Y\ \isasymin +\ synth\ H|]\ \isasymLongrightarrow\ +\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ synth\ H"\isanewline +\ \ \ \ Crypt\ [intro]:\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Key K\ +\isasymin \ H|]\ \isasymLongrightarrow\ Crypt\ K\ X\ +\isasymin \ synth\ H" +\end{isabelle} +The set includes all agent names. Nonces and keys are assumed to be +unguessable, so none are included beyond those already in~$H$. Two +elements of \isa{synth H} can be combined, and an element can be encrypted +using a key present in~$H$. + +Like \isa{analz}, this set operator is monotone and idempotent. It also +satisfies an interesting equation involving \isa{analz}: +\begin{isabelle} +analz (synth H)\ =\ analz H\ \isasymunion\ synth H +\rulename{analz_synth} +\end{isabelle} +% +Rule inversion plays a major role in reasoning about \isa{synth}, through +declarations such as this one: +\begin{isabelle} +\isacommand{inductive\_cases}\ Nonce_synth\ [elim!]:\ "Nonce\ n\ \isasymin +\ synth\ H" +\end{isabelle} +% +The resulting elimination rule replaces every assumption of the form +\isa{Nonce\ n\ \isasymin \ synth\ H} by \isa{Nonce\ n\ +\isasymin \ H}, expressing that a nonce cannot be guessed. +%The theory also uses rule inversion with constructors \isa{Key}, \isa{Crypt} +%and \isa{MPair} (message pairing). + +% +A third operator, \isa{parts}, is useful for stating correctness +properties. The set +\isa{parts H} consists of the components of elements of~$H$. This set +includes~\isa{H} and is closed under the projections from a compound +message to its immediate parts. +Its definition resembles that of \isa{analz} except in the rule +corresponding to the constructor \isa{Crypt}: +\begin{isabelle} +\ \ \ \ \ Crypt\ K\ X\ \isasymin \ parts\ H\ \isasymLongrightarrow\ X\ +\isasymin \ parts\ H +\end{isabelle} +The body of an encrypted message is always regarded as part of it. We can +use \isa{parts} to express general well-formedness properties of a protocol, +for example, that an uncompromised agent's private key will never be +included as a component of any message. + + +\section{Event Traces}\label{sec:events} + +The system's behaviour is formalized as a set of traces of +\emph{events}. The most important event, \isa{Says~A~B~X}, expresses the +attempt by~$A$ to send~$B$ the + message~$X$. A trace is simply a list, constructed in reverse +using~\isa{\#}. + +Sometimes the protocol requires an agent to generate a new nonce. The +probability that a 20-byte random number has appeared before is effectively +zero. To formalize this important property, the set \isa{used evs} +denotes the set of all items mentioned in the trace~\isa{evs}. +The function \isa{used} has a straightforward +recursive definition. Here is the case for \isa{Says} event: +\begin{isabelle} +\ \ \ \ \ used\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\ \isacharbraceleft +X\isacharbraceright \ \isasymunion\ (used\ evs) +\end{isabelle} + +The function \isa{knows} formalizes an agent's knowledge. Mostly we only +case about the spy's knowledge, and \isa{knows Spy evs} is the set of items +available to the spy in the trace~\isa{evs}. Already in the empty trace, +the spy starts with some secrets at his disposal, such as the private keys +of compromised users. After each \isa{Says} event, the spy learns the +message that was sent. Combinations of functions express other important +concepts involving~\isa{evs}: +\begin{itemize} +\item \isa{analz (knows Spy evs)} is the items that the spy could +learn by decryption +\item \isa{synth (analz (knows Spy evs))} is the items that the spy +could generate +\end{itemize} + +The function +\isa{pubK} maps agents to their public keys. The function +\isa{priK} maps agents to their private keys, is defined in terms of +\isa{invKey} and \isa{pubK} by a translation. +\begin{isabelle} +\isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline +\isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline +\isacommand{translations}\ \ \ \ "priK\ x"\ \ ==\ "invKey(pubK\ x)" +\end{isabelle} +The set \isa{bad} consists of those agents whose private keys are known to +the spy. + +Two axioms are asserted about the public-key cryptosystem. +No two agents have the same public key, and no private key equals +any public key. +\begin{isabelle} +\isacommand{axioms}\isanewline +\ \ inj_pubK:\ \ \ \ \ \ \ \ "inj\ pubK"\isanewline +\ \ priK_neq_pubK:\ \ \ "priK\ A\ \isasymnoteq\ pubK\ B" +\end{isabelle} + + + + + +\section{Modelling the Protocol}\label{sec:modelling} + +Let us formalize the Needham-Schroeder public-key protocol, as corrected by +Lowe: +\begin{alignat*}{2} + &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ + &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ + &3.&\quad A\to B &: \comp{Nb}\sb{Kb} +\end{alignat*} + +Each protocol step is specified by a rule of an inductive definition. An +event trace has type \isa{event list}, so we declare the constant +\isa{ns_public} to be a set of such traces. +\begin{isabelle} +\isacommand{consts}\ \ ns_public\ \ ::\ "event\ list\ set" +\end{isabelle} + +\begin{figure} +\begin{isabelle} +\isacommand{inductive}\ ns_public\isanewline +\ \ \isakeyword{intros}\ \isanewline +\ \ \ \ \ \ \ \ \ \isanewline +\ \ \ Nil:\ \ "[]\ \isasymin \ ns_public"\isanewline +\isanewline +\ \ \ \ \ \ \ \ \ \isanewline +\ \ \ Fake:\ "\isasymlbrakk evsf\ \isasymin \ ns_public;\ \ X\ \isasymin \ synth\ (analz\ (spies\ evsf))\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ Spy\ B\ X\ \ \#\ evsf\ \isasymin \ ns_public"\isanewline +\isanewline +\ \ \ \ \ \ \ \ \ \isanewline +\ \ \ NS1:\ \ "\isasymlbrakk evs1\ \isasymin \ ns_public;\ \ Nonce\ NA\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs1\ \ \isasymin \ \ ns_public"\isanewline +\isanewline +\ \ \ \ \ \ \ \ \ \isanewline +\ \ \ NS2:\ \ "\isasymlbrakk evs2\ \isasymin \ ns_public;\ \ Nonce\ NB\ \isasymnotin \ used\ evs2;\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs2\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs2\ \ \isasymin \ \ ns_public"\isanewline +\isanewline +\ \ \ \ \ \ \ \ \ \isanewline +\ \ \ NS3:\ \ "\isasymlbrakk evs3\ \isasymin \ ns_public;\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs3;\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ B'\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymin \ set\ evs3\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \#\ evs3\ \isasymin \ +ns_public" +\end{isabelle} +\caption{An Inductive Protocol Definition}\label{fig:ns_public} +\end{figure} + +Figure~\ref{fig:ns_public} presents the inductive definition. The +\isa{Nil} rule introduces the empty trace. The \isa{Fake} rule models the +adversary's sending a message built from components taken from past +traffic, expressed using the functions \isa{synth} and +\isa{analz}. +The next three rules model how honest agents would perform the three +protocol steps. + +Here is a detailed explanation of rule \isa{NS2}. +A trace containing an event of the form +\begin{isabelle} +\ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ +NA,\ Agent\ A\isasymrbrace) +\end{isabelle} +% +may be extended by an event of the form +\begin{isabelle} +\ \ \ \ \ Says\ B\ A\ (Crypt\ (pubK\ A)\ +\isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace) +\end{isabelle} +where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ \isasymnotin \ used\ evs2}. +Writing the sender as \isa{A'} indicates that \isa{B} does not +know who sent the message. Calling the trace variable \isa{evs2} rather +than simply \isa{evs} helps us know where we are in a proof after many +case-splits: every subgoal mentioning \isa{evs2} involves message~2 of the +protocol. + +Benefits of this approach are simplicity and clarity. The semantic model +is set theory, proofs are by induction and the translation from the informal +notation to the inductive rules is straightforward. + + +\section{Proving Elementary Properties} + +Secrecy properties are hard to prove. The conclusion of a typical secrecy +theorem is +\isa{X\ \isasymnotin\ analz (knows Spy evs)}. The difficulty arises from +having to reason about \isa{analz}, or less formally, showing that the spy +can never learn~\isa{X}. Much easier is to prove that \isa{X} can never +occur at all. Such \emph{regularity} properties are typically expressed +using \isa{parts} rather than \isa{analz}. + +The following lemma states that \isa{A}'s private key is potentially +known to the spy if and only if \isa{A} belongs to the set \isa{bad} of +compromised agents. The statement uses \isa{parts}: the very presence of +her private key in a message, whether protected by encryption or not, is +enough to confirm that \isa{A} is compromised. The proof, like nearly all +protocol proofs, is by induction over traces. +\begin{isabelle} +\isacommand{lemma}\ Spy_see_priK\ [simp]:\ \isanewline +\ \ \ \ \ \ "evs\ \isasymin \ ns_public\isanewline +\ \ \ \ \ \ \ \isasymLongrightarrow \ +(Key\ (priK\ A)\ \isasymin \ parts\ (spies\ evs))\ =\ (A\ \isasymin \ +bad)"\isanewline +\isacommand{apply}\ (erule\ ns_public.induct,\ simp_all) +\end{isabelle} +% +The induction yields five subgoals, one for each rule in the definition of +\isa{ns_public}. Informally, the idea is to prove that the protocol +property holds initially (rule \isa{Nil}), is preserved by each of the +legitimate protocol steps (rules \isa{NS1}--\isa{3}), and even is preserved +in the face of anything the spy can do (rule \isa{Fake}). Simplification +leaves only the \isa{Fake} case (as indicated by the variable name +\isa{evsf}): +\begin{isabelle} +\ 1.\ \isasymAnd X\ evsf.\isanewline +\isaindent{\ 1.\ \ \ \ }\isasymlbrakk evsf\ \isasymin \ ns_public;\isanewline +\isaindent{\ 1.\ \ \ \ \ \ \ }(Key\ (priK\ A)\ \isasymin \ parts\ (knows\ Spy\ evsf))\ =\ (A\ \isasymin \ bad);\isanewline +\isaindent{\ 1.\ \ \ \ \ \ \ }X\ \isasymin \ synth\ (analz\ (knows\ Spy\ evsf))\isasymrbrakk \isanewline +\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ (Key\ (priK\ A)\ \isasymin \ parts\ (insert\ X\ (knows\ Spy\ evsf)))\ =\isanewline +\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }(A\ \isasymin \ +bad)\isanewline +\isacommand{by}\ blast +\end{isabelle} +% +The \isa{Fake} case is proved automatically. If +\isa{priK~A} is in the extended trace then either (1) it was already in the +original trace or (2) it was +generated by the spy, and so the spy must have known this key already. +Either way, the induction hypothesis applies. If the spy can tell himself +something, then he must have known it already. + +\emph{Unicity} lemmas are regularity lemmas stating that specified items +can occur only once in a trace. The following lemma states that a nonce +cannot be used both as $Na$ and as $Nb$ unless +it is known to the spy. Intuitively, it holds because honest agents +always choose fresh values as nonces; only the spy might reuse a value, +and he doesn't know this particular value. The proof script is three steps +long. +\begin{isabelle} +\isacommand{lemma}\ no_nonce_NS1_NS2\ [rule_format]:\ \isanewline +\ "evs\ \isasymin \ ns_public\ \isanewline +\ \ \isasymLongrightarrow \ Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\ NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (spies\ evs)\ \isasymlongrightarrow \isanewline +\ \ \ \ \ \ Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace \ \isasymin \ parts\ (spies\ evs)\ \isasymlongrightarrow \ \ \isanewline +\ \ \ \ \ \ Nonce\ NA\ \isasymin \ analz\ (spies\ evs)" +\end{isabelle} + +This unicity lemma states that, if \isa{NA} is secret, then its appearance +in any instance of message~1 determines the other components. The proof is +another easy induction. +\begin{isabelle} +\isacommand{lemma}\ unique_NA:\ \isanewline +\ \ \ \ \ "\isasymlbrakk Crypt(pubK\ B)\ \ \isasymlbrace Nonce\ NA,\ Agent\ A\ \isasymrbrace \ \isasymin \ parts(spies\ evs);\ \ \isanewline +\ \ \ \ \ \ \ Crypt(pubK\ B')\ \isasymlbrace Nonce\ NA,\ Agent\ A'\isasymrbrace \ \isasymin \ parts(spies\ evs);\ \ \isanewline +\ \ \ \ \ \ \ Nonce\ NA\ \isasymnotin \ analz\ (spies\ evs);\ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline +\ \ \ \ \ \ \isasymLongrightarrow \ A=A'\ \isasymand \ B=B'" +\end{isabelle} + + +\section{Proving Secrecy Theorems}\label{sec:secrecy} + +The secrecy theorems for Bob (the second participant) are especially +important, since they fail for the original protocol. This theorem states +that if Bob sends message~2 to Alice, and both agents are uncompromised, +then Bob's nonce will never reach the spy. +\begin{isabelle} +\isacommand{theorem}\ Spy_not_see_NB\ [dest]:\isanewline +\ "\isasymlbrakk Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline +\ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline +\ \ \isasymLongrightarrow \ Nonce\ NB\ \isasymnotin \ analz\ (spies\ evs)" +\end{isabelle} +% +To prove this, we must formulate the induction properly (one of the +assumptions mentions~\isa{evs}), apply induction, and simplify. +The proof states are too complicated to present in full. +Let's just look +at the easiest subgoal, that for message~1: +\begin{isabelle} +\ 1.\ \isasymAnd Ba\ NAa\ evs1.\isanewline +\isaindent{\ 1.\ \ \ \ }\isasymlbrakk A\ \isasymnotin \ bad;\ B\ \isasymnotin \ bad;\ evs1\ \isasymin \ ns_public;\isanewline +\isaindent{\ 1.\ \ \ \ \ \ \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline +\isaindent{\ 1.\ \ \ \ \ \ \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline +\isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NB\ \isasymnotin \ analz\ (knows\ Spy\ evs1);\isanewline +\isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NAa\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline +\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Ba\ \isasymin \ bad\ \isasymlongrightarrow \isanewline +\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline +\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline +\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }NB\ \isasymnoteq \ NAa +\end{isabelle} +This subgoal refers to another protocol run, in which \isa{B} has sent +message~1 to somebody called~\isa{Ba}. Agent \isa{Ba} +is compromised, and so the spy has learnt the nonce that was just sent, +which is called~\isa{NAa}. We need to know that this nonce differs from the +one we care about, namely~\isa{NB}\@. They do indeed differ: \isa{NB} was +sent earlier, while \isa{NAa} was chosen to be fresh (we have the assumption +\isa{Nonce\ NAa\ \isasymnotin \ used\ evs1}). + +Note that our reasoning concerned \isa{B}'s participation in another +run. Agents may engage in several runs concurrently, and some attacks work +by interleaving the messages of two runs. With model checking, this +possibility can cause a state-space explosion, and for us it +certainly complicates proofs. The biggest subgoal concerns message~2. It +splits into several cases, some of which are proved by unicity, others by +the induction hypothesis. For all those complications, the proofs are +automatic by \isa{blast} with the theorem \isa{no_nonce_NS1_NS2}. + +The remaining proofs are straightforward. This theorem asserts that if +\isa{B} has sent an instance of message~2 to~\isa{A} and has received the +expected reply, then that reply really came from~\isa{A}. The proof is a +simple induction. +\begin{isabelle} +\isacommand{theorem}\ B_trusts_NS3:\isanewline +\ "\isasymlbrakk Says\ B\ A\ \ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline +\ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ evs;\ \isanewline +\ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \ \ \ \ \ \ \ \ \isanewline +\ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ +evs" +\end{isabelle} + +From similar assumptions, we can prove that \isa{A} started the protocol +run by sending an instance of message~1 involving the nonce~\isa{NA}. For +this theorem, the conclusion is +\begin{isabelle} +\ \ \ \ \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ +A\isasymrbrace )\ \isasymin \ set\ evs +\end{isabelle} +% +Analogous theorems can be proved for~\isa{A}, stating that nonce~\isa{NA} +remains secret and that message~2 really originates with~\isa{B}. Even the +flawed protocol establishes these properties for~\isa{A}; +the flaw only harms the second participant. +Detailed information on this technique can be found +elsewhere~\cite{paulson-jcs}, including proofs of an Internet +protocol~\cite{paulson-tls}. + + +\endinput