src/HOL/Auth/README.html
author paulson
Wed, 21 Aug 2002 15:53:30 +0200
changeset 13508 890d736b93a5
parent 6452 6a1b393ccdc0
child 14004 f7382ee9b574
permissions -rw-r--r--
Frederic Blanqui's new "guard" examples
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
13508
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
     4
<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
3119
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
13508
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
     7
growing use of the Internet.  This directory demonstrates a new proof method,
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
     8
which is described in <A
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
     9
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
    10
papers</A>.  The operational semantics of protocol participants is defined
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
    11
inductively.  
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
    12
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
    13
<P>This directory contains proofs concerning
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    14
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    15
<UL>
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    16
<LI>three versions of the Otway-Rees protocol
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    17
4594
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    18
<LI>the Needham-Schroeder protocol (public-key and shared-key versions)
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    19
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents: 6400
diff changeset
    20
<LI>two versions of Kerberos: the simplified form published in the BAN paper
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents: 6400
diff changeset
    21
	and also the full protocol (Kerberos IV)
6400
1f495d4d922b added new theory Yahalom_Bad
paulson
parents: 4594
diff changeset
    22
1f495d4d922b added new theory Yahalom_Bad
paulson
parents: 4594
diff changeset
    23
<LI>three versions of the Yahalom protocol, including a bad one that 
1f495d4d922b added new theory Yahalom_Bad
paulson
parents: 4594
diff changeset
    24
	illustrates the purpose of the Oops rule
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    25
4594
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    26
<LI>a novel recursive authentication protocol 
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    27
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    28
<LI>the Internet protocol TLS
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    29
</UL>
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
<HR>
13508
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
    32
<P>Last modified 20 August 2002
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    33
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    34
<ADDRESS>
13508
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
    35
<A
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
    36
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 6452
diff changeset
    37
<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
    38
</ADDRESS>
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    39
</BODY></HTML>