/*
 * This is a version of the ISO 5-pass Authentication Protocol.
 * It's in Clark and Jacobs (1997) 6.3.9.
 * The original protocol, modified to include message tags,
 * stripping out the extraneous payload messages,
 * and correcting what appear to be some typos (e.g. Alice never sends
 * Bob her name, so Bob has no idea who contacted him):
 *
 *   A -> B : A, Na
 *   B -> S : A, Na, B, Nb1
 *   S -> B : { msg3b(A, Kab, Nb1) }Kbs, { msg3a(B, Kab, Na) }Kas
 *   B -> A : { msg3a(B, Kab, Na) }Kas, { msg4(Na, Nb2) }Kab
 *   A -> B : { msg5(Na, Nb2) }Kab
 * 
 * This protocol is astoundingly similar to Carlsen's Secret Key
 * Initiator Protocol (in carlsen.cry).  The only differences are
 * that msg4 includes Nb2, and that msg5 includes Na.
 *
 * We cannot verify this protocol, for the same reason as for 
 * Carlsen's protocol --  Na is being used twice: 
 * once to verify the freshness of Kab, and once to establish
 * that Bob has sent using Kab.  We can verify a modified version,
 * where we split Na into two nonces, one for each role:
 *
 *   A -> B : A, Na1, Na2
 *   B -> S : A, Na1, B, Nb1
 *   S -> B : { msg3b(A, Kab, Nb1) }Kbs, { msg3a(B, Kab, Na1) }Kas
 *   B -> A : { msg3a(B, Kab, Na1) }Kas, { msg4(Na2, Nb2) }Kab
 *   A -> B : { msg5(Na2, Nb2) }Kab
 * 
 * Alan Jeffrey, v0.0.1 2001/03/10
 */

/*
 * 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 acknowledges : Word;

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

type ISO5SNonceA (a : Host, b : Host)
  = Nonce ( end ( responder b acknowledges initiator a ) );

type ISO5SNonceB (a : Host, b : Host)
  = Nonce ( end ( initiator a acknowledges responder b ) );

type ISO5SMsg4 (a : Host, b : Host)
  = Struct ( nonceA2' : ISO5SNonceA (a, b), nonceB2 : Challenge );

type ISO5SMsg5 (a : Host, b : Host)
  = Struct ( nonceA2' : ISO5SNonceA (a, b), nonceB2' : ISO5SNonceB (a, b) );

type ISO5SMsg (a : Host, b : Host)
  = Union ( msg4 : ISO5SMsg4 (a, b), msg5 : ISO5SMsg5 (a, b) );

type ISO5SKey (a : Host, b : Host)
  = Key (ISO5SMsg (a, b));

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

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

type ISO5Msg3a (a : Host)
  = Struct ( b : Host, sKey : ISO5SKey (a, b), nonceA1' : ISO5NonceA (a, b, sKey) );

type ISO5Msg3b (b : Host)
  = Struct ( a : Host, sKey : ISO5SKey (a, b), nonceB1' : ISO5NonceB (a, b, sKey) );

type ISO5Msg (h : Host) 
  = Union ( msg3a : ISO5Msg3a (h), msg3b : ISO5Msg3b (h) );

type ISO5Key (h : Host) 
  = Key (ISO5Msg (h));

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

type ISO5KDCMsg 
  = Struct (h : Host, keyH : ISO5Key (h));

type ISO5KDCKey 
  = Key (ISO5KDCMsg);

/*
 * The shared keys.
 */

private keyA : ISO5Key (Alice);
private keyB : ISO5Key (Bob);
private keyKDC : ISO5KDCKey;

/*
 * The initiator.
 */

client Initiator at Alice is {

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

  establish Responder at Bob is (socket : Socket);
  output socket is (Alice, nonceA1, nonceA2);

  input socket is ( 
    { msg3a (
      Bob, 
      sKey : ISO5SKey (Alice, Bob), 
      nonceA1' : ISO5NonceA (Alice, Bob, sKey)
    ) }keyA, 
    ticket : Un
  );

  decrypt ticket is ( { msg4 ( 
    nonceA2' : ISO5SNonceA (Alice, Bob),
    nonceB2 : Challenge 
  ) }sKey );

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

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

  begin (initiator Alice acknowledges responder Bob);

  cast nonceB2 is (nonceB2' : ISO5SNonceB (Alice, Bob) );
  output socket is ( { msg5 ( nonceA2', nonceB2' ) }sKey );  

  end (responder Bob acknowledges initiator Alice);

}

/*
 * The responder.
 */

server Responder at Bob is (socketA : Socket) {

  establish Intermediary at Sam is (socketS : Socket);

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

  input socketA is (a : Host, nonceA1 : Challenge, nonceA2 : Challenge);
  output socketS is (a, nonceA1, Bob, nonceB1);
  input socketS is (
    { msg3b (
      a, 
      sKey : ISO5SKey (a, Bob), 
      nonceB1' : ISO5NonceB (a, Bob, sKey)
    ) }keyB,
    ticket : Un);
  check nonceB1 is nonceB1';

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

  begin (responder Bob acknowledges initiator a);

  cast nonceA2 is (nonceA2' : ISO5SNonceA (a, Bob) );
  output socketA is ( ticket, { msg4 ( nonceA2', nonceB2 ) }sKey );
  input socketA is ( { msg5 ( nonceA2', nonceB2' : ISO5SNonceB (a, Bob) ) }sKey );
  check nonceB2 is nonceB2';

  end (initiator a acknowledges responder Bob);


}

/*
 * The intermediary.
 */

server Intermediary at Sam is (socketB : Socket) {

  input socketB is (a : Host, nonceA1 : Challenge, b : Host, nonceB1 : Challenge);

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

  new (sKey : ISO5SKey (a, b));

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

  cast nonceA1 is (nonceA1' : ISO5NonceA (a, b, sKey));
  cast nonceB1 is (nonceB1' : ISO5NonceB (a, b, sKey));

  output socketB is (
    { msg3b ( a, sKey, nonceB1' ) }keyB,
    { msg3a ( b, sKey, nonceA1' ) }keyA
  );

}

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