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