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