Seminar, 27th February 2001
- Speaker:
- Joshua Guttman, the Mitre Corporation
- Date:
- Tuesday 27th February 2001 at 16:15
- Place:
-
Room TP4, Computer Laboratory
- Title:
- CRYPTOGRAPHIC PROTOCOL ANALYSIS VIA STRAND SPACES
Strand spaces are a Dolev-Yao style model of cryptographic protocol
execution. They are intended to retain the minimal information
compatible with the goal of providing reliable proofs of
authentication and secrecy properties where they hold, and
counterexamples where they do not. Strand spaces have been used as
the basis for numerous results, by our group and others:
1. "Authentication tests" easily establish authentication results,
and provide an excellent heuristic for protocol design;
2. "Honest ideals" may be used for confidentiality;
3. These methods are the basis of an automated protocol generator
[Perrig/Song];
4. A general theorem establishes when protocols may be used in
combination, without undermining any security goal the protocols
achieve when used separately;
5. Strand spaces justify a particular tagging discipline for protocol
implementations, preventing type flaw attacks
[Heather/Lowe/Schneider];
6. For a class of protocols, there is a syntactic bound on how many
regular principal sessions a penetrator might need for an attack
[Stoller].
In this talk, we will describe the strand space theory. We focus on
the methods used to show items 1 and 4 above, also illustrating how
those results can be used as a protocol design heuristic.
Seminar, 27th February 2001 /
Ross.Anderson@cl.cam.ac.uk
Last updated: 31st January 2001