/*
 * This example is from section 6.1.5., "Using Non-Reversible Functions", 
 * of the Clark/Jacob survey. In message 2, Alice sends a fresh session
 * key to Bob. In message 3, Bob acknowledges its receipt.
 *
 * B -> A : B,Nb
 * A -> B : Na, { msg2( hash(Nb), K) }Kab 
 * B -> A : { hash( msg3(Na) ) }K      
 *
 * where 
 *   Nb : a nonce generated by Bob
 *   Na : a nonce generated by Alice
 *   Kab : Alice and Bob's shared longterm key
 *   msg2, msg3 : message tags 
 *
 * We have omitted data that is irrelevant to our desired safety properties. 
 * Moreover, we have omitted the unnecessary encryption of Na in message 2. 
 *
 * Christian Haack, v1.1.0, 2004/11/05
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondences.
 */

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

/*
 * Nonce types.
 */

type Challenge = PoshChall();

type ResponseAToB (a:Any, b:Any, k:Any) 
  = PoshResp ( begun(a sending k to b) );

type ResponseBToA (a:Any, b:Any, k:Any)
  = PoshResp ( begun(b acknowledging to a receipt of k) );

/*
 * Message patterns.
 */

pattern Msg2 (a:Any, b:Any) 
  = ( hash ( n:ResponseAToB(a,b,k) ), k:SharedKey(a,b,k) );

pattern Msg3 (a:Any, b:Any, k:Any)
  = ResponseBToA(a,b,k);

/* 
 * Tag types.
 */

tag msg2 (Msg2(a,b)) : Auth (a:Any,b:Any,k:Any);

tag msg3 (Msg3(a,b,k)) : Auth (a:Any,b:Any,k:Any);

/*
 * We assume that two principals are able to securely lookup their shared 
 * longterm keys. We formally express this by assuming the existence 
 * of a secure lookup function of the following dependent function type:
 */

fun lkupKey (p:Any,q:Any) : (k:SharedKey(p,q,k));

/*
 * The initiator.
 */

client Initiator (b:Host, a:Host, kab:SharedKey(a,b,kab)) at b is 
{
  establish Responder at a is (socket : Socket);
  new (nb : Challenge);
  output socket is (b,nb);
  input socket is (na:Challenge, { msg2( hash(nb), k:SharedKey(a,b,k) ) }kab )
    [ begun (a sending k to b) ];
  end (a sending k to b);
  begin (b acknowledging to a receipt of k);
  output socket is { hash( msg3(na) ) }k;
}

/*
 * The responder.
 */

server Responder (a:Host) at a is (socket : Socket) 
{
  input socket is (b:Un, nb:Challenge);
  new (k : SharedKey(a,b,k));
  new (na : Challenge);
  let kab : SharedKey(a,b,kab) = lkupKey (a,b);
  begin (a sending k to b);
  output socket is (na, { msg2( hash(nb), k ) }kab);
  input socket is { hash( msg3(na) ) }k
    [ begun (b acknowledging to a receipt of k) ];
  end (b acknowledging to a receipt of k);
}

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