/*
 * 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