1184902Srwatson\chapter{Case Study: Verifying a Security Protocol}
2184902Srwatson\label{chap:crypto}
3184902Srwatson
4184902Srwatson\index{protocols!security|(}
5184902Srwatson
6184902Srwatson%crypto primitives 
7184902Srwatson\def\lbb{\mathopen{\{\kern-.30em|}}
8184902Srwatson\def\rbb{\mathclose{|\kern-.32em\}}}
9184902Srwatson\def\comp#1{\lbb#1\rbb}
10184902Srwatson
11184902SrwatsonCommunications security is an ancient art.  Julius Caesar is said to have
12184902Srwatsonencrypted his messages, shifting each letter three places along the
13184902Srwatsonalphabet.  Mary Queen of Scots was convicted of treason after a cipher used
14184902Srwatsonin her letters was broken.  Today's postal system
15184902Srwatsonincorporates security features.  The envelope provides a degree of
16184902Srwatson\emph{secrecy}.  The signature provides \emph{authenticity} (proof of
17184902Srwatsonorigin), as do departmental stamps and letterheads.
18184902Srwatson
19184902SrwatsonNetworks are vulnerable: messages pass through many computers, any of which
20184902Srwatsonmight be controlled by an adversary, who thus can capture or redirect
21184902Srwatsonmessages.  People who wish to communicate securely over such a network can
22184902Srwatsonuse cryptography, but if they are to understand each other, they need to
23184902Srwatsonfollow a
24184902Srwatson\emph{protocol}: a pre-arranged sequence of message formats. 
25184902Srwatson
26184902SrwatsonProtocols can be attacked in many ways, even if encryption is unbreakable. 
27184902SrwatsonA \emph{splicing attack} involves an adversary's sending a message composed
28184902Srwatsonof parts of several old messages.  This fake message may have the correct
29184902Srwatsonformat, fooling an honest party.  The adversary might be able to masquerade
30184902Srwatsonas somebody else, or he might obtain a secret key.
31184902Srwatson
32184902Srwatson\emph{Nonces} help prevent splicing attacks. A typical nonce is a 20-byte
33184902Srwatsonrandom number. Each message that requires a reply incorporates a nonce. The
34reply must include a copy of that nonce, to prove that it is not a replay of
35a past message.  The nonce in the reply must be cryptographically
36protected, since otherwise an adversary could easily replace it by a
37different one. You should be starting to see that protocol design is
38tricky!
39
40Researchers are developing methods for proving the correctness of security
41protocols.  The Needham-Schroeder public-key
42protocol~\cite{needham-schroeder} has become a standard test case. 
43Proposed in 1978, it was found to be defective nearly two decades
44later~\cite{lowe-fdr}.  This toy protocol will be useful in demonstrating
45how to verify protocols using Isabelle.
46
47
48\section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol}
49
50\index{Needham-Schroeder protocol|(}%
51This protocol uses public-key cryptography. Each person has a private key, known only to
52himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she
53encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the
54matching private key, which is needed in order to decrypt Alice's message.
55
56The core of the Needham-Schroeder protocol consists of three messages:
57\begin{alignat*}{2}
58  &1.&\quad  A\to B  &: \comp{Na,A}\sb{Kb} \\
59  &2.&\quad  B\to A  &: \comp{Na,Nb}\sb{Ka} \\
60  &3.&\quad  A\to B  &: \comp{Nb}\sb{Kb}
61\end{alignat*}
62First, let's understand the notation. In the first message, Alice
63sends Bob a message consisting of a nonce generated by Alice~($Na$)
64paired  with Alice's name~($A$) and encrypted using Bob's public
65key~($Kb$). In the second message, Bob sends Alice a message
66consisting of $Na$ paired with a nonce generated by Bob~($Nb$), 
67encrypted using Alice's public key~($Ka$). In the last message, Alice
68returns $Nb$ to Bob, encrypted using his public key.
69
70When Alice receives Message~2, she knows that Bob has acted on her
71message, since only he could have decrypted
72$\comp{Na,A}\sb{Kb}$ and extracted~$Na$.  That is precisely what
73nonces are for.  Similarly, message~3 assures Bob that Alice is
74active.  But the protocol was widely believed~\cite{ban89} to satisfy a
75further property: that
76$Na$ and~$Nb$ were secrets shared by Alice and Bob.  (Many
77protocols generate such shared secrets, which can be used
78to lessen the reliance on slow public-key operations.)  
79Lowe\index{Lowe, Gavin|(} found this
80claim to be false: if Alice runs the protocol with someone untrustworthy
81(Charlie say), then he can start a new run with another agent (Bob say). 
82Charlie uses Alice as an oracle, masquerading as
83Alice to Bob~\cite{lowe-fdr}.
84\begin{alignat*}{4}
85  &1.&\quad  A\to C  &: \comp{Na,A}\sb{Kc}   &&
86      \qquad 1'.&\quad  C\to B  &: \comp{Na,A}\sb{Kb} \\
87  &2.&\quad  B\to A  &: \comp{Na,Nb}\sb{Ka} \\
88  &3.&\quad  A\to C  &: \comp{Nb}\sb{Kc}  &&
89      \qquad 3'.&\quad  C\to B  &: \comp{Nb}\sb{Kb}
90\end{alignat*}
91In messages~1 and~3, Charlie removes the encryption using his private
92key and re-encrypts Alice's messages using Bob's public key. Bob is
93left thinking he has run the protocol with Alice, which was not
94Alice's intention, and Bob is unaware that the ``secret'' nonces are
95known to Charlie.  This is a typical man-in-the-middle attack launched
96by an insider.
97
98Whether this counts as an attack has been disputed.  In protocols of this
99type, we normally assume that the other party is honest.  To be honest
100means to obey the protocol rules, so Alice's running the protocol with
101Charlie does not make her dishonest, just careless.  After Lowe's
102attack, Alice has no grounds for complaint: this protocol does not have to
103guarantee anything if you run it with a bad person.  Bob does have
104grounds for complaint, however: the protocol tells him that he is
105communicating with Alice (who is honest) but it does not guarantee
106secrecy of the nonces.
107
108Lowe also suggested a correction, namely to include Bob's name in
109message~2:
110\begin{alignat*}{2}
111  &1.&\quad  A\to B  &: \comp{Na,A}\sb{Kb} \\
112  &2.&\quad  B\to A  &: \comp{Na,Nb,B}\sb{Ka} \\
113  &3.&\quad  A\to B  &: \comp{Nb}\sb{Kb}
114\end{alignat*}
115If Charlie tries the same attack, Alice will receive the message
116$\comp{Na,Nb,B}\sb{Ka}$ when she was expecting to receive
117$\comp{Na,Nb,C}\sb{Ka}$.  She will abandon the run, and eventually so
118will Bob.  Below, we shall look at parts of this protocol's correctness
119proof. 
120
121In ground-breaking work, Lowe~\cite{lowe-fdr}\index{Lowe, Gavin|)}
122showed how such attacks
123could be found automatically using a model checker.  An alternative,
124which we shall examine below, is to prove protocols correct.  Proofs
125can be done under more realistic assumptions because our model does
126not have to be finite.  The strategy is to formalize the operational
127semantics of the system and to prove security properties using rule
128induction.%
129\index{Needham-Schroeder protocol|)}
130
131
132\input{Message}
133\input{Event}
134\input{Public}
135\input{NS_Public}
136