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 Woo and Lam's Mutual Authentication Protocol. * The protocol allows * the server S to generate a session key Kab for use by A and B. * The protocol (once we add message tags, and reorder the messages * to fit the requirements of dependent records, and add A and Bs * names to message 4) is: * * A -> B : A, Na * B -> A : B, Nb * A -> B : { msg3 (A, B, Na, Nb) }Kas * B -> S : A, B, { msg3 (A, B, Na, Nb) }Kas, { msg4 (A, B, Na, Nb) }Kbs * S -> B : { msg5a (B, Kab, Na, Nb) }Kas, { msg5b (A, Kab, Na, Nb) }Kbs * B -> A : { msg5a (B, Kab, Na, Nb) }Kas, { msg6 (Na, Nb) }Kab * A -> B : { msg7 (Nb) }Kab * * This protocol can't be verified directly in Cryptyc, since the nonce * Na is being used for two different purposes: once as a nonce challenge * to Sam to verify the freshness of Kab, and once as a nonce challenge * to Bob to verify that Bob is authenticating to Alice. The same is * true of Nb. We have to split the nonces in their two roles: * * A -> B : A, Na1, Na2 * B -> A : B, Nb1, Nb2 * A -> B : { msg3 (A, B, Na1, Nb1) }Kas * B -> S : A, B, { msg3 (A, B, Na1, Nb1) }Kas, { msg4 (A, B, Na1, Nb1) }Kbs * S -> B : { msg5a (B, Kab, Na1, Nb1) }Kas, { msg5b (A, Kab, Na1, Nb1) }Kbs * B -> A : { msg5a (B, Kab, Na1, Nb1) }Kas, { msg6 (Na2, Nb2) }Kab * A -> B : { msg7 (Nb2) }Kab * * Note that the type analysis here makes it obvious that messages 3 and * 4 do not need to be encrypted, and in fact messages 2 and 3 can be * elimiated all together). * * Alan Jeffrey, v0.0.1 2001/03/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 nonces */
public providing : Word; public contacting : Word; public contacted : Word; public session : Word; public key : Word; public with : Word; public by : Word; public to : Word; public for : Word;
/* * The types of the nonce and keys. */
type WLMANonceA2 (a : Host, b : Host) = Nonce ( end (b contacted by a) ); type WLMANonceB2 (a : Host, b : Host) = Nonce ( end (a contacting b) ); type WLMASMsg6 (a : Host, b : Host) = Struct ( nonceA2' : WLMANonceA2 (a, b), nonceB2 : Challenge ); type WLMASMsg7 (a : Host, b : Host) = WLMANonceB2 (a, b); type WLMASMsg (a : Host, b : Host) = Union ( msg6 : WLMASMsg6 (a, b), msg7 : WLMASMsg7 (a, b), msgP : Payload ); type WLMASKey (a : Host, b : Host) = Key ( WLMASMsg (a, b) ); type WLMANonceB1 (a : Host, b : Host, sKey : WLMASKey (a, b)) = Nonce ( end (Sam providing session key sKey to b for a) ); type WLMANonceA1 (a : Host, b : Host, sKey : WLMASKey (a, b)) = Nonce ( end (Sam providing session key sKey for a to b) );
// Note that this typing makes clear that the encryption of messages
// 3 and 4 is pointless: all the data in the messages is public.
type WLMAMsg3 (a : Host) = Struct ( a' : Host, b: Host, nonceA1 : Challenge, nonceB1 : Challenge ); type WLMAMsg4 (b : Host) = Struct ( a : Host, b': Host, nonceA1 : Challenge, nonceB1 : Challenge ); type WLMAMsg5a (a : Host) = Struct ( b : Host, sKey : WLMASKey (a, b), nonceA1' : WLMANonceA1 (a, b, sKey), nonceB1' : WLMANonceB1 (a, b, sKey) ); type WLMAMsg5b (b : Host) = Struct ( a : Host, sKey : WLMASKey (a, b), nonceA1' : WLMANonceA1 (a, b, sKey), nonceB1' : WLMANonceB1 (a, b, sKey) ); type WLMAMsg (h : Host) = Union ( msg3 : WLMAMsg3 (h), msg4 : WLMAMsg4 (h), msg5a : WLMAMsg5a (h), msg5b : WLMAMsg5b (h) ); type WLMAKey (h : Host) = Key (WLMAMsg (h));
/* * Types used for the server's dialogue with the KDC. */
type WLMAKDCMsg = Struct (h : Host, keyH : WLMAKey (h)); type WLMAKDCKey = Key (WLMAKDCMsg);
/* * The shared keys. */
private keyA : WLMAKey (Alice); private keyB : WLMAKey (Bob); private keyKDC : WLMAKDCKey;
/* * The initiator. */
client Initiator at Alice is { begin (Alice contacting Bob); establish Responder at Bob is (socketB : Socket); new (nonceA1 : Challenge); new (nonceA2 : Challenge); output socketB is (Alice, nonceA1, nonceA2); input socketB is (Alice, Bob, nonceB1 : Challenge, nonceB2 : Challenge); output socketB is ({ msg3 (Alice, Bob, nonceA1, nonceB1) }keyA); input socketB is ({ msg5a ( Bob, sKey : WLMASKey (Alice, Bob), nonceA1' : WLMANonceA1 (Alice, Bob, sKey), nonceB1' : WLMANonceB1 (Alice, Bob, sKey) ) }keyA, { msg6 ( nonceA2' : WLMANonceA2 (Alice, Bob), nonceB2 ) }sKey); cast nonceB2 is (nonceB2' : WLMANonceB2 (Alice, Bob)); output socketB is ( { msg7 (nonceB2') }sKey ); check nonceA1 is nonceA1'; check nonceA2 is nonceA2'; end (Bob contacted by Alice); end (Sam providing session key sKey for Alice to Bob); }
/* * The responder. */
server Responder at Bob is (socketA : Socket) { input socketA is (a : Host, nonceA1 : Challenge, nonceA2 : Challenge); begin (Bob contacted by a); new (nonceB1 : Challenge); new (nonceB2 : Challenge); output socketA is (Bob, nonceB1, nonceB2); input socketA is ( ctext3 : CText ); establish Intermediary at Sam is (socketS : Socket); output socketS is ( ctext3, { msg4 ( a, Bob, nonceA1, nonceB1 ) }keyB ); input socketS is ( ctext5a : CText, { msg5b ( a, sKey : WLMASKey (a, Bob), nonceA1' : WLMANonceA1 (a, Bob, sKey), nonceB1' : WLMANonceB1 (a, Bob, sKey) ) }keyB ); check nonceB1 is nonceB1'; cast nonceA2 is ( nonceA2' : WLMANonceA2 (a, Bob) ); output socketA is ( ctext5a, { msg6 ( nonceA2', nonceB2 ) }sKey ); input socketA is ( { msg7 ( nonceB2' : WLMANonceB2 (a, Bob) ) }sKey ); check nonceB2 is nonceB2'; end (a contacting Bob); end (Sam providing session key sKey to Bob for a); }
/* * The intermediary. */
server Intermediary at Sam is (socketB : Socket) { input socketB is ( a : Host, b : Host, ctext3 : CText, ctext4 : CText ); establish KDC at KDCHost is (socketKDC : Socket); output socketKDC is (a); input socketKDC is ({ a, keyA : WLMAKey (a) }keyKDC); output socketKDC is (b); input socketKDC is ({ b, keyB : WLMAKey (b) }keyKDC); decrypt ctext3 is ( { msg3 ( a, b, nonceA1 : Challenge, nonceB1 : Challenge ) }keyA ); decrypt ctext4 is ( { msg4 ( a, b, nonceA1, nonceB1 ) }keyB ); new (sKey : WLMASKey (a, b)); begin (Sam providing session key sKey for a to b); begin (Sam providing session key sKey to b for a); cast nonceA1 is (nonceA1' : WLMANonceA1 (a, b, sKey)); cast nonceB1 is (nonceB1' : WLMANonceB1 (a, b, sKey)); output socketB is ( { msg5a ( b, sKey, nonceA1', nonceB1' ) }keyA, { msg5b ( a, sKey, nonceA1', nonceB1' ) }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