scyther/spdl/broken1.spdl

40 lines
696 B
Plaintext
Raw Normal View History

/*
* A broken protocol
*
* Cas Cremers
* Visualization challenge of the week.
* Can be checked withouth CL, please do so.
*/
usertype String, Key;
const PlainSight: String;
secret HelloWorld, HelloServer: String;
secret k: Key;
2004-04-01 11:05:00 +01:00
protocol broken1(I,R,S)
{
2004-04-01 11:05:00 +01:00
role I
{
2004-04-01 11:05:00 +01:00
send_1(I, R, PlainSight, {HelloWorld, I, R}k );
send_2(I, S, {HelloServer, I, S}k );
}
2004-04-01 11:05:00 +01:00
role R
{
2004-04-01 11:05:00 +01:00
read_3(S, R, {HelloWorld, S, I, R}k );
read_1(I, R, PlainSight, {HelloWorld, I, R}k );
claim(R, Secret, PlainSight);
}
2004-04-01 11:05:00 +01:00
role S
{
2004-04-01 11:05:00 +01:00
read_2(I, S, {HelloServer, I, S}k );
send_3(S, R, {HelloWorld, S, I, R}k );
}
}
2004-04-01 11:05:00 +01:00
const a, b, S: Agent;
2004-04-01 11:05:00 +01:00
run broken1.I(a, b, S);
run broken1.R(a, b, S);
run broken1.S(a, b, S);