Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/README.html
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3119 bb2ee88aa43f
child 4594 f8d4387b40d9
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
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
 












bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




     4


<H2>Auth--The 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













bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




     8


HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.dvi.gz">new













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 Otway-Rees protocol













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


<LI>the Needham-Schroeder protocol (<A













bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




    16


HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR413-lcp-Mechanized-Proofs-of-Security-Protocols-Needham-Schroeder-with-Public-Keys.dvi.gz">public-key</A>













bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




    17


and shared-key versions)













bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




    18














bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




    19


<LI>two versions of the Yahalom protocol













bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




    20














bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




    21


<LI>a novel <A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz">recursive</A> authentication protocol 













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>













bb2ee88aa43f
Description of the Auth directory: security protocols proofs



paulson


parents: 

diff
changeset




    25


<P>Last modified 7 May 1997













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>















isabelle