/*
 * This is Woo and Lam's Mutual Authentication Protocol.
 * The protocol allows
 * the server S to generate a session key Kab for use by A and B.
 * The protocol (once we add message tags, and reorder the messages
 * to fit the requirements of dependent records, and add A and Bs
 * names to message 4) is:
 *
 *   A -> B : A, Na
 *   B -> A : B, Nb
 *   A -> B : { msg3 (A, B, Na, Nb) }Kas
 *   B -> S : A, B, { msg3 (A, B, Na, Nb) }Kas, { msg4 (A, B, Na, Nb) }Kbs
 *   S -> B : { msg5a (B, Kab, Na, Nb) }Kas, { msg5b (A, Kab, Na, Nb) }Kbs
 *   B -> A : { msg5a (B, Kab, Na, Nb) }Kas, { msg6 (Na, Nb) }Kab
 *   A -> B : { msg7 (Nb) }Kab
 *
 * This protocol can't be verified directly in Cryptyc, since the nonce
 * Na is being used for two different purposes: once as a nonce challenge
 * to Sam to verify the freshness of Kab, and once as a nonce challenge
 * to Bob to verify that Bob is authenticating to Alice.  The same is
 * true of Nb.  We have to split the nonces in their two roles:
 *
 *   A -> B : A, Na1, Na2
 *   B -> A : B, Nb1, Nb2
 *   A -> B : { msg3 (A, B, Na1, Nb1) }Kas
 *   B -> S : A, B, { msg3 (A, B, Na1, Nb1) }Kas, { msg4 (A, B, Na1, Nb1) }Kbs
 *   S -> B : { msg5a (B, Kab, Na1, Nb1) }Kas, { msg5b (A, Kab, Na1, Nb1) }Kbs
 *   B -> A : { msg5a (B, Kab, Na1, Nb1) }Kas, { msg6 (Na2, Nb2) }Kab
 *   A -> B : { msg7 (Nb2) }Kab
 * 
 * Note that the type analysis here makes it obvious that messages 3 and
 * 4 do not need to be encrypted, and in fact messages 2 and 3 can be
 * elimiated all together).
 *
 * Alan Jeffrey, v0.0.1 2001/03/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 nonces
 */

public providing : Word;
public contacting : Word;
public contacted : Word;
public session : Word;
public key : Word;
public with : Word;
public by : Word;
public to : Word;
public for : Word;

/*
 * The types of the nonce and keys.
 */

type WLMANonceA2 (a : Host, b : Host)
  = Nonce ( end (b contacted by a) );

type WLMANonceB2 (a : Host, b : Host)
  = Nonce ( end (a contacting b) );

type WLMASMsg6 (a : Host, b : Host)
  = Struct ( nonceA2' : WLMANonceA2 (a, b), nonceB2 : Challenge );

type WLMASMsg7 (a : Host, b : Host)
  = WLMANonceB2 (a, b);

type WLMASMsg (a : Host, b : Host)
  = Union ( msg6 : WLMASMsg6 (a, b), msg7 : WLMASMsg7 (a, b), msgP : Payload );

type WLMASKey (a : Host, b : Host)
  = Key ( WLMASMsg (a, b) );

type WLMANonceB1 (a : Host, b : Host, sKey : WLMASKey (a, b))
  = Nonce ( end (Sam providing session key sKey to b for a) );

type WLMANonceA1 (a : Host, b : Host, sKey : WLMASKey (a, b))
  = Nonce ( end (Sam providing session key sKey for a to b) );

// Note that this typing makes clear that the encryption of messages
// 3 and 4 is pointless: all the data in the messages is public.

type WLMAMsg3 (a : Host)
  = Struct ( a' : Host, b: Host, nonceA1 : Challenge, nonceB1 : Challenge );

type WLMAMsg4 (b : Host)
  = Struct ( a : Host, b': Host, nonceA1 : Challenge, nonceB1 : Challenge );

type WLMAMsg5a (a : Host)
  = Struct ( b : Host, sKey : WLMASKey (a, b), nonceA1' : WLMANonceA1 (a, b, sKey), nonceB1' : WLMANonceB1 (a, b, sKey) );

type WLMAMsg5b (b : Host)
  = Struct ( a : Host, sKey : WLMASKey (a, b), nonceA1' : WLMANonceA1 (a, b, sKey), nonceB1' : WLMANonceB1 (a, b, sKey) );

type WLMAMsg (h : Host)
  = Union ( msg3 : WLMAMsg3 (h), msg4 : WLMAMsg4 (h), msg5a : WLMAMsg5a (h), msg5b : WLMAMsg5b (h) );

type WLMAKey (h : Host) 
  = Key (WLMAMsg (h));

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

type WLMAKDCMsg = Struct (h : Host, keyH : WLMAKey (h));
type WLMAKDCKey = Key (WLMAKDCMsg);

/*
 * The shared keys.
 */

private keyA : WLMAKey (Alice);
private keyB : WLMAKey (Bob);
private keyKDC : WLMAKDCKey;

/*
 * The initiator.
 */

client Initiator at Alice is {

  begin (Alice contacting Bob);

  establish Responder at Bob is (socketB : Socket);

  new (nonceA1 : Challenge);
  new (nonceA2 : Challenge);

  output socketB is (Alice, nonceA1, nonceA2);

  input socketB is (Alice, Bob, nonceB1 : Challenge, nonceB2 : Challenge);

  output socketB is ({ msg3 (Alice, Bob, nonceA1, nonceB1) }keyA);

  input socketB is ({ msg5a (
    Bob, 
    sKey : WLMASKey (Alice, Bob), 
    nonceA1' : WLMANonceA1 (Alice, Bob, sKey),
    nonceB1' : WLMANonceB1 (Alice, Bob, sKey)
  ) }keyA, { msg6 (
    nonceA2' : WLMANonceA2 (Alice, Bob),
    nonceB2
  ) }sKey);

  cast nonceB2 is (nonceB2' : WLMANonceB2 (Alice, Bob));

  output socketB is ( { msg7 (nonceB2') }sKey );

  check nonceA1 is nonceA1';
  check nonceA2 is nonceA2';

  end (Bob contacted by Alice);
  end (Sam providing session key sKey for Alice to Bob);

}

/*
 * The responder.
 */

server Responder at Bob is (socketA : Socket) {

  input socketA is (a : Host, nonceA1 : Challenge, nonceA2 : Challenge);

  begin (Bob contacted by a);

  new (nonceB1 : Challenge);
  new (nonceB2 : Challenge);

  output socketA is (Bob, nonceB1, nonceB2);

  input socketA is ( ctext3 : CText );

  establish Intermediary at Sam is (socketS : Socket);

  output socketS is ( ctext3, { msg4 (
    a,
    Bob,
    nonceA1,
    nonceB1
  ) }keyB );

  input socketS is ( ctext5a : CText, { msg5b (
    a,
    sKey : WLMASKey (a, Bob),
    nonceA1' : WLMANonceA1 (a, Bob, sKey),
    nonceB1' : WLMANonceB1 (a, Bob, sKey)
  ) }keyB );

  check nonceB1 is nonceB1';

  cast nonceA2 is ( nonceA2' : WLMANonceA2 (a, Bob) );

  output socketA is ( ctext5a, { msg6 ( nonceA2', nonceB2 ) }sKey );

  input socketA is ( { msg7 ( nonceB2' : WLMANonceB2 (a, Bob) ) }sKey );

  check nonceB2 is nonceB2';

  end (a contacting Bob);
  end (Sam providing session key sKey to Bob for a);

}

/*
 * The intermediary.
 */

server Intermediary at Sam is (socketB : Socket) {

  input socketB is ( a : Host, b : Host, ctext3 : CText, ctext4 : CText );

  establish KDC at KDCHost is (socketKDC : Socket);
  output socketKDC is (a);
  input socketKDC is ({ a, keyA : WLMAKey (a) }keyKDC);
  output socketKDC is (b);
  input socketKDC is ({ b, keyB : WLMAKey (b) }keyKDC);

  decrypt ctext3 is ( { msg3 ( a, b, nonceA1 : Challenge, nonceB1 : Challenge ) }keyA );
  decrypt ctext4 is ( { msg4 ( a, b, nonceA1, nonceB1 ) }keyB );

  new (sKey : WLMASKey (a, b));
  begin (Sam providing session key sKey for a to b);
  begin (Sam providing session key sKey to b for a);

  cast nonceA1 is (nonceA1' : WLMANonceA1 (a, b, sKey));
  cast nonceB1 is (nonceB1' : WLMANonceB1 (a, b, sKey));

  output socketB is (
    { msg5a ( b, sKey, nonceA1', nonceB1' ) }keyA,
    { msg5b ( a, sKey, nonceA1', nonceB1' ) }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