author  paulson 
Mon, 02 Feb 1998 12:56:24 +0100  
changeset 4594  f8d4387b40d9 
parent 3119  bb2ee88aa43f 
child 6400  1f495d4d922b 
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 

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

17 
<LI>two versions of the Yahalom protocol 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

18 

4594  19 
<LI>a novel recursive authentication protocol 
20 

21 
<LI>the Internet protocol TLS 

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

22 
</UL> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

23 

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

24 
<HR> 
4594  25 
<P>Last modified 30 Jan 1998 
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

26 

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

27 
<ADDRESS> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

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

29 
</ADDRESS> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

30 
</BODY></HTML> 