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 variant of the Yahalom Protocol, using message tags to * secure against type flaw attacks. 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) is: * * A -> B : A, Na * B -> S : B, { msg2 (A, Na, Nb) }Kbs * S -> A : { msg3(B, Kab, Na, Nb) }Kas, { msg4a(A, Kab) }Kbs * A -> B : { msg4a(A, Kab) }Kbs, { msg4b(Nb) }Kab * * This protocol has been proven correct (for instance, by Guttman in the * strand space model, and by Paulson), even in the presence of key * compromise. Whether this correct protocol type-checks, depends on the * how we write the correspondence specifications. * * If we require the correspondence "providing Kab to B for A" to end * before message 4b gets decrypted, then the protocol does not type-check. * Ending the correspondence at this point guarantees that the decryption * key for 4b is new. * * On the other hand, if we require the correspondence to end after * message 4b has been decrypted, then the protocol type-checks. However, * in this case, Kab is used to decrypt message 4b, although at this point our * specifications do not guarantee that Kab is new. * * Compare this discussion to the discussion of the Needham-Schroder * protocol in ns.cry. * * Interestingly, the Yahalom protocol is safe even against key compromise. * * See yahalom-modified.cry for a modification of Yahalom that type-checks, * even if we end the correspondence for Kab before using Kab. * * Note that this protocol doesn't obey the usual client-server discipline: * we have a cycle where Alice contacts Bob, who contacts Sam, who contacts * Alice again. When Sam contacts Alice, he needs to do it using the same * connection as Bob, which means Bob has to pass the socket connection on * to Sam. * * Alan Jeffrey, v0.0.2 2001/02/26 * Christian Haack, modified, 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;
/* * Nonce types. */
type Challenge = PoshChall (); type ResponseBToA (a:Any, b:Any, na:Any) = PoshResp ( begun(b acknowledging reception of na to a) ); type ResponseSToA (a:Any, b:Any, kab:SharedKey(a,b,kab), na:Any) = PoshResp ( begun(providing kab to a for b), begun(providing kab to b for a), begun(b acknowledging reception of na to a) ); type ResponseSToB (a:Any, b:Any, kab:SharedKey(a,b,kab)) = PoshResp ( begun(providing kab to b for a), begun(a acknowledging reception of kab to b) );
/* * Message patterns. */
pattern Msg2 (b:Host) = ( a:Un, nonceA:ResponseBToA(a,b,nonceA), Challenge ); pattern Msg3 (a:Un) = ( b : Un, kab : SharedKey(a,b,kab), nonceA : ResponseSToA(a,b,kab,nonceA), Challenge ); pattern Msg4a (b:Un) = ( a:Un, kab:SharedKey(a,b,kab) ); pattern Msg4b (a:Host, b:Host, kab:SharedKey(a,b,kab)) = ( nonceB : ResponseSToB(a,b,kab) );
/* * Message tags. */
tag msg2(Msg2(b)) : Auth(b:Host, s:Server, kbs:SharedKey(b,s,kbs)); tag msg3(Msg3(a)) : Auth(a:Un, s:Server, kas:SharedKey(a,s,kas)); tag msg4a(Msg4a(b)) : Auth(b:Un, s:Server, kbs:SharedKey(b,s,kbs)); tag msg4b(Msg4b(a,b,kab)) : Auth(a:Host, b:Host, kab:SharedKey(a,b,kab));
/* * We assume that two principals are able to securely lookup their shared * longterm keys. We formally express this by assuming the existence * of a secure lookup function of the following dependent function type: */
fun lkupKey (p:Any,q:Any) : (k:SharedKey(p,q,k));
/* * The initiator. */
client Initiator (a:Host, b:Host, s:Server, kas:SharedKey(a,s,kas)) at a is { establish Responder at b is (socket : Socket); new (nonceA : Challenge); output socket is (a, nonceA);
// This next message is meant to come from Sam, even
// though the socket was opened as going to Bob.
input socket is ( { msg3 (b, kab:SharedKey(a,b,kab), nonceA, nonceB:Challenge) }kas, ticket : Un ) [ begun(providing kab to a for b), begun(providing kab to b for a), begun(b acknowledging reception of nonceA to a) ]; end (providing kab to a for b); end (b acknowledging reception of nonceA to a); begin (a acknowledging reception of kab to b);
// Next we're back to sending to Bob on this socket.
output socket is (ticket, { msg4b(nonceB) }kab ); }
/* * The responder. */
server Responder (b:Host, s:Server, kbs:SharedKey(b,s,kbs)) at b is (socketA : Socket) { input socketA is (a : Un, nonceA : Challenge); establish Intermediary at s is (socketS : Socket); new (nonceB : Challenge); begin (b acknowledging reception of nonceA 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, { msg2 (a, nonceA, nonceB) }kbs, socketA);
// The next message should come from Alice.
input socketA is ( { msg4a (a, kab:SharedKey(a,b,kab)) }kbs, ctext : Un ); end (providing kab to b for a); // LINE END1 match ctext is { msg4b(nonceB) }kab; // LINE DECRYPT //end (providing kab to b for a); // LINE END2 end (a acknowledging reception of kab to b);
// If we comment out LINE END1 and instead insert LINE END2, then the
// protocol type-checks. However, that change is "unsafe" because, then,
// in LINE DECRYPT we use decryption key kab, although the correspondence
// assertions do not tell us that kab is new.
//
// This protocol happens to be safe, even in the presence of possible
// key compromise, but that requires an additional argument, which is not
// a consequence of type safety.
}
/* * The intermediary. */
server Intermediary (s:Server) at s is (socketB : Socket) { input socketB is (b:Un, request:Un, socketA:Socket); let kbs:SharedKey(b,s,kbs) = lkupKey (b,s); match request is { msg2 ( a:Un, nonceA:ResponseBToA(a,b,nonceA), nonceB:Challenge ) }kbs; let kas:SharedKey(a,s,kas) = lkupKey (a,s); new (kab : SharedKey(a,b,kab)); begin (providing kab to a for b); begin (providing kab to b for a); output socketA is ( { msg3 (b, kab, nonceA, nonceB) }kas, { msg4a (a, kab) }kbs ); }
/* * 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:52