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