src/HOL/Auth/Guard/README.html
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 51404 90a598019aeb
permissions -rw-r--r--
prefer symbols;
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <HTML>
     4 
     5 <HEAD>
     6   <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
     7   <TITLE>HOL/Auth/Guard/README.html</TITLE>
     8 </HEAD>
     9 
    10 <BODY>
    11 
    12 <H1>Protocol-Independent Secrecy Results</H1>
    13 
    14 date: april 2002
    15 author: Frederic Blanqui
    16 email: blanqui@lri.fr
    17 webpage: 
    18 
    19 <P>The current development is built above the HOL (Higher-Order Logic)
    20 Isabelle theory and the formalization of protocols introduced by <A
    21 HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>.  More details are
    22 in his paper <A
    23 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Auth/jcs.pdf">
    24 The Inductive approach
    25 to verifying cryptographic protocols</A> (J. Computer Security 6, pages
    26 85-128, 1998).
    27 
    28 <P>
    29 This directory contains a number of files:
    30 
    31 <UL>
    32 <LI>Extensions.thy contains extensions of Larry Paulson's files with many useful
    33 lemmas.
    34 
    35 <LI>Analz contains an important theorem about the decomposition of analz
    36 between pparts (pairs) and kparts (messages that are not pairs).
    37 
    38 <LI>Guard contains the protocol-independent secrecy theorem for nonces.
    39 <LI>GuardK is the same for keys.
    40 <LI>Guard_Public extends Guard and GuardK for public-key protocols.
    41 <LI>Guard_Shared extends Guard and GuardK for symmetric-key protocols.
    42 
    43 <LI>List_Msg contains definitions on lists (inside messages).
    44 
    45 <LI>P1 contains the definition of the protocol P1 and the proof of its
    46 properties (strong forward integrity, insertion resilience, truncation
    47 resilience, data confidentiality and non-repudiability)
    48 
    49 <LI>P2 is the same for the protocol P2
    50 
    51 <LI>NS_Public is for Needham-Schroeder-Lowe
    52 <LI>OtwayRees is for Otway-Rees
    53 <LI>Yahalom is for Yahalom
    54 
    55 <LI>Proto contains a more precise formalization of protocols with rules
    56 and a protocol-independent theorem for proving guardness from a preservation
    57 property. It also contains the proofs for Needham-Schroeder as an example.
    58 </UL>
    59 
    60 <HR>
    61 <P>Last modified 20 August 2002
    62 
    63 <ADDRESS>
    64 <A HREF="http://www.lri.fr/~blanqui/">Frederic Blanqui</A>,
    65 <A HREF="mailto:blanqui@lri.fr">blanqui@lri.fr</A>
    66 </ADDRESS>
    67 </BODY>
    68 </HTML>