/* 
 * This is the complete Needham-Schroeder-Lowe Protocol. 
 * 
 *   A -> S : A,B
 *   S -> A : {| msgKey(pkB,B) |}sS
 *   A -> B : {| msg1(Na,A) |}pB
 *   B -> S : B,A
 *   S -> B : {| msgKey(pkA,A) |}sS
 *   B -> A : {| msg2(Na,Nb,B) |}pA
 *   A -> B : {| msg3(Nb) |}pB   
 *
 * Christian Haack, v1.1.0 2004/10/11
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public acknowledging : Word;
public receipt : Word;
public of : Word;
public nonce : Word;
public to : Word;

/*
 * Nonce types.
 */

type ChallengeAToB 
  = SoshChall ();

type ResponseBToA ( a:Any, b:Any, na:Any )
  = SoshResp ( begun(b acknowledging to a receipt of nonce na) ); 

type ChallengeBToA ( a:Any, b:Any, nb:Any )
  = SophChall ( begun(a acknowledging to b receipt of nonce nb) );

type ResponseAToB 
  = SophResp ();

/*
 * Message patterns.
 */

pattern MsgKey 
  = ( PublicKey(p), p:Un );

pattern Msg1  
  = ( ChallengeAToB, Host ); 

pattern Msg2 (a:Any)
  = ( na : ResponseBToA(a,b,na),
      nb : ChallengeBToA(a,b,nb),
      b : Host );

pattern Msg3 
  = ResponseAToB;

/* 
 * Message tags.
 */

tag msgKey (MsgKey) : Auth <s:Server>;
tag msg1 (Msg1) : Auth (b:Any);  
tag msg2 (Msg2(a)) : Auth (a:Any);
tag msg3 (Msg3) : Auth (b:Any);

/*
 * The initiator.
 */

client Initiator 
  (a:Host, b:Host, s:Server, sS:AuthKey(s), pA:PrivateKey(a)) 
  at a is 
{
  establish Server at s is (socketS : Socket);
  output socketS is (a,b);
  input socketS is {| msgKey( pB:PublicKey(b), b) |}sS^-1;	
  establish Responder at b is (socketB : Socket);
  new (na : ChallengeAToB);
  output socketB is {| msg1(na,a) |}pB;
  input socketB is {| msg2 (na, nb:ChallengeBToA(a,b,nb), b) |}pA^-1
    [ begun (b acknowledging to a receipt of nonce na) ];
  end (b acknowledging to a receipt of nonce na);
  begin (a acknowledging to b receipt of nonce nb);
  output socketB is {| msg3(nb) |}pB;
}
	 
/*
 * The responder.
 */

server Responder 
   (b:Host, s:Server, sS:AuthKey(s), pB:PrivateKey(b)) 
   at b is (socket : Socket) 
{
  input socket is {| msg1 (na:ChallengeAToB, a:Un) |}pB^-1;
  establish Server at s is (socketS : Socket);
  output socketS is (b,a); 
  input socket is {| msgKey( pA:PublicKey(a), a ) |}sS^-1;
  new (nb : ChallengeBToA(a,b,nb));
  begin (b acknowledging to a receipt of nonce na);
  output socket is {| msg2(na,nb,b) |}pA;
  input socket is {| msg3(nb) |}pB^-1 
    [ begun (a acknowledging to b receipt of nonce nb) ];
  end (a acknowledging to b receipt of nonce nb);
}

/*
 * The Public Key Server.
 */

/*
 * We assume that the public key server is able to securely lookup public 
 * keys. We formally express this by assuming the existence of a secure 
 * lookup function of the following dependent function type:
 */

fun lkupKey (p:Any) : PublicKey(p);

server KeyServer (s:Server, sS:SignKey(s)) at s is (socket : Socket)
{
  input socket is (p:Un,q:Un);
  let pP:PublicKey(p) = lkupKey (p);
  output socket is {| msgKey(pP,p) |}sS;
}

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