/*
 * Sign-then-encrypt.
 *
 *   A -> B : A, {| {| msg(text,B) |}sA |}pB
 *
 * where
 *    msg : a message tag
 *    sA : Alice's private signing key
 *    pB : Bob's public encryption key
 *
 * Christian Haack, v1.1.0 2004/10/14
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public sending : Word;
public secret : Word;
public to : Word;

/*
 * The message pattern.
 */

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

/*
 * The message tag.
 */

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

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

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

/* The sender. */

client Sender
  (a:Host, b:Host, sA:SignKey(a), pB:PublicKey(b)) 
  at a is 
{
  establish Receiver at b is (socket : Socket);
  new (text : Private);
  begin! (a sending secret text to b);
  output socket is (a, {| {| msg(text,b) |}sA |}pB);
}
  
/* The receiver. */

server Receiver
  (b:Host, pB:PrivateKey(b)) 
  at b is (socket : Socket) 
{
  input socket is (a:Un, {| ctext:Tainted |}pB^-1);
  let sA:AuthKey(a) = lkupAuthKey(a);
  match ctext is {| msg(text:Private,b) |}sA^-1
    [ !begun (a sending secret text to b) ];
  end (a sending secret text 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:53