/* 
 * PKMv2-SA-TEK
 *
 * Initial model by:	Sjouke Mauw, Sasa Radomirovic (2007)
 * Model changes:	Cas Cremers (Nov 2012)
 *
 * Analysed in:		"A framework for compositional verification of security protocols"
 * 			With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic.
 * 			Information and Computation, Special issue on Computer Security: 
 * 			Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459,
 * 			Elsevier, 2008. 
 */

// Setup

hashfunction hash;
hashfunction prepak;
const akid;
const u,d;

// The protocol description

protocol pkmv2satek(MS,BS)
{
  role MS
  {
    fresh msrand': Nonce;
    var bsrand', tek0, tek1: Nonce;

    recv_satek1(BS,MS, bsrand',akid,
      hash(d,prepak(MS,BS),BS,MS,bsrand',akid) );
    send_satek2(MS,BS, msrand',bsrand',akid,
      hash(u,prepak(MS,BS),BS,MS,msrand',bsrand',akid) );
    recv_satek3(BS,MS,
    msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS)),
      hash(d,prepak(MS,BS),msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS))));

    claim_rsai3(MS,Niagree);
    claim_rsai4(MS,Nisynch);
    claim_rsai6(MS,SKR,tek0);
    claim_rsai7(MS,SKR,tek1);
  } 
  
  role BS
  {
    var msrand': Nonce;
    fresh bsrand', tek0, tek1: Nonce;

    send_satek1(BS,MS, bsrand',akid,
      hash(d,prepak(MS,BS),BS,MS,bsrand',akid) );
    recv_satek2(MS,BS, msrand',bsrand',akid,
      hash(u,prepak(MS,BS),BS,MS,msrand',bsrand',akid) );
    send_satek3(BS,MS,
    msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS)),
      hash(d,prepak(MS,BS),msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS))));

    claim_rsar3(BS,Niagree);
    claim_rsar4(BS,Nisynch);
    claim_rsar6(BS,SKR,tek0);
    claim_rsar7(BS,SKR,tek1);
  }
}