/*
 * Woo and Lam's authentication protocol Pi
 * as discussed in Clark and Jacob 6.3.10.
 *
 * The protocol (once we add message tags) is:
 *
 *   A -> B : A
 *   B -> A : Nb
 *   A -> B : { msg3(Nb) }Kas
 *   B -> S : { msg4(A, { msg3(Nb) }Kas) }Kbs
 *   S -> B : { msg5(Nb) }Kbs
 *
 * The protocol is flawed since message 3 doesn't contain Bob's name,
 * and message 5 doesn't contain Alice's name.  Note that their protocol
 * Pi3 only fixes one of these flaws.  A fixed version is in wl.cry.
 *
 * Alan Jeffrey, v0.0.2 2001/05/18
 */


/*
 * Include the standard prelude
 */

import oldprelude;

/*
 * This file declares an initiator, a responder and an intermediary:
 */

public Initiator : Client;
public Responder : Server;
public Intermediary : Server;

/*
 * These make use of a Key Distribution Center (not defined here).
 */

public KDC : Server;
public KDCHost : Host;

/*
 * Words used in the session name.
 */

public authenticates : Word;
public to : Word;

/*
 * Types used in the protocol.
 */

type WLNonce (a : Host, b : Host) =
  Nonce (end (a authenticates to b));

// This type definition is not well-formed, because b is free.

type WLMsg3 (a : Host) = 
  Struct (nonce : WLNonce (a, b));

type WLMsg4 =
  Struct (a : Host, b : Host, cText : CText);

// This type definition is not well-formed, because a is free.

type WLMsg5 (b : Host) = 
  Struct (nonce : WLNonce (a, b));

type WLMsg (h : Host) = 
  Union (msg3 : WLMsg3 (h), msg5 : WLMsg5 (h));

type WLKey (h : Host) = 
  Key (WLMsg (h));

/*
 * Types used for the server's dialogue with the KDC.
 */

type WLKDCMsg = Struct (h : Host, keyH : WLKey (h));
type WLKDCKey = Key (WLKDCMsg);

/*
 * The shared keys.
 */

private keyA : WLKey (Alice);
private keyB : WLKey (Bob);
private keyKDC : WLKDCKey;

/*
 * The initiator.
 */

client Initiator at Alice is {

  begin (Alice authenticates to Bob);
  establish Responder at Bob is (socket : Socket);
  output socket is (Alice);
  input socket is (nonce : Challenge);
  cast nonce is (nonce' : WLNonce (Alice, Bob));
  output socket is ({ msg3 (nonce') }keyA);

}

/*
 * The responder.
 */

server Responder at Bob is (socketA : Socket) {

  input socketA is (a : Host);
  new (nonce : Challenge);
  output socketA is (nonce);
  input socketA is (cText : CText);
  establish Intermediary at Sam is (socketS : Socket);
  output socketS is (Bob, { msg4 (a, cText) }keyB);
  input socketS is ({ msg5 (nonce' : WLNonce (a, Bob)) }keyB);
  check nonce is nonce';
  end (a authenticates to Bob);

}

/*
 * The intermediary.
 */

server Intermediary at Sam is (socketB : Socket) {

  input socketB is (b : Host, cText : CText);
  establish KDC at KDCHost is (socketKDC : Socket);
  output socketKDC is (b);
  input socketKDC is ({ b, keyB : WLKey (b) }keyKDC);
  decrypt cText is ({ msg4 (a : Host, cText' : CText) }keyB);
  output socketKDC is (a);
  input socketKDC is ({ a, keyA : WLKey (a) }keyKDC);
  decrypt cText is ({ msg3 (nonce' : WLNonce (a, b)) }keyA);
  output socketB is ({ msg5 (nonce') }keyB);
  
}

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