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 version of the ISO 5-pass Authentication Protocol. * It's in Clark and Jacobs (1997) 6.3.9. * The original protocol, modified to include message tags, * stripping out the extraneous payload messages, * and correcting what appear to be some typos (e.g. Alice never sends * Bob her name, so Bob has no idea who contacted him): * * A -> B : A, Na * B -> S : A, Na, B, Nb1 * S -> B : { msg3b(A, Kab, Nb1) }Kbs, { msg3a(B, Kab, Na) }Kas * B -> A : { msg3a(B, Kab, Na) }Kas, { msg4(Na, Nb2) }Kab * A -> B : { msg5(Na, Nb2) }Kab * * This protocol is astoundingly similar to Carlsen's Secret Key * Initiator Protocol (in carlsen.cry). The only differences are * that msg4 includes Nb2, and that msg5 includes Na. * * We cannot verify this protocol, for the same reason as for * Carlsen's protocol -- Na is being used twice: * once to verify the freshness of Kab, and once to establish * that Bob has sent using Kab. We can verify a modified version, * where we split Na into two nonces, one for each role: * * A -> B : A, Na1, Na2 * B -> S : A, Na1, B, Nb1 * S -> B : { msg3b(A, Kab, Nb1) }Kbs, { msg3a(B, Kab, Na1) }Kas * B -> A : { msg3a(B, Kab, Na1) }Kas, { msg4(Na2, Nb2) }Kab * A -> B : { msg5(Na2, Nb2) }Kab * * Alan Jeffrey, v0.0.1 2001/03/10 */
/* * 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 initiator : Word; public responder : Word; public shares : Word; public with : Word; public for : Word; public and : Word; public generated : Word; public acknowledges : Word;
/* * The types of the nonce and keys. */
type ISO5SNonceA (a : Host, b : Host) = Nonce ( end ( responder b acknowledges initiator a ) ); type ISO5SNonceB (a : Host, b : Host) = Nonce ( end ( initiator a acknowledges responder b ) ); type ISO5SMsg4 (a : Host, b : Host) = Struct ( nonceA2' : ISO5SNonceA (a, b), nonceB2 : Challenge ); type ISO5SMsg5 (a : Host, b : Host) = Struct ( nonceA2' : ISO5SNonceA (a, b), nonceB2' : ISO5SNonceB (a, b) ); type ISO5SMsg (a : Host, b : Host) = Union ( msg4 : ISO5SMsg4 (a, b), msg5 : ISO5SMsg5 (a, b) ); type ISO5SKey (a : Host, b : Host) = Key (ISO5SMsg (a, b)); type ISO5NonceA (a : Host, b : Host, sKey : ISO5SKey (a, b)) = Nonce ( end ( Sam generated sKey for initiator a and responder b ) ); type ISO5NonceB (a : Host, b : Host, sKey : ISO5SKey (a, b)) = Nonce ( end ( Sam generated sKey for responder b and initiator a ) ); type ISO5Msg3a (a : Host) = Struct ( b : Host, sKey : ISO5SKey (a, b), nonceA1' : ISO5NonceA (a, b, sKey) ); type ISO5Msg3b (b : Host) = Struct ( a : Host, sKey : ISO5SKey (a, b), nonceB1' : ISO5NonceB (a, b, sKey) ); type ISO5Msg (h : Host) = Union ( msg3a : ISO5Msg3a (h), msg3b : ISO5Msg3b (h) ); type ISO5Key (h : Host) = Key (ISO5Msg (h));
/* * Types used for the server's dialogue with the KDC. */
type ISO5KDCMsg = Struct (h : Host, keyH : ISO5Key (h)); type ISO5KDCKey = Key (ISO5KDCMsg);
/* * The shared keys. */
private keyA : ISO5Key (Alice); private keyB : ISO5Key (Bob); private keyKDC : ISO5KDCKey;
/* * The initiator. */
client Initiator at Alice is { new (nonceA1 : Challenge); new (nonceA2 : Challenge); establish Responder at Bob is (socket : Socket); output socket is (Alice, nonceA1, nonceA2); input socket is ( { msg3a ( Bob, sKey : ISO5SKey (Alice, Bob), nonceA1' : ISO5NonceA (Alice, Bob, sKey) ) }keyA, ticket : Un ); decrypt ticket is ( { msg4 ( nonceA2' : ISO5SNonceA (Alice, Bob), nonceB2 : Challenge ) }sKey ); check nonceA1 is nonceA1'; check nonceA2 is nonceA2'; end (Sam generated sKey for initiator Alice and responder Bob); begin (initiator Alice acknowledges responder Bob); cast nonceB2 is (nonceB2' : ISO5SNonceB (Alice, Bob) ); output socket is ( { msg5 ( nonceA2', nonceB2' ) }sKey ); end (responder Bob acknowledges initiator Alice); }
/* * The responder. */
server Responder at Bob is (socketA : Socket) { establish Intermediary at Sam is (socketS : Socket); new (nonceB1 : Challenge); new (nonceB2 : Challenge); input socketA is (a : Host, nonceA1 : Challenge, nonceA2 : Challenge); output socketS is (a, nonceA1, Bob, nonceB1); input socketS is ( { msg3b ( a, sKey : ISO5SKey (a, Bob), nonceB1' : ISO5NonceB (a, Bob, sKey) ) }keyB, ticket : Un); check nonceB1 is nonceB1'; end (Sam generated sKey for responder Bob and initiator a); begin (responder Bob acknowledges initiator a); cast nonceA2 is (nonceA2' : ISO5SNonceA (a, Bob) ); output socketA is ( ticket, { msg4 ( nonceA2', nonceB2 ) }sKey ); input socketA is ( { msg5 ( nonceA2', nonceB2' : ISO5SNonceB (a, Bob) ) }sKey ); check nonceB2 is nonceB2'; end (initiator a acknowledges responder Bob); }
/* * The intermediary. */
server Intermediary at Sam is (socketB : Socket) { input socketB is (a : Host, nonceA1 : Challenge, b : Host, nonceB1 : Challenge); establish KDC at KDCHost is (socketKDC : Socket); output socketKDC is (a); input socketKDC is ({ a, keyA : ISO5Key (a) }keyKDC); output socketKDC is (b); input socketKDC is ({ b, keyB : ISO5Key (b) }keyKDC); new (sKey : ISO5SKey (a, b)); begin (Sam generated sKey for initiator a and responder b); begin (Sam generated sKey for responder b and initiator a); cast nonceA1 is (nonceA1' : ISO5NonceA (a, b, sKey)); cast nonceB1 is (nonceB1' : ISO5NonceB (a, b, sKey)); output socketB is ( { msg3b ( a, sKey, nonceB1' ) }keyB, { msg3a ( b, sKey, nonceA1' ) }keyA ); }
/* * 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