/*
 * A simple example of a nonce challenge
 * This is the `ISO Symmetric Key Two-Pass Unilateral Authentication
 * Protocol' of Clark and Jacob (1997).
 *
 *   A -> B : A
 *   B -> A : Na
 *   A -> B : { msg(Na,text) }Kab
 *
 * Alan Jeffrey v0.0.2 2001/02/22
 * Christian Haack, modified for v1.1.0 2004/09/14
 */

/*
 * 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:Payload) 
  = PoshResp ( begun(a sending text to b) );

/*
 * The message pattern.
 */

pattern Msg (a:Host,b:Host) 
  = ( nonceA:Response(a,b,text), text:Payload );

/*
 * The message tag.
 */

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

/*
 * 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) : SharedKey(p,q);

/*
 * 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, kab:SharedKey(a,b)) at a is {

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

}

/*
 * 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);
  let kab:SharedKey(a,b) = lkupKey (a,b); 
  new (nonce : Challenge);
  output socket is nonce;
  input socket is { msg(nonce,text:Payload) }kab
    [ 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:52