47 lines
967 B
Plaintext
47 lines
967 B
Plaintext
# SmartRight view-only
|
|
#
|
|
# Modelled after the description in the SPORE library
|
|
# http://www.lsv.ens-cachan.fr/spore/smartright_viewonly.html
|
|
#
|
|
# Note:
|
|
# According to SPORE there are no known attacks on this protocol
|
|
#
|
|
# Note:
|
|
# Scyther finds an attack because the value of VoR in te last message can
|
|
# be replaced with an arbitrary value
|
|
|
|
hashfunction hash;
|
|
usertype SessionKey;
|
|
usertype XorKey;
|
|
const Vor: XorKey;
|
|
|
|
protocol smartright(I,R)
|
|
{
|
|
role I
|
|
{
|
|
fresh VoKey: SessionKey;
|
|
fresh VoR: XorKey;
|
|
fresh CW;
|
|
var VoRi: Nonce;
|
|
|
|
send_1(I,R, {VoKey,{CW}VoR}k(I,R));
|
|
recv_2(R,I, VoRi);
|
|
send_3(I,R, VoR, {{VoRi}hash}VoKey);
|
|
}
|
|
|
|
role R
|
|
{
|
|
var T: Ticket;
|
|
var VoR: XorKey;
|
|
var VoKey: SessionKey;
|
|
fresh VoRi: Nonce;
|
|
|
|
recv_1(I,R, {VoKey,T}k(I,R));
|
|
send_2(R,I, VoRi);
|
|
recv_3(I,R, VoR,{{VoRi}hash}VoKey);
|
|
|
|
claim_R1(R,Nisynch);
|
|
}
|
|
}
|
|
|