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

/* * A -> B : {| msg1(Na,A) |}pkB * B -> A : {| msg2(Na,Nb) |}pkA * A -> B : {| msg3(Nb) |}pkB * * The Needham-Schroeder Public Key protocol does not typecheck. * Lowe's fix avoids the insider attack on this protocol by including * B's name in msg2. After this fix, the protocol type-checks (see nsl.cry). * * Christian Haack, v.1.1.0, 2006/20/02 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public authenticating : Word; public to : Word;
/* Nonce types. */
type ChallengeAToB = SoshChall (); type ResponseBToA (a:Public, b:Public) = SoshResp ( begun(b authenticating to a) ); type ChallengeBToA (a:Public, b:Public) = SophChall ( begun(a authenticating to b) ); type ResponseAToB = SophResp ();
/* Message patterns. */
pattern Msg1 = ( ChallengeAToB, Public ); pattern Msg2 (a:Public) = ( na : ResponseBToA(a,b), nb : ChallengeBToA(a,b) ); // TYPE ERROR! Variable b is not in scope. pattern Msg3 = ResponseAToB;
/* Message tags. */
tag msg1 (Msg1) : Auth (b:Public); tag msg2 (Msg2(a)) : Auth (a:Public); tag msg3 (Msg3) : Auth (b:Public); client Initiator (a:Public, pA:PrivateKey(a), b:Public, pB:PublicKey(b)) at a is { establish Responder at b is (socket : Socket); new (na : ChallengeAToB); output socket is {| msg1(na,a) |}pB; input socket is {| msg2 (na, nb:ChallengeBToA(a,b)) |}pA^-1 [ begun (b authenticating to a) ]; end (b authenticating to a); begin (a authenticating to b); output socket is {| msg3(nb) |}pB; } server Responder (b:Public, pB:PrivateKey(b), a:Public, pA:PublicKey(a)) at b is (socket : Socket) { input socket is {| msg1 (na:ChallengeAToB, a) |}pB^-1; new (nb : ChallengeBToA(a,b)); begin (b authenticating to a); output socket is {| msg2(na,nb) |}pA; input socket is {| msg3(nb) |}pB^-1 [ begun (a authenticating to b) ]; end (a authenticating to b); }

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:26:19