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 4-pass Authentication Protocol. * It's in Clark and Jacobs (1997) 6.3.8. * The original protocol, modified to include message tags, * stripping out the extraneous payload messages, * and correcting what appear to be some typos is: * * A -> S : A, B, Na * S -> A : { msg2(B, Kab, Na) }Kas, { msg3(A, Kab, Ns) }Kbs * A -> B : { msg3(A, Kab, Ns) }Kbs * B -> A : { msg4(A, Nb) }Kab * * We can use Cryptyc to verify Alice's half of this protocol, but * we can't verify Bob's half, because although Bob issues a nonce * challenge to Alice, Alice never responds! We can fix this by * adding a fifth message: * * A -> B : { msg5(Nb) }Kab * * but this still isn't enough to verify the protocol, since it suffers * from the same key compromise attack as Needham-Schroeder. The problem * is that Bob has no way to associate Alice's msg5 back to msg3 (where * he receives Sam's ticket authenticating Kab). We can fix this by * allowing Alice access to Ns. The resulting protocol is: * * A -> S : A, B, Na * S -> A : { msg2(B, Kab, Ns, Na) }Kas, { msg3(A, Kab, Ns) }Kbs * A -> B : { msg3(A, Kab, Ns) }Kbs * B -> A : { msg4(A, Nb) }Kab * A -> B : { msg5(Ns, Nb) }Kab * * Note that Alice never gets to issue a nonce challenge to Bob, so although * she knows that Sam generated the key for her and Bob, she doesn't know * that Bob actually got it. * * Alan Jeffrey, v0.0.1 2001/03/09 */
/* * 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 contacts : Word;
/* * The types of the nonce and keys. */
type ISO4NonceB (a : Host, b : Host, nonceS : Challenge) = Nonce ( end (initiator a contacts responder b), check (nonceS) ); type ISO4SMsg4 (a : Host, b : Host) = Struct ( a' : Host, nonceB : Challenge ); type ISO4SMsg5 (a : Host, b : Host) = Struct ( nonceS : Challenge, nonceB' : ISO4NonceB (a, b, nonceS) ); type ISO4SMsg (a : Host, b : Host) = Union ( msg4 : ISO4SMsg4 (a, b), msg5 : ISO4SMsg5 (a, b) ); type ISO4SKey (a : Host, b : Host) = Key (ISO4SMsg (a, b)); type ISO4NonceA (a : Host, b : Host, sKey : ISO4SKey (a, b), nonceS : Challenge) = Nonce (end (Sam generated sKey for initiator a and responder b), check (nonceS)); type ISO4NonceS (a : Host, b : Host, sKey : ISO4SKey (a, b)) = Nonce (end (Sam generated sKey for responder b and initiator a)); type ISO4Msg2 (a : Host) = Struct ( b : Host, sKey : ISO4SKey (a, b), nonceS : Challenge, nonceA' : ISO4NonceA (a, b, sKey, nonceS) ); type ISO4Msg3 (b : Host) = Struct ( a : Host, sKey : ISO4SKey (a, b), nonceS' : ISO4NonceS (a, b, sKey) ); type ISO4Msg (h : Host) = Union ( msg2 : ISO4Msg2 (h), msg3 : ISO4Msg3 (h) ); type ISO4Key (h : Host) = Key (ISO4Msg (h));
/* * Types used for the server's dialogue with the KDC. */
type ISO4KDCMsg = Struct (h : Host, keyH : ISO4Key (h)); type ISO4KDCKey = Key (ISO4KDCMsg);
/* * The shared keys. */
private keyA : ISO4Key (Alice); private keyB : ISO4Key (Bob); private keyKDC : ISO4KDCKey;
/* * The initiator. */
client Initiator at Alice is { new (nonceA : Challenge); establish Intermediary at Sam is (socketS : Socket); output socketS is (Alice, Bob, nonceA); input socketS is ( { msg2 ( Bob, sKey : ISO4SKey (Alice, Bob), nonceS : Challenge, nonceA' : ISO4NonceA (Alice, Bob, sKey, nonceS) ) }keyA, ticket : Un ); check nonceA is nonceA'; end (Sam generated sKey for initiator Alice and responder Bob); begin (initiator Alice contacts responder Bob); establish Responder at Bob is (socketB : Socket); output socketB is (ticket); input socketB is ( { msg4 ( Alice, nonceB : Challenge ) }sKey ); cast nonceB is (nonceB' : ISO4NonceB (Alice, Bob, nonceS)); output socketB is ( { msg5 ( nonceS, nonceB' ) }sKey );
// Note that Alice can't end the session with Bob here,
// since she doesn't get to issue a nonce challenge to Bob.
}
/* * The responder. */
server Responder at Bob is (socketA : Socket) { new (nonceB : Challenge); input socketA is ( { msg3 ( a : Host, sKey : ISO4SKey (a, Bob), nonceS' : ISO4NonceS (a, Bob, sKey) ) }keyB );
// Note that at this point we can't trust nonceS', because
// it could be a replay attack using an old ticket.
// We can't trust this message until later, once we issue
// a nonce challenge to a.
output socketA is ( { msg4 ( a, nonceB ) }sKey ); input socketA is ( { msg5 ( nonceS : Challenge, nonceB' : ISO4NonceB (a, Bob, nonceS) ) }sKey );
// Passing this nonce challenge allows us to trust nonceS:
check nonceB is nonceB';
// Passing this nonce challenge allows us to trust sKey:
check nonceS is nonceS'; end (Sam generated sKey for responder Bob and initiator a); end (initiator a contacts responder Bob); }
/* * The intermediary. */
server Intermediary at Sam is (socketA : Socket) { input socketA is (a : Host, b : Host, nonceA : Challenge); establish KDC at KDCHost is (socketKDC : Socket); output socketKDC is (a); input socketKDC is ({ a, keyA : ISO4Key (a) }keyKDC); output socketKDC is (b); input socketKDC is ({ b, keyB : ISO4Key (b) }keyKDC); new (nonceS : Challenge); new (sKey : ISO4SKey (a, b)); begin (Sam generated sKey for initiator a and responder b); begin (Sam generated sKey for responder b and initiator a); cast nonceA is (nonceA' : ISO4NonceA (a, b, sKey, nonceS)); cast nonceS is (nonceS' : ISO4NonceS (a, b, sKey)); output socketA is ( { msg2 ( b, sKey, nonceS, nonceA' ) }keyA, { msg3 ( a, sKey, nonceS' ) }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