64 lines
1.7 KiB
Plaintext
64 lines
1.7 KiB
Plaintext
|
/*
|
||
|
|
* 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);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|