andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Added a strange issue, to be resolved tomorrow.

Browse Source
This commit is contained in:
ccremers 2005-05-11 15:18:32 +00:00
parent 0930556f2e
commit 2e4c5afeb7
1 changed files with 83 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

83
spdl/problems-johanselst.spdl Normal file
View File

@ -0,0 +1,83 @@
/*
* Some authentication protocol
*
* Version by Johan Selst. Seems to segfault at a simple -r4 execution
* with the modelchecker.
*
* Reported on 2005-05-11.
*/
// PKI infrastructure
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
// The protocol description
protocol as3a(X, I, Y)
{
role X
{
var nix: Nonce;
read_1(I, X, nix);
send_2(X, I, {I,nix}sk(X));
}
role I
{
const nix, niy: Nonce;
send_1(I, X, nix);
read_2(X, I, {I,nix}sk(X));
send_3(I, Y, niy);
read_4(Y, I, {niy,I}sk(Y));
claim_i1(I, Nisynch);
}
role Y
{
var niy: Nonce;
read_3(I, Y, niy);
send_4(Y, I, {niy,I}sk(Y));
}
}
// The trusted agents in the system
const Alice,Bob,Carol: Agent;
// An untrusted agent, with leaked information
const Eve: Agent;
untrusted Eve;
compromised sk(Eve);
// The runs (only needed for the modelchecker algorithm)
run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);
run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);
run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);
run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);
run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);
run as3a.X(Agent,Agent,Agent);
run as3a.I(Agent,Agent,Agent);
run as3a.Y(Agent,Agent,Agent);