doc-src/TutorialI/Protocol/protocol.tex

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