isabelle: src/HOL/Auth/README.html@ddea204de5bc (annotated)

3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	1	<!-- $Id$ -->
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	2	<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	3
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	4	<H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	5
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	6	<P>Cryptographic protocols are of major importance, especially with the
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	7	growing use of the Internet. This directory demonstrates a <A
4594 f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	8	HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">new
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	9	proof method</A>. The operational semantics of protocol participants is
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	10	defined inductively. The directory contains proofs concerning
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	11
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	12	<UL>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	13	<LI>three versions of the Otway-Rees protocol
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	14
4594 f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	15	<LI>the Needham-Schroeder protocol (public-key and shared-key versions)
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	16
6452 6a1b393ccdc0 addition of Kerberos IV example paulson parents: 6400 diff changeset	17	<LI>two versions of Kerberos: the simplified form published in the BAN paper
6a1b393ccdc0 addition of Kerberos IV example paulson parents: 6400 diff changeset	18	and also the full protocol (Kerberos IV)
6400 1f495d4d922b added new theory Yahalom_Bad paulson parents: 4594 diff changeset	19
1f495d4d922b added new theory Yahalom_Bad paulson parents: 4594 diff changeset	20	<LI>three versions of the Yahalom protocol, including a bad one that
1f495d4d922b added new theory Yahalom_Bad paulson parents: 4594 diff changeset	21	illustrates the purpose of the Oops rule
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	22
4594 f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	23	<LI>a novel recursive authentication protocol
f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	24
f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	25	<LI>the Internet protocol TLS
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	26	</UL>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	27
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	28	<HR>
4594 f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	29	<P>Last modified 30 Jan 1998
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	30
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	31	<ADDRESS>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	32	<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	33	</ADDRESS>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	34	</BODY></HTML>

author	nipkow
	Mon, 06 Aug 2001 13:43:24 +0200
changeset 11464	ddea204de5bc
parent 6452	6a1b393ccdc0
child 13508	890d736b93a5
permissions	-rw-r--r--