Examples

You can either run the typechecker on the command line with:

  java -jar cryptyc.jar filename.cry

or you can run it as an applet.

A. Simple Introductory Examples

Sign-Then-Encrypt: In simple-sign-then-encrypt.cry.

Signed Digest: In simple-signed-digest.cry.

Public-Out-Signed Home (POSH) Nonce: In simple-posh-nonce.cry

Secret-Out-Public-Home (SOPH) Nonce: In simple-soph-nonce.cry.

B. Examples from the Clark/Jacob Survey

The following examples are taken from A Survey of Authentication Protocol Literature: Version 1.0 by John Clark and Jeremy Jacob, 1997. Some of the examples still contain depreciated forms from the previous Cryptyc version. In particular, some examples still use protocol-specific key types. We have type-checked all examples with the current type-checker and have updated a large subset to omit depreciated syntax, but we have not yet updated all examples.

6.1 Symmetric Key Protocols Without Trusted Third Parties

6.1.1 ISO Symmetric Key One-Pass Unilateral Authentication Protocol

Can't be typechecked, since it uses timestamps / sequence numbers.

6.1.2 ISO Symmetric Key Two-Pass Unilateral Authentication Protocol

In simple.cry.

6.1.3 ISO Symmetric Key Two-Pass Mutual Authentication

Can't be typechecked, since it uses timestamps / sequence numbers.

6.1.4 ISO Symmetric Key Three-Pass Mutual Authentication

In OLDmutual.cry (contains depreciated forms).

6.1.5 Using Non-Reversible Functions

In cj-6-1-5.cry.

6.1.6 Andrew Secure RPC Protocol

In andrewrpc-fail.cry (original broken version).

In andrewrpc.cry (version with obvious fix).

6.3 Symmetric Key Protocols Involving Trusted Third Parties

6.3.1 Needham Schroeder Protocol with Conventional Keys

In ns.cry.

6.3.2 Denning Sacco Protocol

Can't be typechecked, since it uses timestamps.

6.3.3 Otway-Rees Protocol

In or.cry

In or-simplified.cry (Abadi and Needham's simplified version).

6.3.4 Amended Needham Schroeder Protocol

In ns-modified.cry.

6.3.5 Wide Mouthed Frog Protocol

Can't be typechecked since it uses timestamps.

In OLDfail-wmf.cry (broken version using nonces rather than timestamps) (contains depreciated forms).

In OLDwmf.cry (fixed version) (contains depreciated forms).

6.3.6 Yahalom

In yahalom.cry.

In ban-yahalom.cry (Burrow, Abadi and Needham's modified version).

6.3.7 Carlsen's Secret Key Initiator Protocol

In carlsen.cry.

6.3.8 ISO 4-pass Authentication Protocol

In OLDiso4.cry (modified version) (contains depreciated forms).

6.3.9 ISO 5-pass Authentication Protocol

In OLDiso5.cry (slightly modified version) (contains depreciated forms).

6.3.10 Woo and Lam's Authentication Protocls

In OLDfail-wl.cry (broken version) (contains depreciated forms).

In OLDwl.cry (fixed version) (contains depreciated forms).

6.3.11 Woo and Lam's Mutual Authentication Protocl

In OLDwlma.cry (slightly modified version) (contains depreciated forms).

6.7 Public Key Protocols with Trusted Third Party

6.7.1 The Needham-Schroeder-Lowe Public Key Protocol

In ns-public-key-fail.cry (vulnerable to insider attack, does not typecheck).

In nsl-full.cry (Lowe's fix, 7-message version).

In nsl-optimized.cry (NSL, avoiding encryption of nonce responses).

In nsl-with-secret.cry (NSL extended by a secret).

In nsl-with-secret-optimized.cry (NSL with secret, avoiding encryption of the second nonce response).

C. More Examples with Signing and Hashing

Message Digest with Acknowledgment: In digest-with-ack.cry.

Accumulating Trust by Nested Signing: In nested-signing.cry.

Username Signing: In username-signing.cry.

A Version of a Signing Procedure from the X509 Recommendation: In X509-signing.cry.

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.
A Survey of Authentication Protocol Literature Copyright © 1997 John Clark and Jeremy Jacob
Last modified: Mon Feb 20 13:44:11 2006