author wenzelm
Wed, 20 Jan 2021 22:20:26 +0100
changeset 73140 68f0bd0c8e87
parent 51404 90a598019aeb
permissions -rw-r--r--
more informative error; tuned;

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "">


  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">


<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>

<P>Cryptographic protocols are of major importance, especially with the
growing use of the Internet.  This directory demonstrates the ``inductive
method'' of protocol verification, which is described in <A
papers</A>.  The operational semantics of protocol participants is defined

<P>This directory contains proofs concerning

<LI>three versions of the Otway-Rees protocol

<LI>the Needham-Schroeder shared-key protocol

<LI>the Needham-Schroeder public-key protocol (original and with Lowe's

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

<LI>three versions of the Yahalom protocol, including a bad one that 
	illustrates the purpose of the Oops rule

<LI>a novel recursive authentication protocol 

<LI>the Internet protocol TLS

<LI>The certified e-mail protocol of Abadi et al.

<P>Frederic Blanqui has contributed a theory of guardedness, which is
demonstrated by proofs of some roving agent protocols.

HREF="">Larry Paulson</A>,
<A HREF=""></A>