doc-src/TutorialI/Protocol/protocol.tex

fixing list_to_set_comprehension simproc

+
−% $Id$
+
−\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{Protocol/document/Message}
+
−\input{Protocol/document/Event}
+
−\input{Protocol/document/Public}
+
−\input{Protocol/document/NS_Public}