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, slightly modified, 2004/11/04 */
/* * Some standard types for use in protocols. */
type Payload = Private; type Host = Un; type Server = Un; type Client = Un; type Word = Un; type Socket = Un; type Challenge = Un; type CText = Un;
/* * Some standard host names for use in protocols. */
public Alice : Host; public Bob : Host; public Charlie : Host; public Eve : Host; public Sam : Host;
/* * Hashing. */
public hashkey : PubKeyEK(Any); tag hashtag ( {| Private(y) |}hashkey ) : Auth(y:Any); define hash(x:Any) = hashtag( {|x|}hashkey );

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