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

/* * Woo and Lam's authentication protocol * (as modified by Abdadi and Needham, Anderson and Needham, and Gordon and Jeffrey). * The protocol (once we add message tags) is: * * A -> B : A * B -> A : Nb * A -> B : { msg3(B, Nb) }Kas * B -> S : A, B, { msg3(B, Nb) }Kas * S -> B : { msg5(A, Nb) }Kbs * * This improves on the original by: * * a) including Bob's name in msg3. * b) including Alice's name in msg5 * c) sending msg4 in plaintext rather than cyphertext. * * Alan Jeffrey, v0.0.2 2001/05/18 */
/* * Include the standard prelude */
import oldprelude;
/* * This file declares an initiator, a responder and an intermediary: */
public Initiator : Client; public Responder : Server; public Intermediary : Server;
/* * These make use of a Key Distribution Center (not defined here). */
public KDC : Server; public KDCHost : Host;
/* * Words used in the session name. */
public authenticates : Word; public to : Word;
/* * Types used in the protocol. */
type WLNonce (a : Host, b : Host) = Nonce (end (a authenticates to b)); type WLMsg3 (a : Host) = Struct (b : Host, nonce : WLNonce (a, b)); type WLMsg5 (b : Host) = Struct (a : Host, nonce : WLNonce (a, b)); type WLMsg (h : Host) = Union (msg3 : WLMsg3 (h), msg5 : WLMsg5 (h)); type WLKey (h : Host) = Key (WLMsg (h));
/* * Types used for the server's dialogue with the KDC. */
type WLKDCMsg = Struct (h : Host, keyH : WLKey (h)); type WLKDCKey = Key (WLKDCMsg);
/* * The shared keys. */
private keyA : WLKey (Alice); private keyB : WLKey (Bob); private keyKDC : WLKDCKey;
/* * The initiator. */
client Initiator at Alice is { begin (Alice authenticates to Bob); establish Responder at Bob is (socket : Socket); output socket is (Alice); input socket is (nonce : Challenge); cast nonce is (nonce' : WLNonce (Alice, Bob)); output socket is ({ msg3 (Bob, nonce') }keyA); }
/* * The responder. */
server Responder at Bob is (socketA : Socket) { input socketA is (a : Host); new (nonce : Challenge); output socketA is (nonce); input socketA is (cText : CText); establish Intermediary at Sam is (socketS : Socket); output socketS is (a, Bob, cText); input socketS is ({ msg5 (a, nonce' : WLNonce (a, Bob)) }keyB); check nonce is nonce'; end (a authenticates to Bob); }
/* * The intermediary. */
server Intermediary at Sam is (socketB : Socket) { input socketB is (a : Host, b : Host, cText : CText); establish KDC at KDCHost is (socketKDC : Socket); output socketKDC is (a); input socketKDC is ({ a, keyA : WLKey (a) }keyKDC); output socketKDC is (b); input socketKDC is ({ b, keyB : WLKey (b) }keyKDC); decrypt cText is ({ msg3 (b, nonce' : WLNonce (a, b)) }keyA); output socketB is ({ msg5 (a, nonce') }keyB); }
/* * That's all folks. */

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: 2005-12-14 06:33:53