/* 
 * This example is similar to part of an example from Bhargavan, Fournet 
 * and Gordon's paper "A Model for Web Services Security".
 * It is a essentially a version of a one-way authentication procedure that
 * is included in the X509 recommendation. See, for instance, Chapter 14.2 
 * in Stalling's book "Cryptography and Network Security", or Section 6.9.1 
 * in the Clark-Jacob survey. 
 *
 * A -> B  M,A,B,Time,MsgId, 
 *         {| digest( hash( hash(M), hash(B), hash(Time), hash(MsgId) ) ) |}sA
 *
 * where
 *   hash : a one-way hash function
 *   digest : a message tag 
 *    sA : Alice's private signing key.
 *
 * 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) 
  = ( hash( hash(text:Public), hash(b:Host), hash(time:Public), 
            hash(msgid:Public) ) 
    ) [ !begun(a sending text with msgid and time to b) ];

/* 
 * Message digest tag.
 */

tag digest (Digest(a)) : Auth<a:Host>;  

/*
 * We assume that principals are able to securely lookup the required keys.
 * We formally express this by assuming the existence of secure lookup 
 * functions of the following dependent function types:
 */

fun lkupAuthKey (p:Any) : AuthKey(p);

/*
 * The initiator.
 */

client Initiator (a:Host, b:Host, sA:SignKey(a)) 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,
     {| digest( hash( hash(text), hash(b), hash(time), hash(msgid) ) ) |}sA);
}
	 
/*
 * The receiver.
 */

server Receiver (b:Host) at b is (socket : Socket) 
{
  input socket is (text:Un, a:Un, b, time:Un, msgid:Un, signed:Un);
  let sA:AuthKey(a) = lkupAuthKey (a);
  match signed is 
     {| digest( hash( hash(text), hash(b), hash(time), hash(msgid) ) ) |}sA^-1
     [ !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