/*
 * This is a version of the ISO 4-pass Authentication Protocol.
 * It's in Clark and Jacobs (1997) 6.3.8.
 * The original protocol, modified to include message tags,
 * stripping out the extraneous payload messages,
 * and correcting what appear to be some typos is:
 *
 *   A -> S : A, B, Na
 *   S -> A : { msg2(B, Kab, Na) }Kas, { msg3(A, Kab, Ns) }Kbs
 *   A -> B : { msg3(A, Kab, Ns) }Kbs
 *   B -> A : { msg4(A, Nb) }Kab
 *
 * We can use Cryptyc to verify Alice's half of this protocol, but
 * we can't verify Bob's half, because although Bob issues a nonce
 * challenge to Alice, Alice never responds!  We can fix this by
 * adding a fifth message:
 *
 *   A -> B : { msg5(Nb) }Kab
 *
 * but this still isn't enough to verify the protocol, since it suffers
 * from the same key compromise attack as Needham-Schroeder.  The problem
 * is that Bob has no way to associate Alice's msg5 back to msg3 (where
 * he receives Sam's ticket authenticating Kab).  We can fix this by
 * allowing Alice access to Ns.  The resulting protocol is:
 *
 *   A -> S : A, B, Na
 *   S -> A : { msg2(B, Kab, Ns, Na) }Kas, { msg3(A, Kab, Ns) }Kbs
 *   A -> B : { msg3(A, Kab, Ns) }Kbs
 *   B -> A : { msg4(A, Nb) }Kab
 *   A -> B : { msg5(Ns, Nb) }Kab
 *
 * Note that Alice never gets to issue a nonce challenge to Bob, so although
 * she knows that Sam generated the key for her and Bob, she doesn't know
 * that Bob actually got it.
 *
 * Alan Jeffrey, v0.0.1 2001/03/09
 */

/*
 * 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 initiator : Word;
public responder : Word;
public shares : Word;
public with : Word;
public for : Word;
public and : Word;
public generated : Word;
public contacts : Word;

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

type ISO4NonceB (a : Host, b : Host, nonceS : Challenge)
  = Nonce ( end (initiator a contacts responder b), check (nonceS) );

type ISO4SMsg4 (a : Host, b : Host)
  = Struct ( a' : Host, nonceB : Challenge );

type ISO4SMsg5 (a : Host, b : Host)
  = Struct ( nonceS : Challenge, nonceB' : ISO4NonceB (a, b, nonceS) );

type ISO4SMsg (a : Host, b : Host)
  = Union ( msg4 : ISO4SMsg4 (a, b), msg5 : ISO4SMsg5 (a, b) );

type ISO4SKey (a : Host, b : Host)
  = Key (ISO4SMsg (a, b));

type ISO4NonceA (a : Host, b : Host, sKey : ISO4SKey (a, b), nonceS : Challenge)
  = Nonce (end (Sam generated sKey for initiator a and responder b), check (nonceS));

type ISO4NonceS (a : Host, b : Host, sKey : ISO4SKey (a, b))
  = Nonce (end (Sam generated sKey for responder b and initiator a));

type ISO4Msg2 (a : Host)
  = Struct ( b : Host, sKey : ISO4SKey (a, b), nonceS : Challenge, nonceA' : ISO4NonceA (a, b, sKey, nonceS) );

type ISO4Msg3 (b : Host)
  = Struct ( a : Host, sKey : ISO4SKey (a, b), nonceS' : ISO4NonceS (a, b, sKey) );

type ISO4Msg (h : Host)
  = Union ( msg2 : ISO4Msg2 (h), msg3 : ISO4Msg3 (h) );

type ISO4Key (h : Host)
  = Key (ISO4Msg (h));

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

type ISO4KDCMsg 
  = Struct (h : Host, keyH : ISO4Key (h));

type ISO4KDCKey 
  = Key (ISO4KDCMsg);

/*
 * The shared keys.
 */

private keyA : ISO4Key (Alice);
private keyB : ISO4Key (Bob);
private keyKDC : ISO4KDCKey;

/*
 * The initiator.
 */

client Initiator at Alice is {

  new (nonceA : Challenge);

  establish Intermediary at Sam is (socketS : Socket);
  output socketS is (Alice, Bob, nonceA);
  input socketS is (
    { msg2 (
      Bob, 
      sKey : ISO4SKey (Alice, Bob), 
      nonceS : Challenge,
      nonceA' : ISO4NonceA (Alice, Bob, sKey, nonceS)
    ) }keyA,
    ticket : Un
  );

  check nonceA is nonceA';

  end (Sam generated sKey for initiator Alice and responder Bob);

  begin (initiator Alice contacts responder Bob);

  establish Responder at Bob is (socketB : Socket);
  output socketB is (ticket);
  input socketB is ( { msg4 ( Alice, nonceB : Challenge ) }sKey );
  cast nonceB is (nonceB' : ISO4NonceB (Alice, Bob, nonceS));
  output socketB is ( { msg5 ( nonceS, nonceB' ) }sKey );

  // Note that Alice can't end the session with Bob here,
  // since she doesn't get to issue a nonce challenge to Bob.

}

/*
 * The responder.
 */

server Responder at Bob is (socketA : Socket) {

  new (nonceB : Challenge);

  input socketA is ( { msg3 ( 
    a : Host, 
    sKey : ISO4SKey (a, Bob), 
    nonceS' : ISO4NonceS (a, Bob, sKey) 
  ) }keyB );

  // Note that at this point we can't trust nonceS', because
  // it could be a replay attack using an old ticket.
  // We can't trust this message until later, once we issue
  // a nonce challenge to a.

  output socketA is ( { msg4 ( a, nonceB ) }sKey );

  input socketA is ( { msg5 ( 
    nonceS : Challenge, 
    nonceB' : ISO4NonceB (a, Bob, nonceS) 
  ) }sKey );

  // Passing this nonce challenge allows us to trust nonceS:
  check nonceB is nonceB';  

  // Passing this nonce challenge allows us to trust sKey:
  check nonceS is nonceS';  

  end (Sam generated sKey for responder Bob and initiator a);
  end (initiator a contacts responder Bob);

}

/*
 * The intermediary.
 */

server Intermediary at Sam is (socketA : Socket) {

  input socketA is (a : Host, b : Host, nonceA : Challenge);

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

  new (nonceS : Challenge);
  new (sKey : ISO4SKey (a, b));

  begin (Sam generated sKey for initiator a and responder b);
  begin (Sam generated sKey for responder b and initiator a);

  cast nonceA is (nonceA' : ISO4NonceA (a, b, sKey, nonceS));
  cast nonceS is (nonceS' : ISO4NonceS (a, b, sKey));

  output socketA is (
    { msg2 ( b, sKey, nonceS, nonceA' ) }keyA,
    { msg3 ( a, sKey, nonceS' ) }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