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 Information and Computation, 204:1195--1263, 2006. Conference version appeared 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
Conference version of Pattern-Matching Spi-Calculus Copyright © 2004 Kluwer Academic Press
Journal version of Pattern-Matching Last modified: Sun Sep 24 14:38:39 2006