--- a/doc-src/TutorialI/Protocol/protocol.tex Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-\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{document/Message}
-\input{document/Event}
-\input{document/Public}
-\input{document/NS_Public}