equal
deleted
inserted
replaced
14 features. The envelope provides a degree of |
14 features. The envelope provides a degree of |
15 \emph{secrecy}. The signature provides \emph{authenticity} (proof of |
15 \emph{secrecy}. The signature provides \emph{authenticity} (proof of |
16 origin), as do departmental stamps and letterheads. |
16 origin), as do departmental stamps and letterheads. |
17 |
17 |
18 Networks are vulnerable: messages pass through many computers, any of which |
18 Networks are vulnerable: messages pass through many computers, any of which |
19 might be controlled an adversary, who thus can capture or redirect |
19 might be controlled by an adversary, who thus can capture or redirect |
20 messages. People who wish to communicate securely over such a network can |
20 messages. People who wish to communicate securely over such a network can |
21 use cryptography, but if they are to understand each other, they need to |
21 use cryptography, but if they are to understand each other, they need to |
22 follow a |
22 follow a |
23 \emph{protocol}: a pre-arranged sequence of message formats. |
23 \emph{protocol}: a pre-arranged sequence of message formats. |
24 |
24 |
144 abbreviates |
144 abbreviates |
145 $\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. |
145 $\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. |
146 |
146 |
147 Since datatype constructors are injective, we have the theorem |
147 Since datatype constructors are injective, we have the theorem |
148 \begin{isabelle} |
148 \begin{isabelle} |
149 Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand X=X'. |
149 Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand\ X=X'. |
150 \end{isabelle} |
150 \end{isabelle} |
151 A ciphertext can be decrypted using only one key and |
151 A ciphertext can be decrypted using only one key and |
152 can yield only one plaintext. This assumption is realistic if encryption |
152 can yield only one plaintext. This assumption is realistic if encryption |
153 includes some built-in redundancy. |
153 includes some built-in redundancy. |
154 |
154 |
275 \ \ \ \ \ used\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\ \isacharbraceleft |
275 \ \ \ \ \ used\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\ \isacharbraceleft |
276 X\isacharbraceright \ \isasymunion\ (used\ evs) |
276 X\isacharbraceright \ \isasymunion\ (used\ evs) |
277 \end{isabelle} |
277 \end{isabelle} |
278 |
278 |
279 The function \isa{knows} formalizes an agent's knowledge. Mostly we only |
279 The function \isa{knows} formalizes an agent's knowledge. Mostly we only |
280 case about the spy's knowledge, and \isa{knows Spy evs} is the set of items |
280 care about the spy's knowledge, and \isa{knows Spy evs} is the set of items |
281 available to the spy in the trace~\isa{evs}. Already in the empty trace, |
281 available to the spy in the trace~\isa{evs}. Already in the empty trace, |
282 the spy starts with some secrets at his disposal, such as the private keys |
282 the spy starts with some secrets at his disposal, such as the private keys |
283 of compromised users. After each \isa{Says} event, the spy learns the |
283 of compromised users. After each \isa{Says} event, the spy learns the |
284 message that was sent. Combinations of functions express other important |
284 message that was sent. Combinations of functions express other important |
285 concepts involving~\isa{evs}: |
285 concepts involving~\isa{evs}: |
295 \isa{priK} maps agents to their private keys, is defined in terms of |
295 \isa{priK} maps agents to their private keys, is defined in terms of |
296 \isa{invKey} and \isa{pubK} by a translation. |
296 \isa{invKey} and \isa{pubK} by a translation. |
297 \begin{isabelle} |
297 \begin{isabelle} |
298 \isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline |
298 \isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline |
299 \isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline |
299 \isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline |
300 \isacommand{translations}\ \ \ \ "priK\ x"\ \ ==\ "invKey(pubK\ x)" |
300 \isacommand{translations}\ \ \ \ "priK\ x"\ \ \isasymrightleftharpoons\ \ "invKey(pubK\ x)" |
301 \end{isabelle} |
301 \end{isabelle} |
302 The set \isa{bad} consists of those agents whose private keys are known to |
302 The set \isa{bad} consists of those agents whose private keys are known to |
303 the spy. |
303 the spy. |
304 |
304 |
305 Two axioms are asserted about the public-key cryptosystem. |
305 Two axioms are asserted about the public-key cryptosystem. |