Introduction
Applet
Examples
Download
Research Papers
Changelog
To Do List
|
Research Papers
The typechecker is based on our work on dependent type-and-effect
systems for the spi-calculus.
A.D. Gordon and A.S.A. Jeffrey,
Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus
.
In Proc. of 16th Int. Conf. on Concurrency Theory (CONCUR),
August 2005
C. Haack and A.S.A. Jeffrey,
Timed Spi-Calculus with Types for Secrecy and Authenticity
.
In Proc. of 16th Int. Conf. on Concurrency Theory (CONCUR),
August 2005
C. Haack and A.S.A. Jeffrey,
Pattern-Matching Spi-Calculus
.
In Proc. of 2nd IFIP Workshop on Formal Aspects in Security and Trust (FAST), Vol. 173 of IFIP series, Kluwer Academic Press, August 2004
A.D. Gordon and A.S.A. Jeffrey,
Typing One-to-One
and One-to-Many Correspondences in Security Protocols.
In Proc. International Software Security Symposium, 2002.
A.D. Gordon and A.S.A. Jeffrey,
Types
and Effects for Asymmetric Cryptographic Protocols.
In J. Computer Security, 12 (3/4), 2004, pp. 435-484.
Conference version appeared in
Proc. IEEE Computer Security Foundations Workshop, 2002.
A.D. Gordon and A.S.A. Jeffrey,
Authenticity
by Typing for Security Protocols.
In J. Computer Security, 11 (4), 2003, pp. 451-521.
Conference version appeared in
Proc. IEEE Computer Security Foundations Workshop, 2001.
A.D. Gordon and A.S.A. Jeffrey,
Typing
Correspondence Assertions for Communication Protocols.
In Theoretical Computer Science, vol. 300, 2003,
pp. 379-409.
Conference version appeared in
Proc. Mathematical Foundations of Programming Semantics, 2001.
The surface syntax is slightly
different in the tool than in the papers, but otherwise the tool
is an implementation of the system described
in an extended version of Pattern-Matching Spi-Calculus,
which handles nonces and one-to-one correspondences similarly to
Types and Effects in Asymmetric Cryptographic Protocols.
Cryptyc implementation Copyright © 2001-2004, Alan Jeffrey and Christian Haack
Technical reports Copyright © 2000-2004 Microsoft Research,
Alan Jeffrey and Christian Haack
This material is partly based upon work supported by the National
Science Foundation under Grant No. 0208549.
Conference version of Authenticity by Typing for Security Protocols Copyright © 2001 IEEE
Conference version of Types and Effects for Asymmetric Cryptographic Protocols Copyright © 2002 IEEE
Journal version of Authenticity by Typing for Security Protocols Copyright © 2003 IOS Press
Journal version of Typing Correspondence Assertions for Communication Protocols Copyright © 2003 Elsevier
Journal version of Types and Effects for Asymmetric Cryptographic Protocols Copyright © 2004 IOS Press
Pattern-Matching Spi-Calculus Copyright © 2004 Kluwer Academic Press
Last modified: Mon Feb 20 14:22:52 2006
|