/* 
 *   A -> B : {| msg1(Na,A) |}pkB
 *   B -> A : {| msg2(Na,Nb,B) |}pkA
 *   A -> B : {| msg3(Nb) |}pkB   
 *
 * The three-message version of Needham-Schroeder-Lowe.
 *
 * Christian Haack, v1.1.0, 2006/2/20 
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public authenticating : Word;
public to : Word;

/* Nonce types. */
type Challenge (a:Public, b:Public)
  = SophChall ( begun(b authenticating to a) );

type Response
  = SophResp ();

/* Message patterns. */
pattern Msg1 (b:Public) 
  = ( Challenge(a,b), a:Public ); 

pattern Msg2 (a:Public)
  = ( na : Response,
      nb : Challenge(b,a),
      b : Public );

pattern Msg3 
  = Response;

/* Message tags. */
tag msg1 (Msg1(b)) : Auth (b:Public);  
tag msg2 (Msg2(a)) : Auth (a:Public);
tag msg3 (Msg3) : Auth (b:Public);

client Initiator (a:Public, pA:PrivateKey(a), b:Public, pB:PublicKey(b)) 
  at a is 
{
  establish Responder at b is (socket : Socket);
  new (na : Challenge(a,b));
  output socket is {| msg1(na,a) |}pB;
  input socket is {| msg2 (na, nb:Challenge(b,a), b) |}pA^-1
    [ begun (b authenticating to a) ]; 
  end (b authenticating to a);
  begin (a authenticating to b);
  output socket is {| msg3(nb) |}pB;
}
	 
server Responder (b:Public, pB:PrivateKey(b), a:Public, pA:PublicKey(a)) 
  at b is (socket : Socket) 
{
  input socket is {| msg1 (na:Challenge(a,b), a) |}pB^-1;
  new (nb : Challenge(b,a));
  begin (b authenticating to a);
  output socket is {| msg2(na,nb,b) |}pA;
  input socket is {| msg3(nb) |}pB^-1 
    [ begun (a authenticating to b) ];	
  end (a authenticating to b);
}

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: 2006-02-20 04:56:41