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 Needham-Schroeder Symmetric Key Protocol, * using message tags rather than nonce arithmetic. 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 -> S : A, B, Na * S -> A : { msg2(Na, B, Kab, { msg3(Kab, A) }Kbs) }Kas * A -> B : { msg3(Kab, A) }Kbs * B -> A : { msg4(Nb) }Kab * A -> B : { msg5(Nb) }Kab * * This protocol is flawed if one takes into account the possibility * of key compromise (see for example Clark and Jacob, 1997): * Message 3 is vulnerable to replay. As a result, an attacker * can impersonate A and trick B into accepting a compromised key. * * On the other hand, under the idealistic assumption that keys can't * be compromised, this protocol is safe. * * Whether this 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 4, then the protocol does not type-check. Ending the * correspondence at this point guarantees that the key for encrypting * and decrypting messages 4 and 5 is new. * * On the other hand, if we require the correspondence to end after * message 5, then the protocol type-checks. However, in this case, Kab is * used to encrypt and decrypt messages 4 and 5, although at this point our * specifications do not guarantee that Kab is new. * * A fix for the key-compromise attack, as proposed by Needham and Schroeder, * is presented in ns-modified.cry. * * Alan Jeffrey, v0.0.2 2001/02/25 * Christian Haack, modified for v.1.1.0 2004/09/13 */
/* * Include the standard prelude */
import prelude; public providing : Word; public session : Word; public key : Word; public to : Word; public for : Word;
/* * Nonce types. */
type Challenge = PoshChall (); type ResponseSToA ( a:Un, b:Un, kab:SharedKey(a,b,kab) ) = PoshResp ( begun(providing session key kab to a for b), begun(providing session key kab to b for a) ); type ResponseAToB ( a:Host, b:Host, kab:SharedKey(a,b,kab) ) = PoshResp ( begun(providing session key kab to b for a) );
/* * Message patterns. */
pattern Msg2 ( a:Un, s:Server, kas:SharedKey(a,s,kas) ) = ( nonceA : ResponseSToA(a,b,kab), b : Un, kab : SharedKey(a,b,kab), ticket : Un ); pattern Msg3 ( b:Un, s:Server, kbs:SharedKey(b,s,kbs) ) = ( kab : SharedKey(a,b,kab), a : Un ); pattern Msg4 ( a:Un, b:Host, kab:SharedKey(a,b,kab) ) = Challenge; pattern Msg5 ( a:Host, b:Host, kab:SharedKey(a,b,kab) ) = ResponseAToB(a,b,kab);
/* * Message tags. */
tag msg2(Msg2(a,s,kas)) : Auth(a:Un, s:Server, kas:SharedKey(a,s,kas)); tag msg3(Msg3(b,s,kbs)) : Auth(b:Un, s:Server, kbs:SharedKey(b,s,kbs)); tag msg4(Msg4(a,b,kab)) : Auth(a:Un, b:Host, kab:SharedKey(a,b,kab)); tag msg5(Msg5(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 Intermediary at s is (socketS : Socket); new (nonceA : Challenge); output socketS is (a, b, nonceA); input socketS is { msg2(nonceA, b, kab:SharedKey(a,b,kab), ticket:Un) }kas [ begun(providing session key kab to a for b), begun(providing session key kab to b for a) ]; end(providing session key kab to a for b); establish Responder at b is (socketB : Socket); output socketB is ticket; input socketB is { msg4 (nonceB:Challenge) }kab; output socketB is { msg5(nonceB) }kab; }
/* * The responder. */
server Responder (b:Host, s:Server, kbs:SharedKey(b,s,kbs)) at b is (socket : Socket) { input socket is { msg3(kab:SharedKey(a,b,kab), a:Un) }kbs; new (nonceB : Challenge); end (providing session key kab to b for a); // line b3 output socket is { msg4(nonceB) }kab; // line b4 input socket is { msg5(nonceB) }kab; // line b5 //end (providing session key kab to b for a); // line b6
// If we comment out line b3 and uncomment line b6, instead,
// then the protocol type-checks. But then our spec does not
// guarantee that key kab used in lines b4 and b5 is new.
}
/* * The intermediary. */
server Intermediary (s:Server) at s is (socket : Socket) { input socket is (a:Un, b:Un, nonceA:Challenge); let kas:SharedKey(a,s,kas) = lkupKey (a,s); let kbs:SharedKey(b,s,kbs) = lkupKey (b,s); new (kab : SharedKey(a,b,kab)); begin(providing session key kab to a for b); begin(providing session key kab to b for a); output socket is { msg2(nonceA, b, kab, { msg3(kab,a) }kbs) }kas; }
/* * 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