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

/* * Some standard definitions for use in Cryptyc programs * Alan Jeffrey v0.0.8 2001/03/08 * Christian Haack, modified for v1.1.0, 2004/10/11 */
/* * Some standard types for use in protocols. */
type Payload = Private(); type Host = Public(); type Server = Public(); type Client = Public(); type Word = Public(); type Socket = Un;
/* * Some standard host names for use in protocols. */
public Alice : Host; public Bob : Host; public Charlie : Host; public Eve : Host; public Sam : Host;
/* * Symmetric key. */
type SharedKey (x:Any) = SymKey (Private(x), _);
/* * Public encryptyion key and corresponding decryption key. */
type PublicKey (x:Any) = PubKeyEK (Private(x), _); type PrivateKey (x:Any) = PubKeyDK (Private(x), _);
/* * Signing key and corresponding authentication key. */
type SignKey (x:Any) = SignKeyEK (Private(x,y), y:Any); type AuthKey (x:Any) = SignKeyDK (Private(x,y), y:Any);
/* * Hashing. */
public hashkey : PubKeyEK(Any); tag hashtag ({| Private(y) |}hashkey) : Auth(y:Any); define hash (x:Any) = hashtag( {|x|}hashkey );
/* * Keyed hashing. */
define keyedhash (k:Any,x:Any) = { hash(x) }k; type HashKey (x:Any) = SymKey (hash(Private(x)), _);

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