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 example uses nested signatures. Alice and Bob want to send a secret * message M that is signed by both of them to Charly. To this end, Alice * generates M, signs it and then sends it to Bob requesting his signature. * Then Bob reads and signs M, and forwards the doubly signed message to * Charly. * * A -> B : A, { signRequest(C, {| msg(M,C) |}sA) }kAB * B -> C : A, B, {| {| {| msg(M,C) |}sA |}sB |}pC * * where * msg : a message tag * sA : Alice's private signing key * signRequest : a message tag * kAB : Alice and Bob's shared key * sB : Bob's private signing key * pC : Charly's public encryption key * * Christian Haack, v1.1.0 2004/10/21 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public and : Word; public sending : Word; public to : Word;
/* * The message patterns. */
pattern Msg (a:Host,b:Host,c:Host) = ( text:Private, c ) [!begun (a and b sending text to c)]; pattern SignRequest (b:Host) = ( c:Host, Private(b,c) );
/* * The message tags. */
tag msg (Msg(a,b,c)) : Auth (a:Host,b:Host,c:Host); tag signRequest (SignRequest(b)) : Auth (a:Host,b:Host);
/* * We assume that principals are able to securely lookup the required keys. * We formally express this by assuming the existence of secure lookup * functions of the following dependent function types: */
fun lkupPubKey (p:Any) : PublicKey(p); fun lkupAuthKey (p:Any) : AuthKey(p); fun lkupSharedKey (p:Any,q:Any) : SharedKey(p,q);
/* The initiator. */
client Initiator (a:Host, b:Host, c:Host, sA:SignKey(a), kAB:SharedKey(a,b)) at a is { establish Intermediary at b is (socket : Socket); new (text : Private); begin!(a and b sending text to c); output socket is ( a, { signRequest(c, {| msg(text,c) |}sA) }kAB ); }
/* The intermediary. */
server Intermediary (b:Host, sB:SignKey(b)) at b is (socket : Socket) { input socket is (a:Un, ctext:Un); let kAB:SharedKey(a,b) = lkupSharedKey(a,b); let sA:AuthKey(a) = lkupAuthKey(a); match ctext is { signRequest(c:Host, signedtext:Private(b,c)) }kAB; match signedtext is {| msg(text:Private, c) |}sA^-1; establish Receiver at c is (socketC : Socket); let pC:PublicKey(c) = lkupPubKey(c); output socketC is (a, b, {| {| signedtext |}sB |}pC); }
/* The receiver */
server Receiver (c:Host, pC:PrivateKey(c)) at c is (socket : Socket) { input socket is (a:Un, b:Un, {| signedtext:Tainted |}pC^-1); let sB:AuthKey(b) = lkupAuthKey(b); let sA:AuthKey(a) = lkupAuthKey(a); match signedtext is {| {| msg(text:Private, c) |}sA^-1 |}sB^-1 [ !begun(a and b sending text to c) ]; end(a and b sending text to c); }
/* * 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