author nipkow Fri, 20 Apr 2001 17:18:47 +0200 changeset 11262 9fde0021e1af parent 11261 51bcafc7bfca child 11263 e502756bcb11
*** empty log message ***
--- a/doc-src/TutorialI/Protocol/protocol.tex	Fri Apr 20 11:11:40 2001 +0200
+++ b/doc-src/TutorialI/Protocol/protocol.tex	Fri Apr 20 17:18:47 2001 +0200
@@ -16,7 +16,7 @@
origin), as do departmental stamps and letterheads.

Networks are vulnerable: messages pass through many computers, any of which
-might be controlled an adversary, who thus can capture or redirect
+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
@@ -146,7 +146,7 @@

Since datatype constructors are injective, we have the theorem
\begin{isabelle}
-Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand X=X'.
+Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand\ X=X'.
\end{isabelle}
A ciphertext can be decrypted using only one key and
can yield only one plaintext.  This assumption is realistic if encryption
@@ -277,7 +277,7 @@
\end{isabelle}

The function \isa{knows} formalizes an agent's knowledge.  Mostly we only
-case about the spy's knowledge, and \isa{knows Spy evs} is the set of items
+care about the spy's knowledge, and \isa{knows Spy evs} is the set of items
available to the spy in the trace~\isa{evs}.  Already in the empty trace,
the spy starts with some secrets at his disposal, such as the private keys
of compromised users.  After each \isa{Says} event, the spy learns the
@@ -297,7 +297,7 @@
\begin{isabelle}
\isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
\isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
-\isacommand{translations}\ \ \ \ "priK\ x"\ \ ==\ "invKey(pubK\ x)"
+\isacommand{translations}\ \ \ \ "priK\ x"\ \ \isasymrightleftharpoons\ \ "invKey(pubK\ x)"
\end{isabelle}
The set \isa{bad} consists of those agents whose private keys are known to
the spy.