1\chapter{Case Study: Verifying a Security Protocol} 2\label{chap:crypto} 3 4\index{protocols!security|(} 5 6%crypto primitives 7\def\lbb{\mathopen{\{\kern-.30em|}} 8\def\rbb{\mathclose{|\kern-.32em\}}} 9\def\comp#1{\lbb#1\rbb} 10 11Communications security is an ancient art. Julius Caesar is said to have 12encrypted his messages, shifting each letter three places along the 13alphabet. Mary Queen of Scots was convicted of treason after a cipher used 14in her letters was broken. Today's postal system 15incorporates security features. The envelope provides a degree of 16\emph{secrecy}. The signature provides \emph{authenticity} (proof of 17origin), as do departmental stamps and letterheads. 18 19Networks are vulnerable: messages pass through many computers, any of which 20might be controlled by an adversary, who thus can capture or redirect 21messages. People who wish to communicate securely over such a network can 22use cryptography, but if they are to understand each other, they need to 23follow a 24\emph{protocol}: a pre-arranged sequence of message formats. 25 26Protocols can be attacked in many ways, even if encryption is unbreakable. 27A \emph{splicing attack} involves an adversary's sending a message composed 28of parts of several old messages. This fake message may have the correct 29format, fooling an honest party. The adversary might be able to masquerade 30as somebody else, or he might obtain a secret key. 31 32\emph{Nonces} help prevent splicing attacks. A typical nonce is a 20-byte 33random number. Each message that requires a reply incorporates a nonce. The 34reply must include a copy of that nonce, to prove that it is not a replay of 35a past message. The nonce in the reply must be cryptographically 36protected, since otherwise an adversary could easily replace it by a 37different one. You should be starting to see that protocol design is 38tricky! 39 40Researchers are developing methods for proving the correctness of security 41protocols. The Needham-Schroeder public-key 42protocol~\cite{needham-schroeder} has become a standard test case. 43Proposed in 1978, it was found to be defective nearly two decades 44later~\cite{lowe-fdr}. This toy protocol will be useful in demonstrating 45how to verify protocols using Isabelle. 46 47 48\section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol} 49 50\index{Needham-Schroeder protocol|(}% 51This protocol uses public-key cryptography. Each person has a private key, known only to 52himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she 53encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the 54matching private key, which is needed in order to decrypt Alice's message. 55 56The core of the Needham-Schroeder protocol consists of three messages: 57\begin{alignat*}{2} 58 &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ 59 &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ 60 &3.&\quad A\to B &: \comp{Nb}\sb{Kb} 61\end{alignat*} 62First, let's understand the notation. In the first message, Alice 63sends Bob a message consisting of a nonce generated by Alice~($Na$) 64paired with Alice's name~($A$) and encrypted using Bob's public 65key~($Kb$). In the second message, Bob sends Alice a message 66consisting of $Na$ paired with a nonce generated by Bob~($Nb$), 67encrypted using Alice's public key~($Ka$). In the last message, Alice 68returns $Nb$ to Bob, encrypted using his public key. 69 70When Alice receives Message~2, she knows that Bob has acted on her 71message, since only he could have decrypted 72$\comp{Na,A}\sb{Kb}$ and extracted~$Na$. That is precisely what 73nonces are for. Similarly, message~3 assures Bob that Alice is 74active. But the protocol was widely believed~\cite{ban89} to satisfy a 75further property: that 76$Na$ and~$Nb$ were secrets shared by Alice and Bob. (Many 77protocols generate such shared secrets, which can be used 78to lessen the reliance on slow public-key operations.) 79Lowe\index{Lowe, Gavin|(} found this 80claim to be false: if Alice runs the protocol with someone untrustworthy 81(Charlie say), then he can start a new run with another agent (Bob say). 82Charlie uses Alice as an oracle, masquerading as 83Alice to Bob~\cite{lowe-fdr}. 84\begin{alignat*}{4} 85 &1.&\quad A\to C &: \comp{Na,A}\sb{Kc} && 86 \qquad 1'.&\quad C\to B &: \comp{Na,A}\sb{Kb} \\ 87 &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ 88 &3.&\quad A\to C &: \comp{Nb}\sb{Kc} && 89 \qquad 3'.&\quad C\to B &: \comp{Nb}\sb{Kb} 90\end{alignat*} 91In messages~1 and~3, Charlie removes the encryption using his private 92key and re-encrypts Alice's messages using Bob's public key. Bob is 93left thinking he has run the protocol with Alice, which was not 94Alice's intention, and Bob is unaware that the ``secret'' nonces are 95known to Charlie. This is a typical man-in-the-middle attack launched 96by an insider. 97 98Whether this counts as an attack has been disputed. In protocols of this 99type, we normally assume that the other party is honest. To be honest 100means to obey the protocol rules, so Alice's running the protocol with 101Charlie does not make her dishonest, just careless. After Lowe's 102attack, Alice has no grounds for complaint: this protocol does not have to 103guarantee anything if you run it with a bad person. Bob does have 104grounds for complaint, however: the protocol tells him that he is 105communicating with Alice (who is honest) but it does not guarantee 106secrecy of the nonces. 107 108Lowe also suggested a correction, namely to include Bob's name in 109message~2: 110\begin{alignat*}{2} 111 &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ 112 &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ 113 &3.&\quad A\to B &: \comp{Nb}\sb{Kb} 114\end{alignat*} 115If Charlie tries the same attack, Alice will receive the message 116$\comp{Na,Nb,B}\sb{Ka}$ when she was expecting to receive 117$\comp{Na,Nb,C}\sb{Ka}$. She will abandon the run, and eventually so 118will Bob. Below, we shall look at parts of this protocol's correctness 119proof. 120 121In ground-breaking work, Lowe~\cite{lowe-fdr}\index{Lowe, Gavin|)} 122showed how such attacks 123could be found automatically using a model checker. An alternative, 124which we shall examine below, is to prove protocols correct. Proofs 125can be done under more realistic assumptions because our model does 126not have to be finite. The strategy is to formalize the operational 127semantics of the system and to prove security properties using rule 128induction.% 129\index{Needham-Schroeder protocol|)} 130 131 132\input{Message} 133\input{Event} 134\input{Public} 135\input{NS_Public} 136