--- a/src/HOL/Auth/Guard/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- <TITLE>HOL/Auth/Guard/README.html</TITLE>
-</HEAD>
-
-<BODY>
-
-<H1>Protocol-Independent Secrecy Results</H1>
-
-date: april 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage:
-
-<P>The current development is built above the HOL (Higher-Order Logic)
-Isabelle theory and the formalization of protocols introduced by <A
-HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>. More details are
-in his paper <A
-HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Auth/jcs.pdf">
-The Inductive approach
-to verifying cryptographic protocols</A> (J. Computer Security 6, pages
-85-128, 1998).
-
-<P>
-This directory contains a number of files:
-
-<UL>
-<LI>Extensions.thy contains extensions of Larry Paulson's files with many useful
-lemmas.
-
-<LI>Analz contains an important theorem about the decomposition of analz
-between pparts (pairs) and kparts (messages that are not pairs).
-
-<LI>Guard contains the protocol-independent secrecy theorem for nonces.
-<LI>GuardK is the same for keys.
-<LI>Guard_Public extends Guard and GuardK for public-key protocols.
-<LI>Guard_Shared extends Guard and GuardK for symmetric-key protocols.
-
-<LI>List_Msg contains definitions on lists (inside messages).
-
-<LI>P1 contains the definition of the protocol P1 and the proof of its
-properties (strong forward integrity, insertion resilience, truncation
-resilience, data confidentiality and non-repudiability)
-
-<LI>P2 is the same for the protocol P2
-
-<LI>NS_Public is for Needham-Schroeder-Lowe
-<LI>OtwayRees is for Otway-Rees
-<LI>Yahalom is for Yahalom
-
-<LI>Proto contains a more precise formalization of protocols with rules
-and a protocol-independent theorem for proving guardness from a preservation
-property. It also contains the proofs for Needham-Schroeder as an example.
-</UL>
-
-<HR>
-<P>Last modified 20 August 2002
-
-<ADDRESS>
-<A HREF="http://www.lri.fr/~blanqui/">Frederic Blanqui</A>,
-<A HREF="mailto:blanqui@lri.fr">blanqui@lri.fr</A>
-</ADDRESS>
-</BODY>
-</HTML>