author | wenzelm |
Tue, 28 Aug 2012 14:37:57 +0200 | |
changeset 48966 | 6e15de7dd871 |
parent 48522 | doc-src/TutorialI/Protocol/protocol.tex@708278fc2dff |
permissions | -rw-r--r-- |
11428 | 1 |
\chapter{Case Study: Verifying a Security Protocol} |
11248 | 2 |
\label{chap:crypto} |
3 |
||
11428 | 4 |
\index{protocols!security|(} |
5 |
||
11267 | 6 |
%crypto primitives |
11248 | 7 |
\def\lbb{\mathopen{\{\kern-.30em|}} |
8 |
\def\rbb{\mathclose{|\kern-.32em\}}} |
|
9 |
\def\comp#1{\lbb#1\rbb} |
|
10 |
||
11 |
Communications security is an ancient art. Julius Caesar is said to have |
|
12 |
encrypted his messages, shifting each letter three places along the |
|
13 |
alphabet. Mary Queen of Scots was convicted of treason after a cipher used |
|
11267 | 14 |
in her letters was broken. Today's postal system |
15 |
incorporates security features. The envelope provides a degree of |
|
11248 | 16 |
\emph{secrecy}. The signature provides \emph{authenticity} (proof of |
11267 | 17 |
origin), as do departmental stamps and letterheads. |
11248 | 18 |
|
19 |
Networks are vulnerable: messages pass through many computers, any of which |
|
11262 | 20 |
might be controlled by an adversary, who thus can capture or redirect |
11248 | 21 |
messages. People who wish to communicate securely over such a network can |
22 |
use cryptography, but if they are to understand each other, they need to |
|
23 |
follow a |
|
24 |
\emph{protocol}: a pre-arranged sequence of message formats. |
|
25 |
||
26 |
Protocols can be attacked in many ways, even if encryption is unbreakable. |
|
27 |
A \emph{splicing attack} involves an adversary's sending a message composed |
|
28 |
of parts of several old messages. This fake message may have the correct |
|
29 |
format, fooling an honest party. The adversary might be able to masquerade |
|
30 |
as somebody else, or he might obtain a secret key. |
|
31 |
||
32 |
\emph{Nonces} help prevent splicing attacks. A typical nonce is a 20-byte |
|
33 |
random number. Each message that requires a reply incorporates a nonce. The |
|
34 |
reply must include a copy of that nonce, to prove that it is not a replay of |
|
11267 | 35 |
a past message. The nonce in the reply must be cryptographically |
36 |
protected, since otherwise an adversary could easily replace it by a |
|
37 |
different one. You should be starting to see that protocol design is |
|
38 |
tricky! |
|
11248 | 39 |
|
40 |
Researchers are developing methods for proving the correctness of security |
|
41 |
protocols. The Needham-Schroeder public-key |
|
42 |
protocol~\cite{needham-schroeder} has become a standard test case. |
|
43 |
Proposed in 1978, it was found to be defective nearly two decades |
|
44 |
later~\cite{lowe-fdr}. This toy protocol will be useful in demonstrating |
|
45 |
how to verify protocols using Isabelle. |
|
46 |
||
47 |
||
48 |
\section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol} |
|
49 |
||
11428 | 50 |
\index{Needham-Schroeder protocol|(}% |
11248 | 51 |
This protocol uses public-key cryptography. Each person has a private key, known only to |
52 |
himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she |
|
53 |
encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the |
|
54 |
matching private key, which is needed in order to decrypt Alice's message. |
|
55 |
||
56 |
The 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*} |
|
62 |
First, let's understand the notation. In the first message, Alice |
|
63 |
sends Bob a message consisting of a nonce generated by Alice~($Na$) |
|
64 |
paired with Alice's name~($A$) and encrypted using Bob's public |
|
65 |
key~($Kb$). In the second message, Bob sends Alice a message |
|
66 |
consisting of $Na$ paired with a nonce generated by Bob~($Nb$), |
|
67 |
encrypted using Alice's public key~($Ka$). In the last message, Alice |
|
68 |
returns $Nb$ to Bob, encrypted using his public key. |
|
69 |
||
70 |
When Alice receives Message~2, she knows that Bob has acted on her |
|
71 |
message, since only he could have decrypted |
|
72 |
$\comp{Na,A}\sb{Kb}$ and extracted~$Na$. That is precisely what |
|
73 |
nonces are for. Similarly, message~3 assures Bob that Alice is |
|
74 |
active. But the protocol was widely believed~\cite{ban89} to satisfy a |
|
75 |
further property: that |
|
76 |
$Na$ and~$Nb$ were secrets shared by Alice and Bob. (Many |
|
77 |
protocols generate such shared secrets, which can be used |
|
11428 | 78 |
to lessen the reliance on slow public-key operations.) |
79 |
Lowe\index{Lowe, Gavin|(} found this |
|
11248 | 80 |
claim 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). |
|
82 |
Charlie uses Alice as an oracle, masquerading as |
|
83 |
Alice to Bob~\cite{lowe-fdr}. |
|
84 |
\begin{alignat*}{4} |
|
11267 | 85 |
&1.&\quad A\to C &: \comp{Na,A}\sb{Kc} && |
11248 | 86 |
\qquad 1'.&\quad C\to B &: \comp{Na,A}\sb{Kb} \\ |
87 |
&2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ |
|
11267 | 88 |
&3.&\quad A\to C &: \comp{Nb}\sb{Kc} && |
89 |
\qquad 3'.&\quad C\to B &: \comp{Nb}\sb{Kb} |
|
11248 | 90 |
\end{alignat*} |
91 |
In messages~1 and~3, Charlie removes the encryption using his private |
|
92 |
key and re-encrypts Alice's messages using Bob's public key. Bob is |
|
93 |
left thinking he has run the protocol with Alice, which was not |
|
94 |
Alice's intention, and Bob is unaware that the ``secret'' nonces are |
|
95 |
known to Charlie. This is a typical man-in-the-middle attack launched |
|
96 |
by an insider. |
|
97 |
||
11267 | 98 |
Whether this counts as an attack has been disputed. In protocols of this |
99 |
type, we normally assume that the other party is honest. To be honest |
|
100 |
means to obey the protocol rules, so Alice's running the protocol with |
|
101 |
Charlie does not make her dishonest, just careless. After Lowe's |
|
102 |
attack, Alice has no grounds for complaint: this protocol does not have to |
|
103 |
guarantee anything if you run it with a bad person. Bob does have |
|
104 |
grounds for complaint, however: the protocol tells him that he is |
|
105 |
communicating with Alice (who is honest) but it does not guarantee |
|
106 |
secrecy of the nonces. |
|
107 |
||
108 |
Lowe also suggested a correction, namely to include Bob's name in |
|
109 |
message~2: |
|
11248 | 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*} |
|
115 |
If 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 |
|
11267 | 118 |
will Bob. Below, we shall look at parts of this protocol's correctness |
119 |
proof. |
|
11248 | 120 |
|
11428 | 121 |
In ground-breaking work, Lowe~\cite{lowe-fdr}\index{Lowe, Gavin|)} |
122 |
showed how such attacks |
|
11248 | 123 |
could be found automatically using a model checker. An alternative, |
124 |
which we shall examine below, is to prove protocols correct. Proofs |
|
125 |
can be done under more realistic assumptions because our model does |
|
126 |
not have to be finite. The strategy is to formalize the operational |
|
127 |
semantics of the system and to prove security properties using rule |
|
11428 | 128 |
induction.% |
129 |
\index{Needham-Schroeder protocol|)} |
|
11248 | 130 |
|
131 |
||
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
132 |
\input{Message} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
133 |
\input{Event} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
134 |
\input{Public} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
135 |
\input{NS_Public} |