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

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

author	paulson
	Mon, 12 May 2003 12:26:50 +0200
changeset 14004	f7382ee9b574
parent 13508	890d736b93a5
child 14946	8aea9f96847f
permissions	-rw-r--r--