% $Id$\chapter{Case Study: Verifying a Security Protocol}\label{chap:crypto}\index{protocols!security|(}%crypto primitives \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 haveencrypted his messages, shifting each letter three places along thealphabet. Mary Queen of Scots was convicted of treason after a cipher usedin her letters was broken. Today's postal systemincorporates security features. The envelope provides a degree of\emph{secrecy}. The signature provides \emph{authenticity} (proof oforigin), as do departmental stamps and letterheads.Networks are vulnerable: messages pass through many computers, any of whichmight be controlled by an adversary, who thus can capture or redirectmessages. People who wish to communicate securely over such a network canuse cryptography, but if they are to understand each other, they need tofollow 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 composedof parts of several old messages. This fake message may have the correctformat, fooling an honest party. The adversary might be able to masqueradeas somebody else, or he might obtain a secret key.\emph{Nonces} help prevent splicing attacks. A typical nonce is a 20-byterandom number. Each message that requires a reply incorporates a nonce. Thereply must include a copy of that nonce, to prove that it is not a replay ofa past message. The nonce in the reply must be cryptographicallyprotected, since otherwise an adversary could easily replace it by adifferent one. You should be starting to see that protocol design istricky!Researchers are developing methods for proving the correctness of securityprotocols. The Needham-Schroeder public-keyprotocol~\cite{needham-schroeder} has become a standard test case. Proposed in 1978, it was found to be defective nearly two decadeslater~\cite{lowe-fdr}. This toy protocol will be useful in demonstratinghow to verify protocols using Isabelle.\section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol}\index{Needham-Schroeder protocol|(}%This protocol uses public-key cryptography. Each person has a private key, known only tohimself, and a public key, known to everybody. If Alice wants to send Bob a secret message, sheencrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has thematching 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, Alicesends Bob a message consisting of a nonce generated by Alice~($Na$)paired with Alice's name~($A$) and encrypted using Bob's publickey~($Kb$). In the second message, Bob sends Alice a messageconsisting of $Na$ paired with a nonce generated by Bob~($Nb$), encrypted using Alice's public key~($Ka$). In the last message, Alicereturns $Nb$ to Bob, encrypted using his public key.When Alice receives Message~2, she knows that Bob has acted on hermessage, since only he could have decrypted$\comp{Na,A}\sb{Kb}$ and extracted~$Na$. That is precisely whatnonces are for. Similarly, message~3 assures Bob that Alice isactive. But the protocol was widely believed~\cite{ban89} to satisfy afurther property: that$Na$ and~$Nb$ were secrets shared by Alice and Bob. (Manyprotocols generate such shared secrets, which can be usedto lessen the reliance on slow public-key operations.) Lowe\index{Lowe, Gavin|(} found thisclaim 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 asAlice 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} && \qquad 3'.&\quad C\to B &: \comp{Nb}\sb{Kb}\end{alignat*}In messages~1 and~3, Charlie removes the encryption using his privatekey and re-encrypts Alice's messages using Bob's public key. Bob isleft thinking he has run the protocol with Alice, which was notAlice's intention, and Bob is unaware that the ``secret'' nonces areknown to Charlie. This is a typical man-in-the-middle attack launchedby an insider.Whether this counts as an attack has been disputed. In protocols of thistype, we normally assume that the other party is honest. To be honestmeans to obey the protocol rules, so Alice's running the protocol withCharlie does not make her dishonest, just careless. After Lowe'sattack, Alice has no grounds for complaint: this protocol does not have toguarantee anything if you run it with a bad person. Bob does havegrounds for complaint, however: the protocol tells him that he iscommunicating with Alice (who is honest) but it does not guaranteesecrecy of the nonces.Lowe also suggested a correction, namely to include Bob's name inmessage~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 sowill Bob. Below, we shall look at parts of this protocol's correctnessproof. In ground-breaking work, Lowe~\cite{lowe-fdr}\index{Lowe, Gavin|)}showed how such attackscould be found automatically using a model checker. An alternative,which we shall examine below, is to prove protocols correct. Proofscan be done under more realistic assumptions because our model doesnot have to be finite. The strategy is to formalize the operationalsemantics of the system and to prove security properties using ruleinduction.%\index{Needham-Schroeder protocol|)}\section{Agents and Messages}All protocol specifications refer to a syntactic theory of messages. Datatype\isa{agent} introduces the constant \isa{Server} (a trusted centralmachine, needed for some protocols), an infinite population offriendly 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 tothe 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 andcan yield only one plaintext. In the real world, decryption with thewrong key succeeds but yields garbage. Our model of encryption isrealistic if encryption adds some redundancy to the plaintext, such as achecksum, so that garbage can be detected.\section{Modelling the Adversary}The spy is part of the system and must be built into the model. He isa malicious user who does not have to follow the protocol. Hewatches the network and uses any keys he knows to decrypt messages.Thus he accumulates additional keys and nonces. These he can use tocompose 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 ofmessages. The set \isa{analz H} formalizes what the adversary can learnfrom the set of messages~$H$. The closure properties of this set aredefined 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:\ \ \ \ \ "{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \analz\ H\\isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline\ \ \ \ Snd:\ \ \ \ \ "{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ analz\ H\\isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline\ \ \ \ Decrypt\ [dest]:\ \isanewline\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\K):\ analz\ H\isasymrbrakk\isanewline\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ X\ \isasymin \ analz\ H"\end{isabelle}%Note the \isa{Decrypt} rule: the spy can decrypt amessage 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}\isanewlineanalz (analz H) = analz H\rulename{analz_idem} \end{isabelle}The set of fake messages that an intruder could inventstarting 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\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}X\ \isasymin \ synth\ H;\ \ Y\ \isasymin\ synth\ H\isasymrbrakk\ \isasymLongrightarrow\{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ synth\ H"\isanewline\ \ \ \ Crypt\ [intro]:\isanewline\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}X\ \isasymin \ synth\ H;\ \ Key K\\isasymin \ H\isasymrbrakk\ \isasymLongrightarrow\ Crypt\ K\ X\\isasymin \ synth\ H"\end{isabelle}The set includes all agent names. Nonces and keys are assumed to beunguessable, so none are included beyond those already in~$H$. Twoelements of \isa{synth H} can be combined, and an element can be encryptedusing a key present in~$H$.Like \isa{analz}, this set operator is monotone and idempotent. It alsosatisfies 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}, throughdeclarations 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 correctnessproperties. The set\isa{parts H} consists of the components of elements of~$H$. This setincludes~\isa{H} and is closed under the projections from a compoundmessage to its immediate parts. Its definition resembles that of \isa{analz} except in the rulecorresponding 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 canuse \isa{parts} to express general well-formedness properties of a protocol,for example, that an uncompromised agent's private key will never beincluded 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$A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$.A trace is simply a list, constructed in reverseusing~\isa{\#}. Other event types include reception of messages (whenwe want to make it explicit) and an agent's storing a fact.Sometimes the protocol requires an agent to generate a new nonce. Theprobability that a 20-byte random number has appeared before is effectivelyzero. 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 straightforwardrecursive definition. Here is the case for \isa{Says} event:\begin{isabelle}\ \ \ \ \ used\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\ \isacharbraceleftX\isacharbraceright \ \isasymunion\ (used\ evs)\end{isabelle}The function \isa{knows} formalizes an agent's knowledge. Mostly we onlycare about the spy's knowledge, and \isa{knows Spy evs} is the set of itemsavailable 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 keysof compromised users. After each \isa{Says} event, the spy learns themessage that was sent:\begin{isabelle}\ \ \ \ \ knows\ Spy\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\\isacharbraceleft X\isacharbraceright \ \isasymunion\ (knows\ Spy\ evs)\end{isabelle}%Combinations of functions express other importantsets of messages derived from~\isa{evs}:\begin{itemize}\item \isa{analz (knows Spy evs)} is everything that the spy couldlearn by decryption\item \isa{synth (analz (knows Spy evs))} is everything that the spycould generate\end{itemize}The function\isa{pubK} maps agents to their public keys. The function\isa{priK} maps agents to their private keys. It is defined in terms of\isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} isnot a proper constant, so we declare it using \isacommand{syntax}\begin{isabelle}\isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline\isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline\isacommand{translations}\ \ \ \ "priK\ x"\ \ \isasymrightleftharpoons\ \ "invKey(pubK\ x)"\end{isabelle}The set \isa{bad} consists of those agents whose private keys are known tothe spy.Two axioms are asserted about the public-key cryptosystem. No two agents have the same public key, and no private key equalsany 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 byLowe:\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. Anevent 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\ (knows\ Spy\ 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 theadversary's sending a message built from components taken from pasttraffic, expressed using the functions \isa{synth} and\isa{analz}. The next three rules model how honest agents would perform the threeprotocol 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} ratherthan simply \isa{evs} helps us know where we are in a proof after manycase-splits: every subgoal mentioning \isa{evs2} involves message~2 of theprotocol.Benefits of this approach are simplicity and clarity. The semantic modelis set theory, proofs are by induction and the translation from the informalnotation to the inductive rules is straightforward. \section{Proving Elementary Properties}\label{sec:regularity}Secrecy properties can be hard to prove. The conclusion of a typicalsecrecy theorem is \isa{X\ \isasymnotin\ analz (knows Spy evs)}. The difficulty arises fromhaving to reason about \isa{analz}, or less formally, showing that the spycan never learn~\isa{X}. Much easier is to prove that \isa{X} can neveroccur at all. Such \emph{regularity} properties are typically expressedusing \isa{parts} rather than \isa{analz}.The following lemma states that \isa{A}'s private key is potentiallyknown to the spy if and only if \isa{A} belongs to the set \isa{bad} ofcompromised agents. The statement uses \isa{parts}: the very presence of\isa{A}'s private key in a message, whether protected by encryption ornot, is enough to confirm that \isa{A} is compromised. The proof, likenearly 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\ (knows\ Spy\ 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}. The idea is to prove thatthe 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 thespy can do (rule\isa{Fake}). The proof is trivial. No legitimate protocol rule sends any keysat all, so only \isa{Fake} is relevant. Indeed,simplification leaves only the \isa{Fake} case, as indicated by thevariable 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 theoriginal trace or (2) it wasgenerated by the spy, who must have known this key already. Either way, the induction hypothesis applies.\emph{Unicity} lemmas are regularity lemmas stating that specified itemscan occur only once in a trace. The following lemma states that a noncecannot be used both as $Na$ and as $Nb$ unlessit is known to the spy. Intuitively, it holds because honest agentsalways choose fresh values as nonces; only the spy might reuse a value,and he doesn't know this particular value. The proof script is short:induction, simplification, \isa{blast}.\begin{isabelle}\isacommand{lemma}\ no_nonce_NS1_NS2:\isanewline\ \ \ \ "\isasymlbrakk Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (knows\ Spy\evs);\isanewline\ \ \ \ \ \ Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\A\isasymrbrace \ \isasymin \ parts\ (knows\ Spy\ evs);\isanewline\ \ \ \ \ \ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline\ \ \ \ \ \isasymLongrightarrow \ Nonce\ NA\ \isasymin \ analz\ (knows\Spy\ evs)"\isanewline\isacommand{apply}\ (erule\ rev_mp,\ erule\ rev_mp)\isanewline\isacommand{apply}\ (erule\ ns_public.induct,\ simp_all)\isanewline\isacommand{apply}\ (blast\ intro:\ analz_insertI)+\isanewline\isacommand{done}\end{isabelle}The following unicity lemma states that, if \isa{NA} is secret, then itsappearance in any instance of message~1 determines the other components. The proof is similar to the previous one.\begin{isabelle}\isacommand{lemma}\ unique_NA:\ \isanewline\ \ \ \ \ "\isasymlbrakk Crypt(pubK\ B)\ \ \isasymlbrace Nonce\ NA,\ Agent\ A\ \isasymrbrace \ \isasymin \ parts(knows\ Spy\ evs);\ \ \isanewline\ \ \ \ \ \ \ Crypt(pubK\ B')\ \isasymlbrace Nonce\ NA,\ Agent\ A'\isasymrbrace \ \isasymin \ parts(knows\ Spy\ evs);\ \ \isanewline\ \ \ \ \ \ \ Nonce\ NA\ \isasymnotin \ analz\ (knows\ Spy\ 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 especiallyimportant because they fail for the original protocol. The followingtheorem states that if Bob sends message~2 to Alice, and both agents areuncompromised, 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\ (knows\ Spy\ evs)"\end{isabelle}%To prove it, we must formulate the induction properly (one of theassumptions mentions~\isa{evs}), apply induction, and simplify:\begin{isabelle}\isacommand{apply}\ (erule\ rev_mp,\ erule\ ns_public.induct,\ simp_all)\end{isabelle}%The proof states are too complicated to present in full. Let's examine the simplest subgoal, that for message~1. The followingevent has just occurred:\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'} \]The variables above have been primed because this stepbelongs to a different run from that referred to in the theoremstatement --- the theoremrefers to a past instance of message~2, while this subgoalconcerns message~1 being sent just now.In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$we have \isa{Ba} and~\isa{NAa}:\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}%The simplifier has used a default simplification rule that does a caseanalysis for each encrypted message on whether or not the decryption keyis compromised.\begin{isabelle} analz\ (insert\ (Crypt\ K\ X)\ H)\ =\isanewline \ (if\ Key\ (invKey\ K)\ \isasymin \ analz\ H\isanewline\ \ then\ insert\(Crypt\ K\ X)\ (anal\ z\ (insert\ X\ H))\isanewline \ \ else\ insert\ (Crypt\ K\ X)\ (analz\ H)) \rulename{analz_Crypt_if} \end{isabelle} The simplifier has also used \isa{Spy_see_priK}, proved in{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ \isasymin \ bad}.Recall that this subgoal concerns the casewhere the last message to be sent was\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'}. \]This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised,allowing the spy to decrypt the message. The Isabelle subgoal saysprecisely this, if we allow for its choice of variable names.Proving \isa{NB\ \isasymnoteq \ NAa} is easy: \isa{NB} wassent earlier, while \isa{NAa} is fresh; formally, we havethe assumption\isa{Nonce\ NAa\ \isasymnotin \ used\ evs1}. Note that our reasoning concerned \isa{B}'s participation in anotherrun. Agents may engage in several runs concurrently, and some attacks workby interleaving the messages of two runs. With model checking, thispossibility can cause a state-space explosion, and for us itcertainly complicates proofs. The biggest subgoal concerns message~2. Itsplits into several cases, such as whether or not the message just sent isthe very message mentioned in the theorem statement.Some of the cases are proved by unicity, others bythe induction hypothesis. For all those complications, the proofs areautomatic by \isa{blast} with the theorem \isa{no_nonce_NS1_NS2}.The remaining theorems about the protocol are not hard to prove. Thefollowing one asserts a form of \emph{authenticity}: if\isa{B} has sent an instance of message~2 to~\isa{A} and has received theexpected reply, then that reply really originated with~\isa{A}. Theproof 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 protocolrun 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 theflawed protocol establishes these properties for~\isa{A};the flaw only harms the second participant.\medskipDetailed information on this protocol verification technique can be foundelsewhere~\cite{paulson-jcs}, including proofs of an Internetprotocol~\cite{paulson-tls}. We must stress that the protocol discussedin this chapter is trivial. There are only three messages; no keys areexchanged; we merely have to prove that encrypted data remains secret. Real world protocols are much longer and distribute many secrets to theirparticipants. To be realistic, the model has to include the possibilityof keys being lost dynamically due to carelessness. If those keys havebeen used to encrypt other sensitive information, there may be cascadinglosses. We may still be able to establish a bound on the losses and toprove that other protocol runs functioncorrectly~\cite{paulson-yahalom}. Proofs of real-world protocols followthe strategy illustrated above, but the subgoals canbe much bigger and there are more of them.\index{protocols!security|)}\endinput