/* 
 * An acknowledgment using a nonce.
 * This is a "Secret-Out-Public-Home" (SOPH) nonce.
 * SOPH nonces are similar to Guttman's outgoing tests.
 *
 * Alice sends a text and a nonce N to Bob. 
 * Bob returns N, in order to acknowledge the receipt of the text.
 * 
 *   A -> B : {| msg(A,text,N) |}pB
 *   B -> A : N
 *
 * where 
 *   N : a nonce
 *   msg : a message tag
 *   pB : Bob's public encryption key
 *
 * Christian Haack, v1.1.0 2004/10/25
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public acknowledging : Word;
public receipt : Word;
public of : Word;
public to : Word;

/*
 * Nonce types.
 */

type Challenge (a:Any, b:Any, text:Any)
  = SophChall ( begun(b acknowledging receipt of text to a) );

type Response 
  = SophResp ( ); 

/*
 * Message pattern.
 */

pattern Msg (b:Host) 
  = ( a:Host, text:Private, n:Challenge(a,b,text) );

/* 
 * Message tag.
 */

tag msg (Msg(b)) : Auth(b:Host);  

/*
 * The initiator.
 */

client Initiator (a:Host, b:Host, pB:PublicKey(b)) at a is 
{
  establish Responder at b is (socket : Socket);
  new (text : Private);	
  new (n : Challenge(a,b,text));
  output socket is {| msg(a,text,n) |}pB;
  input socket is n 
    [ begun(b acknowledging receipt of text to a) ];
  end(b acknowledging receipt of text to a);
}
	 
/*
 * The responder.
 */

server Responder (b:Host, pB:PrivateKey(b)) at b is (socket : Socket) 
{
  input socket is 
    {| msg(a:Un, text:Tainted, n:Challenge(a,b,text)) |}pB^-1;
  begin(b acknowledging receipt of text to a);
  output socket is n;	
}

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