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 a stripped down version of part of a web services protocol. * The example is similar to an example from Bhargavan, Fournet and Gordon's * paper "A Model for Web Services Security". * * A -> B M,A,B,Time,MsgId, * keyedhash * ( kab, * digest( hash( hash(M), hash(Time), hash(MsgId) ) ) * ) * * where * hash : a one-way hash function * digest : a message tag * kab : a hash key * keyedhash : a keyed one-way hash function * * 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 and : Word; public with : Word;
/* * Message digest pattern. */
pattern Digest (a:Host, b:Host) = ( hash( hash(text:Public), hash(time:Public), hash(msgid:Public) ) ) [ !begun(a sending text with msgid and time to b) ];
/* * Message digest tag. */
tag digest (Digest(a,b)) : Auth(a:Host,b:Host);
/* * We assume that principals are able to securely lookup the required hash * keys. We formally express this by assuming the existence of a secure lookup * function of the following dependent function type: */
fun lkupHashKey (p:Any,q:Any) : HashKey(p,q);
/* * The initiator. */
client Initiator (a:Host, b:Host, kab:HashKey(a,b)) at a is { establish Receiver at b is (socket : Socket); new (text : Public); new (msgid : Public); new (time : Public); begin! (a sending text with msgid and time to b); output socket is (text, a, b, time, msgid, keyedhash( kab, digest( hash( hash(text), hash(time), hash(msgid) ) ) )); }
/* * The receiver. */
server Receiver (b:Host) at b is (socket : Socket) { input socket is (text:Un, a:Un, b, time:Un, msgid:Un, digest':Un); let kab:HashKey(a,b) = lkupHashKey (a,b); match digest' is keyedhash( kab, digest( hash( hash(text), hash(time), hash(msgid) ) ) ) [ !begun (a sending text with msgid and time to b) ]; end (a sending text with msgid and time 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:52