# HG changeset patch
# User paulson
# Date 886420584 -3600
# Node ID f8d4387b40d91f7f6ee963ec1e23e624c3073ec1
# Parent  6fc8f224655fe756381167cf3c3eb5399357fb1c
fixed WWW links

diff -r 6fc8f224655f -r f8d4387b40d9 src/HOL/Auth/README.html
--- a/src/HOL/Auth/README.html	Mon Feb 02 12:55:39 1998 +0100
+++ b/src/HOL/Auth/README.html	Mon Feb 02 12:56:24 1998 +0100
@@ -5,24 +5,24 @@
 
 <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/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.dvi.gz">new
+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
 
 <UL>
 <LI>three versions of the Otway-Rees protocol
 
-<LI>the Needham-Schroeder protocol (<A
-HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR413-lcp-Mechanized-Proofs-of-Security-Protocols-Needham-Schroeder-with-Public-Keys.dvi.gz">public-key</A>
-and shared-key versions)
+<LI>the Needham-Schroeder protocol (public-key and shared-key versions)
 
 <LI>two versions of the Yahalom protocol
 
-<LI>a novel <A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz">recursive</A> authentication protocol 
+<LI>a novel recursive authentication protocol 
+
+<LI>the Internet protocol TLS
 </UL>
 
 <HR>
-<P>Last modified 7 May 1997
+<P>Last modified 30 Jan 1998
 
 <ADDRESS>
 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>