/*
 * The Abadi/Gordon wide mouth frog protocol.
 * This is a varient of the Wide Mouthed Frog protocol
 * with nonce challenges rather than timestamps.
 * Alan Jeffrey, v0.0.1 2001/02/08
 */

/*
 * 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 sending : Word;
public key : Word;

/*
 * Types used in the protocol.
 */

type SKey =
  Key (Payload);

type WMFNonce (a : Host, b : Host, sKey : SKey) =
  Nonce (end (a sending b key sKey));

type WMFMsg3 (a : Host) = 
  Struct (b : Host, sKey : SKey, nonce : WMFNonce (a, b, sKey));

type WMFMsg6 (b : Host) = 
  Struct (a : Host, sKey : SKey, nonce : WMFNonce (a, b, sKey));

type WMFMsg (h : Host) = 
  Union (msg3 : WMFMsg3 (h), msg6 : WMFMsg6 (h));

type WMFKey (h : Host) = 
  Key (WMFMsg (h));

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

type WMFKDCMsg = Struct (h : Host, keyH : WMFKey (h));
type WMFKDCKey = Key (WMFKDCMsg);

/*
 * The shared keys.
 */

private keyA : WMFKey (Alice);
private keyB : WMFKey (Bob);
private keyKDC : WMFKDCKey;

/*
 * The initiator.
 */

client Initiator at Alice is {

  new (sKey : SKey);
  begin (Alice sending Bob key sKey);
  establish Intermediary at Sam is (socket : Socket);
  output socket is (Alice);
  input socket is (nonceA : Challenge);
  cast nonceA is (nonceA' : WMFNonce (Alice, Bob, sKey));
  output socket is (Alice, { msg3 (Bob, sKey, nonceA') }keyA);

}

/*
 * The responder.
 */

server Responder at Bob is (socket : Socket) {

  new (nonceB : Challenge);
  output socket is (nonceB);
  input socket is ({ msg6 (a : Host, sKey : SKey, nonceB' : WMFNonce (a, Bob, sKey)) }keyB);
  check nonceB is nonceB';
  end (a sending Bob key sKey);

}

/*
 * The intermediary.
 */

server Intermediary at Sam is (socketA : Socket) {

  input socketA is (a : Host);
  establish KDC at KDCHost is (socketKDC : Socket);
  output socketKDC is (a);
  input socketKDC is ({ a, keyA : WMFKey (a) }keyKDC);
  new (nonceA : Challenge);
  output socketA is (nonceA);
  input socketA is (a, { msg3 (b : Host, sKey : SKey, nonceA' : WMFNonce (a, b, sKey)) }keyA);
  check nonceA is nonceA';
  output socketKDC is (b);
  input socketKDC is ({ b, keyB : WMFKey (b) }keyKDC);
  establish Responder at b is (socketB : Socket);
  input socketB is (nonceB : Challenge);
  cast nonceB is (nonceB' : WMFNonce (a, b, sKey));
  output socketB is ({ msg6 (a, sKey, nonceB') }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