/*
 * This example uses nested signatures. Alice and Bob want to send a secret 
 * message M that is signed by both of them to Charly. To this end, Alice 
 * generates M, signs it and then sends it to Bob requesting his signature. 
 * Then Bob reads and signs M, and forwards the doubly signed message to 
 * Charly. 
 *
 *   A -> B : A, { signRequest(C, {| msg(M,C) |}sA) }kAB
 *   B -> C : A, B, {| {| {| msg(M,C) |}sA |}sB |}pC
 *
 * where
 *   msg : a message tag
 *   sA : Alice's private signing key
 *   signRequest : a message tag
 *   kAB : Alice and Bob's shared key
 *   sB : Bob's private signing key
 *   pC : Charly's public encryption key
 *
 * Christian Haack, v1.1.0 2004/10/21
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public and : Word;
public sending : Word;
public to : Word;

/*
 * The message patterns.
 */

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

pattern SignRequest (b:Host) 
  = ( c:Host, Private(b,c) );

/*
 * The message tags.
 */

tag msg (Msg(a,b,c)) : Auth (a:Host,b:Host,c:Host);
tag signRequest (SignRequest(b)) : Auth (a:Host,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 lkupPubKey (p:Any) : PublicKey(p);
fun lkupAuthKey (p:Any) : AuthKey(p);
fun lkupSharedKey (p:Any,q:Any) : SharedKey(p,q);

/* The initiator. */

client Initiator 
  (a:Host, b:Host, c:Host, sA:SignKey(a), kAB:SharedKey(a,b)) 
  at a is 
{
  establish Intermediary at b is (socket : Socket);
  new (text : Private);
  begin!(a and b sending text to c);
  output socket is ( a, { signRequest(c, {| msg(text,c) |}sA) }kAB );
}  	

/* The intermediary. */

server Intermediary 
  (b:Host, sB:SignKey(b)) 
  at b is (socket : Socket) 
{
  input socket is (a:Un, ctext:Un);
  let kAB:SharedKey(a,b) = lkupSharedKey(a,b);	
  let sA:AuthKey(a) = lkupAuthKey(a);
  match ctext is { signRequest(c:Host, signedtext:Private(b,c)) }kAB;
  match signedtext is {| msg(text:Private, c) |}sA^-1;
  establish Receiver at c is (socketC : Socket);  	
  let pC:PublicKey(c) = lkupPubKey(c);
  output socketC is (a, b, {| {| signedtext |}sB |}pC);
}

/* The receiver */

server Receiver 
  (c:Host, pC:PrivateKey(c))
  at c is (socket : Socket)
{
  input socket is (a:Un, b:Un, {| signedtext:Tainted |}pC^-1);
  let sB:AuthKey(b) = lkupAuthKey(b);
  let sA:AuthKey(a) = lkupAuthKey(a);
  match signedtext is {| {| msg(text:Private, c) |}sA^-1 |}sB^-1
    [ !begun(a and b sending text to c) ];
  end(a and b sending text to c);
}	

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