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

/* * The Abadi/Gordon Wide Mouthed Frog protocol. * This is a variant of the Wide Mouthed Frog protocol * with nonce challenges rather than timestamps. * In this failed version, we don't use tags, so we get a type error. * Alan Jeffrey, v0.0.1 2001/02/08 */
/* * 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 sending : Word; public key : Word;
/* * Types used in the protocol. */
type SKey = Key (Payload); type WMFNonce (a : Host, b : Host, sKey : SKey) = Nonce (end (a sending b key sKey)); type WMFMsg (a : Host) = Struct (b : Host, sKey : SKey, nonce : WMFNonce (a, b, sKey)); type WMFKey (h : Host) = Key (WMFMsg (h));
/* * Types used for the server's dialogue with the KDC. */
type WMFKDCMsg = Struct (h : Host, keyH : WMFKey (h)); type WMFKDCKey = Key (WMFKDCMsg);
/* * The shared keys. */
private keyA : WMFKey (Alice); private keyB : WMFKey (Bob); private keyKDC : WMFKDCKey;
/* * The initiator. */
client Initiator at Alice is { new (sKey : SKey); begin (Alice sending Bob key sKey); establish Intermediary at Sam is (socket : Socket); output socket is (Alice); input socket is (nonceA : Challenge); cast nonceA is (nonceA' : WMFNonce (Alice, Bob, sKey)); output socket is (Alice, { Bob, sKey, nonceA' }keyA); }
/* * The responder. */
server Responder at Bob is (socket : Socket) { new (nonceB : Challenge); output socket is (nonceB); input socket is ({ a : Host, sKey : SKey, nonceB' : WMFNonce (a, Bob, sKey) }keyB); check nonceB is nonceB'; end (a sending Bob key sKey); }
/* * The intermediary. */
server Intermediary at Sam is (socketA : Socket) { input socketA is (a : Host); establish KDC at KDCHost is (socketKDC : Socket); output socketKDC is (a); input socketKDC is ({ a, keyA : WMFKey (a) }keyKDC); new (nonceA : Challenge); output socketA is (nonceA); input socketA is (a, { b : Host, sKey : SKey, nonceA' : WMFNonce (a, b, sKey) }keyA); check nonceA is nonceA'; output socketKDC is (b); input socketKDC is ({ b, keyB : WMFKey (b) }keyKDC); establish Responder at b is (socketB : Socket); input socketB is (nonceB : Challenge); cast nonceB is (nonceB' : WMFNonce (a, b, sKey)); output socketB is ({ a, sKey, nonceB' }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