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 Pi * as discussed in Clark and Jacob 6.3.10. * * The protocol (once we add message tags) is: * * A -> B : A * B -> A : Nb * A -> B : { msg3(Nb) }Kas * B -> S : { msg4(A, { msg3(Nb) }Kas) }Kbs * S -> B : { msg5(Nb) }Kbs * * The protocol is flawed since message 3 doesn't contain Bob's name, * and message 5 doesn't contain Alice's name. Note that their protocol * Pi3 only fixes one of these flaws. A fixed version is in wl.cry. * * 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));
// This type definition is not well-formed, because b is free.
type WLMsg3 (a : Host) = Struct (nonce : WLNonce (a, b)); type WLMsg4 = Struct (a : Host, b : Host, cText : CText);
// This type definition is not well-formed, because a is free.
type WLMsg5 (b : Host) = Struct (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 (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 (Bob, { msg4 (a, cText) }keyB); input socketS is ({ msg5 (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 (b : Host, cText : CText); establish KDC at KDCHost is (socketKDC : Socket); output socketKDC is (b); input socketKDC is ({ b, keyB : WLKey (b) }keyKDC); decrypt cText is ({ msg4 (a : Host, cText' : CText) }keyB); output socketKDC is (a); input socketKDC is ({ a, keyA : WLKey (a) }keyKDC); decrypt cText is ({ msg3 (nonce' : WLNonce (a, b)) }keyA); output socketB is ({ msg5 (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