scyther/testing/tls/tls-HSDDM05-2.spdl

# 1 "tls-HSDDM05-2.cpp"
# 1 "<built-in>"
# 1 "<command line>"
# 1 "tls-HSDDM05-2.cpp"
# 34 "tls-HSDDM05-2.cpp"
usertype Params, String;

const pk,hash: Function;
secret sk,unhash: Function;
inversekeys(pk,sk);
inversekeys(hash,unhash);

const clientstring,serverstring: String;

const Alice, Bob, Eve: Agent;
const Terence: Agent;

protocol tls-HSDDM05(X,Y)
{
 role X
 {
  fresh Nx: Nonce;
  fresh msecret: Nonce;
  fresh pa: Params;
  var Ny: Nonce;
  var pb: Params;

  send_1( X,Y, X,Nx,pa );
  recv_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
  send_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) );
  recv_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) );

  claim_X1( X, Secret, msecret );
 }

 role Y
 {
  var Nx: Nonce;
  var msecret: Nonce;
  var pa: Params;
  fresh Ny: Nonce;
  fresh pb: Params;

  recv_1( X,Y, X,Nx,pa );
  send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
  recv_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) );
  send_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) );

  claim_Y1( Y, Secret, msecret );
 }
}