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 the complete Needham-Schroeder-Lowe Protocol. * * A -> S : A,B * S -> A : {| msgKey(pkB,B) |}sS * A -> B : {| msg1(Na,A) |}pB * B -> S : B,A * S -> B : {| msgKey(pkA,A) |}sS * B -> A : {| msg2(Na,Nb,B) |}pA * A -> B : {| msg3(Nb) |}pB * * Christian Haack, v1.1.0 2004/10/11 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public acknowledging : Word; public receipt : Word; public of : Word; public nonce : Word; public to : Word;
/* * Nonce types. */
type ChallengeAToB = SoshChall (); type ResponseBToA ( a:Any, b:Any, na:Any ) = SoshResp ( begun(b acknowledging to a receipt of nonce na) ); type ChallengeBToA ( a:Any, b:Any, nb:Any ) = SophChall ( begun(a acknowledging to b receipt of nonce nb) ); type ResponseAToB = SophResp ();
/* * Message patterns. */
pattern MsgKey = ( PublicKey(p), p:Un ); pattern Msg1 = ( ChallengeAToB, Host ); pattern Msg2 (a:Any) = ( na : ResponseBToA(a,b,na), nb : ChallengeBToA(a,b,nb), b : Host ); pattern Msg3 = ResponseAToB;
/* * Message tags. */
tag msgKey (MsgKey) : Auth <s:Server>; tag msg1 (Msg1) : Auth (b:Any); tag msg2 (Msg2(a)) : Auth (a:Any); tag msg3 (Msg3) : Auth (b:Any);
/* * The initiator. */
client Initiator (a:Host, b:Host, s:Server, sS:AuthKey(s), pA:PrivateKey(a)) at a is { establish Server at s is (socketS : Socket); output socketS is (a,b); input socketS is {| msgKey( pB:PublicKey(b), b) |}sS^-1; establish Responder at b is (socketB : Socket); new (na : ChallengeAToB); output socketB is {| msg1(na,a) |}pB; input socketB is {| msg2 (na, nb:ChallengeBToA(a,b,nb), b) |}pA^-1 [ begun (b acknowledging to a receipt of nonce na) ]; end (b acknowledging to a receipt of nonce na); begin (a acknowledging to b receipt of nonce nb); output socketB is {| msg3(nb) |}pB; }
/* * The responder. */
server Responder (b:Host, s:Server, sS:AuthKey(s), pB:PrivateKey(b)) at b is (socket : Socket) { input socket is {| msg1 (na:ChallengeAToB, a:Un) |}pB^-1; establish Server at s is (socketS : Socket); output socketS is (b,a); input socket is {| msgKey( pA:PublicKey(a), a ) |}sS^-1; new (nb : ChallengeBToA(a,b,nb)); begin (b acknowledging to a receipt of nonce na); output socket is {| msg2(na,nb,b) |}pA; input socket is {| msg3(nb) |}pB^-1 [ begun (a acknowledging to b receipt of nonce nb) ]; end (a acknowledging to b receipt of nonce nb); }
/* * The Public Key Server. */
/* * We assume that the public key server is able to securely lookup public * keys. We formally express this by assuming the existence of a secure * lookup function of the following dependent function type: */
fun lkupKey (p:Any) : PublicKey(p); server KeyServer (s:Server, sS:SignKey(s)) at s is (socket : Socket) { input socket is (p:Un,q:Un); let pP:PublicKey(p) = lkupKey (p); output socket is {| msgKey(pP,p) |}sS; }
/* * 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