/* 
 * A signed message digest followed by an acknowledgment. 
 *
 *   A -> B : A, text, {| hash( msg(B,text) ) |}sA
 *   B -> A : {| ack(A, {| hash( msg(B,text) ) |}sA) |}sB
 *
 * where 
 *   msg : a message tag
 *   hash : a one-way hash function
 *   sA : Alice's private signing key
 *   ack : a message tag
 *   sB : Bob'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 acknowledging : Word;
public receipt : Word;
public of : Word;

/*
 * Message patterns and tags.
 */

pattern Msg (a:Host) 
  = ( b:Host, text:Public ) [ !begun(a sending text to b) ];

tag msg (Msg(a)) : Auth<a:Host>;  

pattern Ack (b:Host) 
  = ( a:Un, {| hash( msg(_,text:Un) ) |}_^-1 )
    [ !begun(b acknowledging to a receipt of text) ];

tag ack (Ack(b)) : Auth<b: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), sB:AuthKey(b)) at a is 
{
  establish Receiver at b is (socket : Socket);
  new (text : Public);	
  begin! (a sending text to b);	
  output socket is (a, text, {| hash( msg(b,text) ) |}sA);
  input socket is {| ack (a, {| hash( msg(b,text) ) |}sA) |}sB^-1
    [ !begun (b acknowledging to a receipt of text) ];
  end (b acknowledging to a receipt of text); 
}
	 
/*
 * The receiver.
 */

server Receiver (b:Host, sB:SignKey(b)) at b is (socket : Socket) 
{
  input socket is (a:Un, text:Un, ctext:Un);
  let sA:AuthKey(a) = lkupAuthKey(a);
  match ctext is {| hash( msg(b,text) ) |}sA^-1
    [ !begun (a sending text to b) ];
  end (a sending text to b);
  begin! (b acknowledging to a receipt of text);
  output socket is {| ack(a,ctext) |}sB;
}

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