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 simple example discussed in the Introduction at intro.html. * * Christian Haack, v.1.1.0 2004/11/08 */
import prelude; public sending : Word; public to : Word; private SKey : SharedKey (Alice,Bob); pattern Msg (a:Host, b:Host) = ( msg : Public ) [ !begun (a sending msg to b) ]; tag MTag (Msg(a,b)) : Auth(a:Host, b:Host); client Sender at Alice is { establish Receiver at Bob is (socket : Socket); new (msg : Public); begin! (Alice sending msg to Bob); output socket is { MTag(msg) }SKey; } server Receiver at Bob is (socket : Socket) { input socket is { MTag(msg:Public) }SKey; end (Alice sending msg to Bob); }
/* * 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