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

15283 f21466450330 DOCTYPE declaration added webertj parents: 14946 diff changeset	1	<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added webertj parents: 14946 diff changeset	2
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	3	<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	4
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 6452 diff changeset	5	<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	6
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	7	<P>Cryptographic protocols are of major importance, especially with the
14004 f7382ee9b574 updated text paulson parents: 13508 diff changeset	8	growing use of the Internet. This directory demonstrates the ``inductive
f7382ee9b574 updated text paulson parents: 13508 diff changeset	9	method'' of protocol verification, which is described in <A
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 6452 diff changeset	10	HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 6452 diff changeset	11	papers</A>. The operational semantics of protocol participants is defined
14004 f7382ee9b574 updated text paulson parents: 13508 diff changeset	12	inductively.
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 6452 diff changeset	13
890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 6452 diff changeset	14	<P>This directory contains proofs concerning
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	15
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	16	<UL>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	17	<LI>three versions of the Otway-Rees protocol
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	18
14004 f7382ee9b574 updated text paulson parents: 13508 diff changeset	19	<LI>the Needham-Schroeder shared-key protocol
f7382ee9b574 updated text paulson parents: 13508 diff changeset	20
f7382ee9b574 updated text paulson parents: 13508 diff changeset	21	<LI>the Needham-Schroeder public-key protocol (original and with Lowe's
f7382ee9b574 updated text paulson parents: 13508 diff changeset	22	modification)
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	23
6452 6a1b393ccdc0 addition of Kerberos IV example paulson parents: 6400 diff changeset	24	<LI>two versions of Kerberos: the simplified form published in the BAN paper
6a1b393ccdc0 addition of Kerberos IV example paulson parents: 6400 diff changeset	25	and also the full protocol (Kerberos IV)
6400 1f495d4d922b added new theory Yahalom_Bad paulson parents: 4594 diff changeset	26
1f495d4d922b added new theory Yahalom_Bad paulson parents: 4594 diff changeset	27	<LI>three versions of the Yahalom protocol, including a bad one that
1f495d4d922b added new theory Yahalom_Bad paulson parents: 4594 diff changeset	28	illustrates the purpose of the Oops rule
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	29
4594 f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	30	<LI>a novel recursive authentication protocol
f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	31
f8d4387b40d9 fixed WWW links paulson parents: 3119 diff changeset	32	<LI>the Internet protocol TLS
14004 f7382ee9b574 updated text paulson parents: 13508 diff changeset	33
f7382ee9b574 updated text paulson parents: 13508 diff changeset	34	<LI>The certified e-mail protocol of Abadi et al.
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	35	</UL>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	36
14946 8aea9f96847f fixed bad link paulson parents: 14004 diff changeset	37	<P>Frederic Blanqui has contributed a theory of guardedness, which is
8aea9f96847f fixed bad link paulson parents: 14004 diff changeset	38	demonstrated by proofs of some roving agent protocols.
14004 f7382ee9b574 updated text paulson parents: 13508 diff changeset	39
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	40	<HR>
14004 f7382ee9b574 updated text paulson parents: 13508 diff changeset	41	<P>Last modified $Date$
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	42
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	43	<ADDRESS>
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 6452 diff changeset	44	<A
890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 6452 diff changeset	45	HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 6452 diff changeset	46	<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
3119 bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	47	</ADDRESS>
bb2ee88aa43f Description of the Auth directory: security protocols proofs paulson parents: diff changeset	48	</BODY></HTML>

author	nipkow
	Mon, 07 Feb 2005 08:02:49 +0100
changeset 15503	38616a65bfbd
parent 15283	f21466450330
child 15582	7219facb3fd0
permissions	-rw-r--r--