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

/* * This is a simple mutual authentication protocol * where Alice and Bob authenticate themselves to each other. * This is the `ISO Symmetric Key Three-Pass Mutual Authentication' * protocol from Clark and Jacob (1997) with the non-secret messages * removed, and the messages reordered to deal with dependent records. * * B -> A : Nb * A -> B : { MsgA, B, Na, Nb }Kab // Note that B is redundant here * B -> A : { MsgB, Na, Nb }Kab // Note that Nb is redundant here * * Alan Jeffrey, v0.0.1 2001/02/22 */
/* * Include the standard prelude */
import oldprelude;
/* * This file declares a server Responder and a client Initiator. */
public Responder : Server; public Initiator : Client;
/* * Words used in the nonce */
public sent : Word; public for : Word;
/* * The types of the nonce and keys. */
type NonceA (msgB : Payload) = Nonce (end (Initiator for Bob sent msgB)); type NonceB (msgA : Payload) = Nonce (end (Responder for Alice sent msgA)); type Msg2 = Struct (msgA : Payload, b : Host, nonceA : Challenge, nonceB' : NonceB (msgA)); type Msg3 = Struct (msgB : Payload, nonceA' : NonceA (msgB), nonceB : Challenge); type MutualMsg = Union (msg2 : Msg2, msg3 : Msg3); type MutualKey = Key (MutualMsg);
/* * The key shared between Alice and Bob. */
private SKey : MutualKey;
/* * The responder. */
server Responder at Alice is (socket : Socket) { input socket is (nonceB : Challenge); new (msgA : Payload); new (nonceA : Challenge); begin (Responder for Alice sent msgA); cast nonceB is (nonceB' : NonceB (msgA)); output socket is ({ msg2 (msgA, Bob, nonceA, nonceB') }SKey); input socket is ({ msg3 (msgB : Payload, nonceA' : NonceA (msgB), nonceB) }SKey); check nonceA is nonceA'; end (Initiator for Bob sent msgB); }
/* * The initiator. */
client Initiator at Bob is { establish Responder at Alice is (socket : Socket); new (msgB : Payload); new (nonceB : Challenge); begin (Initiator for Bob sent msgB); output socket is (nonceB); input socket is ({ msg2(msgA : Payload, Bob, nonceA : Challenge, nonceB' : NonceB (msgA)) }SKey); check nonceB is nonceB'; cast nonceA is (nonceA' : NonceA (msgB)); output socket is ({ msg3(msgB, nonceA', nonceB) }SKey); end (Responder for Alice sent msgA); }
/* * 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