[Prev][Next][Index][Thread]
Cryptyc papers
We are pleased to announce the availability of the first two technical
reports from the Cryptyc project:
* A.D. Gordon and A.S.A. Jeffrey: Authenticity by Typing for
Security Protocols.
* A.D. Gordon and A.S.A. Jeffrey: Typing Correspondence Assertions
for Communication Protocols.
These papers use a type-and-effect system to statically verify
authenticity properties of communication protocols expressed in the
spi-calculus, and the pi-calculus respectively.
The papers are available from:
http://cryptyc.cs.depaul.edu/papers.html
http://research.microsoft.com/~adg/Publications/
A proof-of-concept implementation of the type system, together with its
use on a number of cryptographic protocols, is available at:
http://cryptyc.cs.depaul.edu/
The abstracts are attached.
Andrew D. Gordon and Alan Jeffrey
--
A.D. Gordon and A.S.A. Jeffrey: Authenticity by typing for security
protocols. Technical Report MSR-TR-2000-49, Microsoft Research,
conference version to appear in Proc. IEEE Computer Security Foundations
Workshop, 2001.
We propose a new method to check authenticity properties of
cryptographic protocols. First, code up the protocol in the spi-calculus
of Abadi and Gordon. Second, specify authenticity properties by
annotating the code with correspondence assertions in the style of Woo
and Lam. Third, figure out types for the keys, nonces, and messages of
the protocol. Fourth, check that the spi-calculus code is well-typed
according to a novel type and effect system presented in this paper. Our
main theorem guarantees that any well-typed protocol is robustly safe,
that is, its correspondence assertions are true in the presence of any
opponent expressible in spi. It is feasible to apply this method by hand
to several well-known cryptographic protocols. It requires little human
effort per protocol, puts no bound on the size of the opponent, and
requires no state space enumeration. Moreover, the types for protocol
data provide some intuitive explanation of how the protocol works. This
paper describes our method and gives some simple examples. Our method
has led us to the independent rediscovery of flaws in existing protocols
and to the design of improved protocols.
--
A.D. Gordon and A.S.A. Jeffrey: Typing correspondence assertions for
communication protocols. Technical Report MSR-TR-2000-48, Microsoft
Research, conference version to appear in Proc. Mathematical Foundations
of Programming Semantics, 2001.
Woo and Lam propose correspondence assertions for specifying
authenticity properties of security protocols. The only prior work on
checking correspondence assertions depends on model-checking and is
limited to finite-state systems. We propose a dependent type and effect
system for checking correspondence assertions. Since it is based on
type-checking, our method is not limited to finite-state systems. This
paper presents our system in the simple and general setting of the
pi-calculus. We show how to type-check correctness properties of example
communication protocols based on secure channels.