/*
 * A simple nonce challenge. 
 * This is a "Public-Out-Signed-Home" (POSH) nonce.
 * POSH nonces are similar to Guttman's incoming tests.
 *
 *   A -> B : A
 *   B -> A : N
 *   A -> B : {| msg(N,text,B) |}sA
 *
 * where 
 *   N : nonce
 *   msg : a message tag
 *   sA : Alice's private signing key
 *
 * Alan Jeffrey v0.0.2 2001/02/22
 * Christian Haack, modified for v1.1.0 2004/11/03
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public sending : Word;
public to : Word;

/*
 * Nonce types.
 */

type Challenge = PoshChall ();

type Response (a:Host,b:Host,text:Public) 
  = PoshResp ( begun(a sending text to b) );

/*
 * The message pattern.
 */

pattern Msg (a:Host) 
  = ( nA:Response(a,b,text), text:Public, b:Host );

/*
 * The message tag.
 */

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

/*
 * We assume that two 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, who receives a nonce challenge from the receiver,
 * generates a new message, begins the appropriate session,
 * then tags and encrypts the text with the authorizing nonce,
 * then sends the ciphertext.
 */

client Sender (a:Host, b:Host, sA:SignKey(a)) at a is {

  establish Receiver at b is (socket : Socket);
  output socket is a;
  input socket is (nonce : Challenge);
  new (text : Public);
  begin(a sending text to b);
  output socket is {| msg(nonce,text,b) |}sA;

}

/*
 * The receiver, who issues the nonce challenge, 
 * gets back the response, checks the nonce is the one issued,
 * and ends the session.
 */

server Receiver (b:Host) at b is (socket : Socket) {

  input socket is (a:Un);
  new (nonce : Challenge);
  output socket is nonce;
  let sA:AuthKey(a) = lkupAuthKey (a); 
  input socket is {| msg(nonce, text:Public, b) |}sA^-1
    [ begun(a sending text to b) ];
  end(a sending 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