author  paulson 
Tue, 20 Apr 1999 14:33:48 +0200  
changeset 6452  6a1b393ccdc0 
parent 6400  1f495d4d922b 
child 13508  890d736b93a5 
permissions  rwrr 
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>AuthThe 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  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 OtwayRees protocol 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

14 

4594  15 
<LI>the NeedhamSchroeder protocol (publickey and sharedkey versions) 
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

16 

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

6400  19 

20 
<LI>three versions of the Yahalom protocol, including a bad one that 

21 
illustrates the purpose of the Oops rule 

3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

22 

4594  23 
<LI>a novel recursive authentication protocol 
24 

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  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> 