# HG changeset patch
# User nipkow
# Date 987779927 -7200
# Node ID 9fde0021e1af363838e77bd2521284ea835e0ca8
# Parent  51bcafc7bfca3b0804ad62d6876cdb7489163c33
*** empty log message ***

diff -r 51bcafc7bfca -r 9fde0021e1af doc-src/TutorialI/Protocol/protocol.tex
--- 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
 follow a
@@ -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.