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

/* * Sign-then-encrypt. * * A -> B : A, {| {| msg(text,B) |}sA |}pB * * where * msg : a message tag * sA : Alice's private signing key * pB : Bob's public encryption key * * Christian Haack, v1.1.0 2004/10/14 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public sending : Word; public secret : Word; public to : Word;
/* * The message pattern. */
pattern Msg (a:Host) = (text:Private, b:Host) [!begun (a sending secret text to b)];
/* * The message tag. */
tag msg (Msg(a)) : Auth (a:Host,b:Host);
/* * We assume that principals are able to securely lookup the required * authentication keys. We formally express this by assuming the existence * of a secure lookup function of the following dependent function type: */
fun lkupAuthKey (p:Any) : AuthKey(p);
/* The sender. */
client Sender (a:Host, b:Host, sA:SignKey(a), pB:PublicKey(b)) at a is { establish Receiver at b is (socket : Socket); new (text : Private); begin! (a sending secret text to b); output socket is (a, {| {| msg(text,b) |}sA |}pB); }
/* The receiver. */
server Receiver (b:Host, pB:PrivateKey(b)) at b is (socket : Socket) { input socket is (a:Un, {| ctext:Tainted |}pB^-1); let sA:AuthKey(a) = lkupAuthKey(a); match ctext is {| msg(text:Private,b) |}sA^-1 [ !begun (a sending secret text to b) ]; end (a sending secret text to 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