scyther/protocols/misc/splice-as.spdl

60 lines
1012 B
Plaintext
Raw Normal View History

2006-11-21 13:40:50 +00:00
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol spliceAS(C,AS,S)
{
role C
{
fresh N1,N2: Nonce;
fresh T: TimeStamp;
fresh L: LifeTime;
2006-11-21 13:40:50 +00:00
send_1(C,AS, C, S, N1 );
2012-05-02 22:26:41 +01:00
recv_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) );
2006-11-21 13:40:50 +00:00
send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
2012-05-02 22:26:41 +01:00
recv_6(S,C, S, C, {S, N2}pk(C) );
2006-11-21 13:40:50 +00:00
claim_7(C, Secret, N2);
claim_9(C, Niagree);
claim_10(C, Nisynch);
}
role AS
{
var N1,N3: Nonce;
2012-05-02 22:26:41 +01:00
recv_1(C,AS, C, S, N1 );
2006-11-21 13:40:50 +00:00
send_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) );
2012-05-02 22:26:41 +01:00
recv_4(S,AS, S, C, N3 );
2006-11-21 13:40:50 +00:00
send_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) );
}
role S
{
fresh N3: Nonce;
2006-11-21 13:40:50 +00:00
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
fresh nr: Nonce;
2006-11-21 13:40:50 +00:00
2012-05-02 22:26:41 +01:00
recv_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
2006-11-21 13:40:50 +00:00
send_4(S,AS, S, C, N3 );
2012-05-02 22:26:41 +01:00
recv_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) );
2006-11-21 13:40:50 +00:00
send_6(S,C, S, C, {S, N2}pk(C) );
claim_8(S, Secret, N2);
claim_11(S, Niagree);
claim_12(S, Nisynch);
}
}