--- a/src/HOL/Auth/README.html Sat Aug 17 14:55:08 2002 +0200
+++ b/src/HOL/Auth/README.html Wed Aug 21 15:53:30 2002 +0200
@@ -1,13 +1,16 @@
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
-<H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>
+<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
<P>Cryptographic protocols are of major importance, especially with the
-growing use of the Internet. This directory demonstrates a <A
-HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">new
-proof method</A>. The operational semantics of protocol participants is
-defined inductively. The directory contains proofs concerning
+growing use of the Internet. This directory demonstrates a new proof method,
+which is described in <A
+HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
+papers</A>. The operational semantics of protocol participants is defined
+inductively.
+
+<P>This directory contains proofs concerning
<UL>
<LI>three versions of the Otway-Rees protocol
@@ -26,9 +29,11 @@
</UL>
<HR>
-<P>Last modified 30 Jan 1998
+<P>Last modified 20 August 2002
<ADDRESS>
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+<A
+HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
+<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
</BODY></HTML>