--- /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}