diff -r 1fead823c7c6 -r 6e15de7dd871 doc-src/TutorialI/document/protocol.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/document/protocol.tex Tue Aug 28 14:37:57 2012 +0200 @@ -0,0 +1,135 @@ +\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}