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 Andrew Secure RPC Protocol * from Clark and Jacob (1997), using message tags rather * than nonce arithmetic. The protocol is used to exchange * a session key SK and a session nonce SN. The original protocol is: * * A -> B : A, { msg1(Na) }Kab * B -> A : { msg2(Na, Nb) }Kab * A -> B : { msg3(Nb) }Kab * B -> A : { msg4(SK, SN) }Kab * * This protocol is flawed, not to mention rather redundant: a * 3-way handshake is being used for nonce challenges, which are * then ignored in the final message! We can fix this by merging * messages 2 and 4 into one message: * * A -> B : A, { msg1(Na) }Kab * B -> A : { msg2(SK, SN, Na, Nb) }Kab * A -> B : { msg3(Nb) }Kab * * Alan Jeffrey, v0.0.1 2001/02/22 * Christian Haack, modified for v1.1.0 2004/09/08 */
/* * Include the standard prelude */
import prelude;
/* * Words used in the correspondence assertions. */
public contacting : Word; public generating : Word; public and : Word; public for : Word;
/* * The nonce types. */
type Challenge = SoshChall(); type ResponseToA( a:Host, b:Host, sessionKey:SharedKey(a,b), sessionNonce:Challenge ) = SoshResp( begun(b generating sessionKey and sessionNonce for a), fresh(sessionNonce:Challenge) ); type ResponseToB(a:Host,b:Host) = SoshResp ( begun(a contacting b) );
/* * The message patterns. */
pattern Msg1 = Challenge; pattern Msg2(a:Host,b:Host) = ( sessionKey : SharedKey(a,b), sessionNonce : Challenge, nonceA : ResponseToA(a,b,sessionKey,sessionNonce), nonceB : Challenge ); pattern Msg3(a:Host,b:Host) = ResponseToB(a,b);
/* * The tag types. */
tag msg1(Msg1) : Auth(a:Host,b:Host); tag msg2(Msg2(a,b)) : Auth(a:Host,b:Host); tag msg3(Msg3(a,b)) : Auth(a:Host,b:Host);
/* * We assume that 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(a:Any,b:Any) : SharedKey(a,b);
/* * The initiator. */
client Initiator (a:Host, b:Host, kab:SharedKey(a,b)) at a is { establish responder at b is (socket:Socket); begin(a contacting b); new (nonceA : Challenge); output socket is (a, { msg1(nonceA) }kab); input socket is { msg2( sessionKey : SharedKey(a,b), sessionNonce : Challenge, nonceA, nonceB : Challenge ) }kab [ begun(b generating sessionKey and sessionNonce for a), fresh(sessionNonce:Challenge) ]; output socket is { msg3(nonceB) }kab; end(b generating sessionKey and sessionNonce for a); }
/* * The responder. */
server Responder(b:Host) at b is (socket:Socket) { input socket is (a:Un,ctext:Un); let kab:SharedKey(a,b) = lkupKey(a,b); match ctext is { msg1(nonceA:Challenge) }kab; new (nonceB:Challenge); new (sessionKey:SharedKey(a,b)); new (sessionNonce:Challenge); begin(b generating sessionKey and sessionNonce for a); output socket is { msg2(sessionKey,sessionNonce,nonceA,nonceB) }kab; input socket is { msg3(nonceB) }kab [ begun(a contacting b) ]; end(a contacting b); }
/* * 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