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

/* * In their BAN logic article, Burrows, Abadi and Needham propose the * following modification of the Yahalom protocol. (See yahalom.cry for * the unmodified Yahalom.) As an advantage, they mention that this * protocol is easier to analyze because it does not use an uncertified * key. * * A -> B : A, Na * B -> S : B, Nb, { msg2 (A, Na) }Kbs * S -> A : Nb, { msg3(B, Kab, Na) }Kas, { msg4a(A, Kab, Nb) }Kbs * A -> B : { msg4a(A, Kab, Nb) }Kbs, { msg4b(Nb) }Kab * * The main difference to the original Yahalom protocol is that * the original does not include Nb in message 4a. Moreover, the * original includes Nb in the ciphertexts in messages 2 and 3. In the * modified version, this is no longer necessary. * * Alan Jeffrey, v0.0.2 2001/02/26 * Christian Haack, modified for v1.1.0, 2004/09/15 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public providing : Word; public acknowledging : Word; public reception : Word; public to : Word; public for : Word; public of : Word;
/* Challenge type. */
type Challenge = PoshChall ();
/* Response types for na. */
type ResponseBToA (a:Public, b:Public, na:Any) = PoshResp ( begun(b acknowledging reception of na to a) ); type ResponseSToA (a:Public, b:Public, s:Public, kab:SharedKey(a,b,kab), na:Any) = PoshResp ( begun(s providing kab to a for b), begun(b acknowledging reception of na to a) );
/* Response type for nb. */
type ResponseSToB (a:Public, b:Public, s:Public, kab:SharedKey(a,b,kab)) = PoshResp ( begun(s providing kab to b for a) );
/* Message patterns. */
pattern Msg2 (b:Public) = ( a:Public, nA:ResponseBToA(a,b,nA) ); pattern Msg3 (a:Public, s:Public) = ( b:Public, kab:SharedKey(a,b,kab), nA:ResponseSToA(a,b,s,kab,nA) ); pattern Msg4a (b:Public, s:Public) = ( a:Public, kab:SharedKey(a,b,kab), nB:ResponseSToB(a,b,s,kab) ); pattern Msg4b (a:Public, b:Public, kab:SharedKey(a,b,kab)) = Any [ !begun(a acknowledging reception of kab to b) ];
/* Message tags. */
tag msg2 (Msg2(b)) : Auth (b:Public, s:Public, kbs:SharedKey(b,s,kbs)); tag msg3 (Msg3(a,s)) : Auth (a:Public, s:Public, kas:SharedKey(a,s,kas)); tag msg4a (Msg4a(b,s)) : Auth (b:Public, s:Public, kbs:SharedKey(b,s,kbs)); tag msg4b (Msg4b(a,b,kab)) : Auth (a:Public, b:Public, kab:SharedKey(a,b,kab)); client Initiator (a:Public, b:Public, s:Public, kas:SharedKey(a,s,kas)) at a is { establish Responder at b is (socket : Socket); new (nA : Challenge); output socket is (a,nA);
// This next message is meant to come from Sam, even
// though the socket was opened as going to Bob.
input socket is ( nB : Challenge, { msg3(b, kab:SharedKey(a,b,kab), nA) }kas, ticketB:Un ) [ begun(s providing kab to a for b), begun(b acknowledging reception of nA to a) ]; end(s providing kab to a for b); end(b acknowledging reception of nA to a); begin!(a acknowledging reception of kab to b);
// Next we're back to sending to Bob on this socket.
output socket is (ticketB, { msg4b(nB) }kab ); } server Responder (a:Public, b:Public, s:Public, kbs:SharedKey(b,s,kbs)) at b is (socketA : Socket) { input socketA is (a, nA : Challenge); establish Intermediary at s is (socketS : Socket); new (nB : Challenge); begin (b acknowledging reception of nA to a);
// Note that in the next output we have to include the socket connection to
// Alice, otherwise Sam has no way to contact Alice.
output socketS is (b, nB, { msg2 (a, nA) }kbs, socketA);
// The next message should come from Alice.
input socketA is ( { msg4a(a, kab:SharedKey(a,b,kab), nB) }kbs, { msg4b(nB) }kab ) [ begun(s providing kab to b for a), !begun(a acknowledging reception of kab to b) ]; end(s providing kab to b for a); end(a acknowledging reception of kab to b); } server Intermediary (s:Public, a:Public, kas:SharedKey(a,s,kas), b:Public, kbs:SharedKey(b,s,kbs)) at s is (socketB : Socket) { input socketB is (b, nB:Challenge, { msg2(a, nA:ResponseBToA(a,b,nA)) }kbs, socketA:Socket); new (kab:SharedKey(a,b,kab)); begin(s providing kab to a for b); begin(s providing kab to b for a); output socketA is ( { msg3(b,kab,nA) }kas, { msg4a(a,kab,nB) }kbs ); }

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: 2006-02-20 06:31:11