src/HOL/Auth/README.html
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 6452 6a1b393ccdc0
child 13508 890d736b93a5
permissions -rw-r--r--
hide many names from Datatype_Universe.

<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>

<H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>

<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

<UL>
<LI>three versions of the Otway-Rees protocol

<LI>the Needham-Schroeder protocol (public-key and shared-key versions)

<LI>two versions of Kerberos: the simplified form published in the BAN paper
	and also the full protocol (Kerberos IV)

<LI>three versions of the Yahalom protocol, including a bad one that 
	illustrates the purpose of the Oops rule

<LI>a novel recursive authentication protocol 

<LI>the Internet protocol TLS
</UL>

<HR>
<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>
</ADDRESS>
</BODY></HTML>