Mercurial Mercurial > repos > isabelle / file revision
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/Guard/README.html
author wenzelm
Tue, 30 Sep 2008 14:19:26 +0200
changeset 28425 25d6099179a6
parent 15582 7219facb3fd0
child 51404 90a598019aeb
permissions -rw-r--r--
export setmp_thread_position; commit_exit: position; added plain command execution; simplified command_excursion, eliminated old (present_)excursion;

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

<!-- $Id$ -->

<HTML>

<HEAD>
  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
  <TITLE>HOL/Auth/Guard/README.html</TITLE>
</HEAD>

<BODY>

<H1>Protocol-Independent Secrecy Results</H1>

date: april 2002
author: Frederic Blanqui
email: blanqui@lri.fr
webpage: 

<P>The current development is built above the HOL (Higher-Order Logic)
Isabelle theory and the formalization of protocols introduced by <A
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>.  More details are
in his paper <A
HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Auth/jcs.pdf">
The Inductive approach
to verifying cryptographic protocols</A> (J. Computer Security 6, pages
85-128, 1998).

<P>
This directory contains a number of files:

<UL>
<LI>Extensions.thy contains extensions of Larry Paulson's files with many useful
lemmas.

<LI>Analz contains an important theorem about the decomposition of analz
between pparts (pairs) and kparts (messages that are not pairs).

<LI>Guard contains the protocol-independent secrecy theorem for nonces.
<LI>GuardK is the same for keys.
<LI>Guard_Public extends Guard and GuardK for public-key protocols.
<LI>Guard_Shared extends Guard and GuardK for symmetric-key protocols.

<LI>List_Msg contains definitions on lists (inside messages).

<LI>P1 contains the definition of the protocol P1 and the proof of its
properties (strong forward integrity, insertion resilience, truncation
resilience, data confidentiality and non-repudiability)

<LI>P2 is the same for the protocol P2

<LI>NS_Public is for Needham-Schroeder-Lowe
<LI>OtwayRees is for Otway-Rees
<LI>Yahalom is for Yahalom

<LI>Proto contains a more precise formalization of protocols with rules
and a protocol-independent theorem for proving guardness from a preservation
property. It also contains the proofs for Needham-Schroeder as an example.
</UL>

<HR>
<P>Last modified 20 August 2002

<ADDRESS>
<A HREF="http://www.lri.fr/~blanqui/">Frederic Blanqui</A>,
<A HREF="mailto:blanqui@lri.fr">blanqui@lri.fr</A>
</ADDRESS>
</BODY>
</HTML>
isabelle