/* 
 *   A -> B : {| msg1(Na,A) |}pkB
 *   B -> A : {| msg2(Na,Nb,M,B) |}pkA
 *   A -> B : {| msg3(Nb) |}pkB   
 *
 *   NSL extended with a secret M that B sends to A.
 *   Here it is important that the nonce response Na from B to A is 
 *   encrypted together with M. The response Nb from A to B may be
 *   sent in the open, though. (See nsl-with-secret-optimized.cry.)
 *
 *   Christian Haack, v.1.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 ChallengeAToB 
  = SoshChall ();

type ResponseBToA (a:Public, b:Public, m:Any)
  = SoshResp ( begun(b authenticating m to a), m:Private ); 

type ChallengeBToA (a:Public, b:Public)
  = SophChall ( begun(a authenticating to b) );

type ResponseAToB 
  = SophResp ();

/* Message patterns. */
pattern Msg1  
  = ( ChallengeAToB, Public ); 

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

pattern Msg3 
  = ResponseAToB;

/* Message tags. */
tag msg1 (Msg1) : 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 : ChallengeAToB);
  output socket is {| msg1(na,a) |}pB;
  input socket is {| msg2 (na, nb:ChallengeBToA(a,b), m:Private, b) |}pA^-1
    [ begun (b authenticating m to a) ]; 
  end (b authenticating m 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:ChallengeAToB, a) |}pB^-1;
  new (m : Private);
  new (nb : ChallengeBToA(a,b));
  begin (b authenticating m to a);
  output socket is {| msg2(na,nb,m,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 06:53:58