NameDateSize

..25-Jul-2019169

All_Symmetric.thyH A D25-Jul-2019297

Auth_Public.thyH A D25-Jul-2019335

Auth_Shared.thyH A D25-Jul-2019501

CertifiedEmail.thyH A D25-Jul-201919.1 KiB

document/H25-Jul-20193

Event.thyH A D25-Jul-201910.8 KiB

Guard/H25-Jul-201918

Kerberos_BAN.thyH A D25-Jul-201928.4 KiB

Kerberos_BAN_Gets.thyH A D25-Jul-201929.1 KiB

KerberosIV.thyH A D25-Jul-201976.2 KiB

KerberosIV_Gets.thyH A D25-Jul-201962.4 KiB

KerberosV.thyH A D25-Jul-201965.3 KiB

Message.thyH A D25-Jul-201931.9 KiB

NS_Public.thyH A D25-Jul-20198.8 KiB

NS_Public_Bad.thyH A D25-Jul-20199.9 KiB

NS_Shared.thyH A D25-Jul-201923.1 KiB

OtwayRees.thyH A D25-Jul-201920.7 KiB

OtwayRees_AN.thyH A D25-Jul-201912.5 KiB

OtwayRees_Bad.thyH A D25-Jul-201912.4 KiB

OtwayReesBella.thyH A D25-Jul-201916.4 KiB

Public.thyH A D25-Jul-201914.3 KiB

README.htmlH A D25-Jul-20191.5 KiB

Recur.thyH A D25-Jul-201918.9 KiB

Shared.thyH A D25-Jul-20198.7 KiB

Smartcard/H25-Jul-20197

TLS.thyH A D25-Jul-201938.7 KiB

WooLam.thyH A D25-Jul-20196.7 KiB

Yahalom.thyH A D25-Jul-201928.6 KiB

Yahalom2.thyH A D25-Jul-201918.9 KiB

Yahalom_Bad.thyH A D25-Jul-201915.2 KiB

ZhouGollmann.thyH A D25-Jul-201917.3 KiB

README.html

1<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
2
3<HTML>
4
5<HEAD>
6  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
7  <TITLE>HOL/Auth/README</TITLE>
8</HEAD>
9
10<BODY>
11
12<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
13
14<P>Cryptographic protocols are of major importance, especially with the
15growing use of the Internet.  This directory demonstrates the ``inductive
16method'' of protocol verification, which is described in <A
17HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
18papers</A>.  The operational semantics of protocol participants is defined
19inductively.
20
21<P>This directory contains proofs concerning
22
23<UL>
24<LI>three versions of the Otway-Rees protocol
25
26<LI>the Needham-Schroeder shared-key protocol
27
28<LI>the Needham-Schroeder public-key protocol (original and with Lowe's
29modification)
30
31<LI>two versions of Kerberos: the simplified form published in the BAN paper
32	and also the full protocol (Kerberos IV)
33
34<LI>three versions of the Yahalom protocol, including a bad one that 
35	illustrates the purpose of the Oops rule
36
37<LI>a novel recursive authentication protocol 
38
39<LI>the Internet protocol TLS
40
41<LI>The certified e-mail protocol of Abadi et al.
42</UL>
43
44<P>Frederic Blanqui has contributed a theory of guardedness, which is
45demonstrated by proofs of some roving agent protocols.
46
47<ADDRESS>
48<A
49HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
50<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
51</ADDRESS>
52</BODY>
53</HTML>
54