Tutorial/document/protocol.tex

11 Communications security is an ancient art.  Julius Caesar is said to have
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
29 format, fooling an honest party.  The adversary might be able to masquerade
34 reply must include a copy of that nonce, to prove that it is not a replay of
37 different one. You should be starting to see that protocol design is
43 Proposed in 1978, it was found to be defective nearly two decades
45 how to verify protocols using Isabelle.
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.
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}
68 returns $Nb$ to Bob, encrypted using his public key.
74 active.  But the protocol was widely believed~\cite{ban89} to satisfy a
78 to lessen the reliance on slow public-key operations.)
80 claim to be false: if Alice runs the protocol with someone untrustworthy
83 Alice to Bob~\cite{lowe-fdr}.
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}
95 known to Charlie.  This is a typical man-in-the-middle attack launched
100 means to obey the protocol rules, so Alice's running the protocol with
102 attack, Alice has no grounds for complaint: this protocol does not have to
108 Lowe also suggested a correction, namely to include Bob's name in
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}
116 $\comp{Na,Nb,B}\sb{Ka}$ when she was expecting to receive
124 which we shall examine below, is to prove protocols correct.  Proofs
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