# HG changeset patch # User paulson # Date 1052735210 -7200 # Node ID f7382ee9b5745af28da4ab0527ac6390df81df2e # Parent 740788f3f6b787b177e810d79a7ec4da0a75dd88 updated text diff -r 740788f3f6b7 -r f7382ee9b574 src/HOL/Auth/README.html --- a/src/HOL/Auth/README.html Mon May 12 12:12:19 2003 +0200 +++ b/src/HOL/Auth/README.html Mon May 12 12:26:50 2003 +0200 @@ -1,21 +1,23 @@ - HOL/Auth/README

Auth--The Inductive Approach to Verifying Security Protocols

Cryptographic protocols are of major importance, especially with the -growing use of the Internet. This directory demonstrates a new proof method, -which is described in various papers. The operational semantics of protocol participants is defined -inductively. +inductively.

This directory contains proofs concerning

three versions of the Otway-Rees protocol -
the Needham-Schroeder protocol (public-key and shared-key versions) +
the Needham-Schroeder shared-key protocol + +
the Needham-Schroeder public-key protocol (original and with Lowe's +modification)
two versions of Kerberos: the simplified form published in the BAN paper and also the full protocol (Kerberos IV) @@ -26,10 +28,15 @@
a novel recursive authentication protocol
the Internet protocol TLS + +
The certified e-mail protocol of Abadi et al.

Subdirectory Guard develops a theory of guardedness, by +Frederic Blanqui, and includes proofs of some roving agent protocols. +

Last modified 20 August 2002 +

Last modified $Date$