Further cleanup.
This commit is contained in:
parent
52e23f5c86
commit
ab7d37fca2
7
protocols/misc/README.txt
Normal file
7
protocols/misc/README.txt
Normal file
@ -0,0 +1,7 @@
|
||||
|
||||
The protocols in this directory are experimental and are not considered
|
||||
to be stable in any way. Therefore, they should not be used as reference
|
||||
models for experimenting with Scyther. Rather, use the protocols in
|
||||
../SPORE or ../Demo.
|
||||
|
||||
|
@ -1,83 +0,0 @@
|
||||
/*
|
||||
* 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);
|
||||
|
@ -1,34 +0,0 @@
|
||||
/* default includes */
|
||||
|
||||
/* asymmetric */
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys (pk,sk);
|
||||
inversekeys (hash,unhash);
|
||||
|
||||
|
||||
/* symmetric */
|
||||
|
||||
usertype SessionKey;
|
||||
secret k: Function;
|
||||
|
||||
/* agents */
|
||||
|
||||
const a,b,e: Agent;
|
||||
|
||||
|
||||
/* untrusted e */
|
||||
|
||||
untrusted e;
|
||||
compromised sk(e);
|
||||
const ne: Nonce;
|
||||
const kee: SessionKey;
|
||||
|
||||
compromised k(e,e);
|
||||
compromised k(e,a);
|
||||
compromised k(e,b);
|
||||
compromised k(a,e);
|
||||
compromised k(b,e);
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user