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,B) |}pkA * A -> B : {| msg3(Nb) |}pkB * * The three-message version of Needham-Schroeder-Lowe. * * Christian Haack, v1.1.0, 2006/2/20 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public authenticating : Word; public to : Word;
/* Nonce types. */
type Challenge (a:Public, b:Public) = SophChall ( begun(b authenticating to a) ); type Response = SophResp ();
/* Message patterns. */
pattern Msg1 (b:Public) = ( Challenge(a,b), a:Public ); pattern Msg2 (a:Public) = ( na : Response, nb : Challenge(b,a), b : Public ); pattern Msg3 = Response;
/* Message tags. */
tag msg1 (Msg1(b)) : 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 : Challenge(a,b)); output socket is {| msg1(na,a) |}pB; input socket is {| msg2 (na, nb:Challenge(b,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:Challenge(a,b), a) |}pB^-1; new (nb : Challenge(b,a)); begin (b authenticating to a); output socket is {| msg2(na,nb,b) |}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 04:56:41