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 protocol is the result of Needham and Schroeder's fix to the original * Needham-Schroeder protocol to avoid the key compromise attack. The * original Needham-Schroeder protocol is in ns.cry. * * The protocol allows the server S to generate a session key Kab for use * by A and B. * * A -> B : A * B -> A : { msg2 (A, Nb0) }Kbs * A -> S : A, B, Na, { msg2 (A, Nb0) }Kbs * S -> A : { msg4 (Na, B, Kab, { msg5 (Kab, Nb0, A) }Kbs) }Kas * A -> B : { msg5 (Kab, Nb0, A) }Kbs * B -> A : { msg6 (Nb1) }Kab * A -> B : { msg7 (Nb1) }Kab * * Alan Jeffrey, v0.0.2 2001/02/26 * Christian Haack, modified for v1.1.0 2004/09/14 * */
/* * Include the standard prelude */
import prelude; public providing : Word; public session : Word; public key : Word; public to : Word; public for : Word; public acknowledging : Word; public reception : Word; public of : Word;
/* * Nonce types. */
type Challenge = PoshChall (); type ResponseSToA ( a:Un, b:Un, s:Server, kab:SharedKey(a,b,kab) ) = PoshResp ( begun(s providing session key kab to a for b) ); type ResponseSToB ( a:Un, b:Un, s:Server, kab:SharedKey(a,b,kab) ) = PoshResp ( begun(s providing session key kab to b for a) ); type ResponseAToB ( a:Host, b:Host, kab:SharedKey(a,b,kab) ) = PoshResp ( begun(a acknowledging reception of kab to b) );
/* * Message patterns. */
pattern Msg2 = (Un,Challenge); pattern Msg4 ( a:Un, s:Server, kas:SharedKey(a,s,kas) ) = ( nonceA : ResponseSToA(a,b,s,kab), b : Un, kab : SharedKey(a,b,kab), ticket : Public ); pattern Msg5 ( b:Un, s:Server, kbs:SharedKey(b,s,kbs) ) = ( kab : SharedKey(a,b,kab), nonceB0 : ResponseSToB(a,b,s,kab), a : Un ); pattern Msg6 ( a:Un, b:Host, kab:SharedKey(a,b,kab) ) = Challenge [ !begun(b acknowledging reception of kab to a) ]; pattern Msg7 ( a:Host, b:Host, kab:SharedKey(a,b,kab) ) = ResponseAToB(a,b,kab);
/* * Message tags. */
tag msg2 (Msg2) : Auth (b:Host, s:Host, kbs:SharedKey(b,s,kbs)); tag msg4 (Msg4(a,s,kas)) : Auth (a:Un, s:Host, kas:SharedKey(a,s,kas)); tag msg5 (Msg5(b,s,kbs)) : Auth (b:Un, s:Server, kbs:SharedKey(b,s,kbs)); tag msg6 (Msg6(a,b,kab)) : Auth (a:Un, b:Host, kab:SharedKey(a,b,kab)); tag msg7 (Msg7(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 a is (socketB : Socket); output socketB is a; input socketB is (request : Un); establish Intermediary at s is (socketS : Socket); new (nonceA : Challenge); output socketS is (a, b, nonceA, request); input socketS is { msg4(nonceA, b, kab:SharedKey(a,b,kab), ticket:Un) }kas [ begun(s providing session key kab to a for b) ]; end(s providing session key kab to a for b); output socketB is ticket; input socketB is { msg6(nonceB:Challenge) }kab [ !begun(b acknowledging reception of kab to a) ]; end(b acknowledging reception of kab to a); begin(a acknowledging reception of kab to b); output socketB is { msg7(nonceB) }kab; }
/* * The responder. */
server Responder (b:Host, s:Server, kbs:SharedKey(b,s,kbs)) at b is (socket : Socket) { input socket is (a:Un); new (nonceB0 : Challenge); output socket is { msg2(a,nonceB0) }kbs; input socket is { msg5(kab:SharedKey(a,b,kab), nonceB0, a) }kbs [ begun(s providing session key kab to b for a) ]; end (s providing session key kab to b for a); begin! (b acknowledging reception of kab to a); new (nonceB1 : Challenge); output socket is { msg6(nonceB1) }kab; input socket is { msg7(nonceB1) }kab [ begun(a acknowledging reception of kab to b) ]; end(a acknowledging reception of kab to b); }
/* * The intermediary. */
server Intermediary (s:Server) at s is (socket : Socket) { input socket is (a:Un,b:Un,nonceA:Challenge,ctext:Un); let kas:SharedKey(a,s,kas) = lkupKey (a,s); let kbs:SharedKey(b,s,kbs) = lkupKey (b,s); match ctext is { msg2 (a, nonceB0:Challenge) }kbs; new (kab : SharedKey(a,b,kab)); begin(s providing session key kab to a for b); begin(s providing session key kab to b for a); output socket is { msg4(nonceA, b, kab, { msg5(kab,nonceB0,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