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 signed message digest followed by an acknowledgment. * * A -> B : A, text, {| hash( msg(B,text) ) |}sA * B -> A : {| ack(A, {| hash( msg(B,text) ) |}sA) |}sB * * where * msg : a message tag * hash : a one-way hash function * sA : Alice's private signing key * ack : a message tag * sB : Bob's private signing key * * Christian Haack, v1.1.0, 2004/10/28 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public sending : Word; public to : Word; public acknowledging : Word; public receipt : Word; public of : Word;
/* * Message patterns and tags. */
pattern Msg (a:Host) = ( b:Host, text:Public ) [ !begun(a sending text to b) ]; tag msg (Msg(a)) : Auth<a:Host>; pattern Ack (b:Host) = ( a:Un, {| hash( msg(_,text:Un) ) |}_^-1 ) [ !begun(b acknowledging to a receipt of text) ]; tag ack (Ack(b)) : Auth<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 lkupAuthKey (p:Any) : AuthKey(p);
/* * The initiator. */
client Initiator (a:Host, b:Host, sA:SignKey(a), sB:AuthKey(b)) at a is { establish Receiver at b is (socket : Socket); new (text : Public); begin! (a sending text to b); output socket is (a, text, {| hash( msg(b,text) ) |}sA); input socket is {| ack (a, {| hash( msg(b,text) ) |}sA) |}sB^-1 [ !begun (b acknowledging to a receipt of text) ]; end (b acknowledging to a receipt of text); }
/* * The receiver. */
server Receiver (b:Host, sB:SignKey(b)) at b is (socket : Socket) { input socket is (a:Un, text:Un, ctext:Un); let sA:AuthKey(a) = lkupAuthKey(a); match ctext is {| hash( msg(b,text) ) |}sA^-1 [ !begun (a sending text to b) ]; end (a sending text to b); begin! (b acknowledging to a receipt of text); output socket is {| ack(a,ctext) |}sB; }
/* * 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