\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 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 by 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. The nonce in the reply must be cryptographically protected, since otherwise an adversary could easily replace it by a different one. 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} \index{Needham-Schroeder 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\index{Lowe, Gavin|(} 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} && \qquad 3'.&\quad C\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. Whether this counts as an attack has been disputed. In protocols of this type, we normally assume that the other party is honest. To be honest means to obey the protocol rules, so Alice's running the protocol with Charlie does not make her dishonest, just careless. After Lowe's attack, Alice has no grounds for complaint: this protocol does not have to guarantee anything if you run it with a bad person. Bob does have grounds for complaint, however: the protocol tells him that he is communicating with Alice (who is honest) but it does not guarantee secrecy of the nonces. Lowe also suggested a correction, 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. Below, we shall look at parts of this protocol's correctness proof. In ground-breaking work, Lowe~\cite{lowe-fdr}\index{Lowe, Gavin|)} 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.% \index{Needham-Schroeder protocol|)} \input{Message} \input{Event} \input{Public} \input{NS_Public}