Andrew D. Gordon
Microsoft Research

Christian Haack
Radboud University

Alan Jeffrey
Bell Labs

Cryptographic Protocol Type Checker

Introduction

Applet

Examples

Download

Research Papers

Changelog

To Do List

To-do list

Bugs

Currently no known bugs.

Implementation enhancements

Better error messages.

Provide a syntax for opponents (this is just a matter of allowing opponents to hijack sessions).

Allow networks to be executed, to produce message-passing diagrams.

Add a LaTeX / HTML pretty printer.

Language enhancements

Extend the checker to distinguish between short- and long-term keys and deal with key compromise (as described in our CONCUR'05 papers).

Find a way to allow a single nonce to be used multiple times within the same protocol, if confusion is ruled out by the message context. This would allow us to obtain a one-to-one correspondence for the acknowledgment in Carlsen.

Coding issues

Add proper Javadoc comments.

Examples

Update remaining examples from Cryptyc 1.1 to Cryptyc 1.2 and protocol-independent key types.

Look at examples with key compromise.

Documentation

Document the Cryptyc surface syntax properly.

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.
Last modified: Mon Feb 20 14:28:46 2006