Moved development protocol files to a better named directory.
This commit is contained in:
Cas Cremers
@@ -1,41 +0,0 @@
|
||||
/*
|
||||
* Needham-Schroeder protocol
|
||||
*/
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol ns3(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,40 +0,0 @@
|
||||
/*
|
||||
* Needham-Schroeder-Lowe protocol,
|
||||
* broken version (wrong role name in first message)
|
||||
*/
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol nsl3-broken(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {R,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {R,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,78 +0,0 @@
|
||||
/*
|
||||
* Needham-Schroeder-Lowe protocol,
|
||||
* broken version (wrong role name in first message)
|
||||
*/
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol nsl3-broken(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {R,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {R,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
* Needham-Schroeder-Lowe protocol
|
||||
*/
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol nsl3(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
@@ -1,38 +0,0 @@
|
||||
/*
|
||||
* Needham-Schroeder-Lowe protocol
|
||||
*/
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol nsl3(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
@@ -1,48 +0,0 @@
|
||||
/*
|
||||
* Course 2r890
|
||||
*
|
||||
* Assignment 0405-3
|
||||
*
|
||||
* Protocol a
|
||||
*
|
||||
* nisynch, niagree
|
||||
*/
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol course2r890year0405ex3(X,Y,I)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh nx: Nonce;
|
||||
fresh ny: Nonce;
|
||||
|
||||
send_1(I,X, nx );
|
||||
recv_2(X,I, { I,nx }sk(X) );
|
||||
send_3(I,Y, ny );
|
||||
recv_4(Y,I, { ny,I }sk(Y) );
|
||||
|
||||
claim_i1(I,Niagree);
|
||||
claim_i2(I,Nisynch);
|
||||
}
|
||||
|
||||
role X
|
||||
{
|
||||
var nx: Nonce;
|
||||
|
||||
recv_1(I,X, nx );
|
||||
send_2(X,I, { I,nx }sk(X) );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var ny: Nonce;
|
||||
|
||||
recv_3(I,Y, ny );
|
||||
send_4(Y,I, { ny,I }sk(Y) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,47 +0,0 @@
|
||||
/*
|
||||
* Course 2r890
|
||||
*
|
||||
* Assignment 0405-3
|
||||
*
|
||||
* Protocol b
|
||||
*
|
||||
* not nisynch, but still niagree
|
||||
*/
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol course2r890year0405ex3(X,Y,I)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
send_1(I,X, ni );
|
||||
recv_2(X,I, { I,ni }sk(X) );
|
||||
send_3(I,Y, ni );
|
||||
recv_4(Y,I, { ni,I }sk(Y) );
|
||||
|
||||
claim_i1(I,Niagree);
|
||||
claim_i2(I,Nisynch);
|
||||
}
|
||||
|
||||
role X
|
||||
{
|
||||
var nx: Nonce;
|
||||
|
||||
recv_1(I,X, nx );
|
||||
send_2(X,I, { I,nx }sk(X) );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var ny: Nonce;
|
||||
|
||||
recv_3(I,Y, ny );
|
||||
send_4(Y,I, { ny,I }sk(Y) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,7 +0,0 @@
|
||||
|
||||
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,41 +0,0 @@
|
||||
usertype SessionKey;
|
||||
secret k: Function;
|
||||
|
||||
protocol andrewBan(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr,nr2: Nonce;
|
||||
var kir: SessionKey;
|
||||
|
||||
send_1(I,R, I,{ni}k(I,R) );
|
||||
recv_2(R,I, {ni,nr}k(I,R) );
|
||||
send_3(I,R, {nr}k(I,R) );
|
||||
recv_4(R,I, {kir,nr2,ni}k(I,R) );
|
||||
claim_5(I,Nisynch);
|
||||
claim_5b(I,Niagree);
|
||||
claim_6(I,Secret, kir);
|
||||
claim_7(I,Secret, k(I,R));
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr,nr2: Nonce;
|
||||
fresh kir: SessionKey;
|
||||
|
||||
recv_1(I,R, I,{ni}k(I,R) );
|
||||
send_2(R,I, {ni,nr}k(I,R) );
|
||||
recv_3(I,R, {nr}k(I,R) );
|
||||
send_4(R,I, {kir,nr2,ni}k(I,R) );
|
||||
claim_8(R,Nisynch);
|
||||
claim_8b(R,Niagree);
|
||||
claim_9(R,Secret, kir);
|
||||
claim_10(R,Secret, k(I,R));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const kee: SessionKey;
|
||||
|
||||
@@ -1,41 +0,0 @@
|
||||
usertype SessionKey;
|
||||
secret k: Function;
|
||||
|
||||
protocol andrewLoweBan(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: SessionKey;
|
||||
|
||||
send_1(I,R, I,ni );
|
||||
recv_2(R,I, {ni,kir,I}k(I,R) );
|
||||
send_3(I,R, {ni}kir );
|
||||
recv_4(R,I, nr );
|
||||
claim_5(I,Nisynch);
|
||||
claim_5b(I,Niagree);
|
||||
claim_6(I,Secret, kir);
|
||||
claim_7(I,Secret, k(I,R));
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh kir: SessionKey;
|
||||
|
||||
recv_1(I,R, I,ni );
|
||||
send_2(R,I, {ni,kir,I}k(I,R) );
|
||||
recv_3(I,R, {ni}kir );
|
||||
send_4(R,I, nr );
|
||||
claim_8(R,Nisynch);
|
||||
claim_8b(R,Niagree);
|
||||
claim_9(R,Secret, kir);
|
||||
claim_10(R,Secret, k(I,R));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const kee: SessionKey;
|
||||
|
||||
@@ -1,39 +0,0 @@
|
||||
/*
|
||||
* Athena breaker protocol
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol abreaker(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
send_!1(I,R, {{I,ni}pk(R)}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var T:Ticket;
|
||||
|
||||
recv_!1(I,R, {T}pk(R) );
|
||||
send_!2(R,I, T );
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
// The agents in the system
|
||||
|
||||
|
||||
// An untrusted agent, with leaked information
|
||||
|
||||
|
||||
@@ -1,44 +0,0 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (bkebroken)
|
||||
Broken version with man in the middle attack.
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk,h: Function;
|
||||
secret sk,hinv: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
inversekeys (h,hinv);
|
||||
|
||||
protocol bkebroken(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Key;
|
||||
|
||||
send_1 (I,R, { ni,I }pk(R) );
|
||||
recv_2 (R,I, { h(ni),nr,kir }pk(I) );
|
||||
send_3 (I,R, { h(nr),kir }pk(R) );
|
||||
claim_4 (I, Secret, kir );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh kir: Key;
|
||||
|
||||
recv_1 (I,R, { ni,I }pk(R) );
|
||||
send_2 (R,I, { h(ni),nr,kir }pk(I) );
|
||||
recv_3 (I,R, { h(nr),kir }pk(R) );
|
||||
claim_5 (R, Secret, kir );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
untrusted e;
|
||||
compromised sk(e);
|
||||
|
||||
@@ -1,46 +0,0 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (bkeONE)
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
inversekeys (hash,unhash);
|
||||
|
||||
protocol bkeONE(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Key;
|
||||
|
||||
send_1 (I,R, { ni,I }pk(R) );
|
||||
recv_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
|
||||
send_3 (I,R, { hash(nr) }kir );
|
||||
claim_4 (I, Secret, kir );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh kir: Key;
|
||||
|
||||
recv_1 (I,R, { ni,I }pk(R) );
|
||||
send_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
|
||||
recv_3 (I,R, { hash(nr) }kir );
|
||||
claim_5 (R, Secret, kir );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
untrusted e;
|
||||
compromised sk(e);
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,49 +0,0 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (BKEPK)
|
||||
Variation for exercise 2r890
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
inversekeys (hash,unhash);
|
||||
|
||||
protocol bkevariation(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Key;
|
||||
|
||||
send_1 (I,R, { ni,I }pk(R) );
|
||||
recv_2 (R,I, { hash(ni),nr,kir }pk(I) );
|
||||
send_3 (I,R, { hash(nr) }kir );
|
||||
claim_4 (I, Secret, kir );
|
||||
claim_5 (I, Niagree );
|
||||
claim_6 (I, Nisynch );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh kir: Key;
|
||||
|
||||
recv_1 (I,R, { ni,I }pk(R) );
|
||||
send_2 (R,I, { hash(ni),nr,kir }pk(I) );
|
||||
recv_3 (I,R, { hash(nr) }kir );
|
||||
claim_7 (R, Secret, kir );
|
||||
claim_8 (R, Niagree );
|
||||
claim_9 (R, Nisynch );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
untrusted e;
|
||||
compromised sk(e);
|
||||
|
||||
|
||||
@@ -1,46 +0,0 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (BKEPK)
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
hashfunction hash;
|
||||
|
||||
protocol bke(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Key;
|
||||
|
||||
send_1 (I,R, { ni,I }pk(R) );
|
||||
recv_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
|
||||
send_3 (I,R, { hash(nr) }kir );
|
||||
claim_4 (I, Secret, kir );
|
||||
claim_5 (I, Niagree );
|
||||
claim_6 (I, Nisynch );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh kir: Key;
|
||||
|
||||
recv_1 (I,R, { ni,I }pk(R) );
|
||||
send_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
|
||||
recv_3 (I,R, { hash(nr) }kir );
|
||||
claim_7 (R, Secret, kir );
|
||||
claim_8 (R, Niagree );
|
||||
claim_9 (R, Nisynch );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
untrusted e;
|
||||
compromised sk(e);
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,51 +0,0 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (bkeCE)
|
||||
|
||||
Version from Corin/Etalle: An Improved Constraint-Based System for the Verification of Security Protocols.
|
||||
Tried to stay as close as possible to compare timing results.
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
inversekeys (hash,unhash);
|
||||
|
||||
protocol bkeCE(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var nb: Nonce;
|
||||
fresh na: Nonce;
|
||||
fresh kab: Key;
|
||||
|
||||
recv_1 (B,A, B,{ nb,B }pk(A) );
|
||||
send_2 (A,B, { hash(nb),na,A,kab }pk(B) );
|
||||
recv_3 (B,A, { hash(na) }kab );
|
||||
|
||||
claim_A1 (A, Secret, na);
|
||||
claim_A2 (A, Secret, nb);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
fresh nb: Nonce;
|
||||
var na: Nonce;
|
||||
var kab: Key;
|
||||
|
||||
send_1 (B,A, B,{ nb,B }pk(A) );
|
||||
recv_2 (A,B, { hash(nb),na,A,kab }pk(B) );
|
||||
send_3 (B,A, { hash(na) }kab );
|
||||
|
||||
claim_B1 (B, Secret, na);
|
||||
claim_B2 (B, Secret, nb);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve;
|
||||
|
||||
|
||||
|
||||
@@ -1,51 +0,0 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (bkepkCE2)
|
||||
|
||||
Version from Corin/Etalle: An Improved Constraint-Based System for the Verification of Security Protocols.
|
||||
Tried to stay as close as possible to compare timing results.
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol bkepkCE2(A,B,testnonce)
|
||||
{
|
||||
role B
|
||||
{
|
||||
fresh nb: Nonce;
|
||||
var na: Nonce;
|
||||
var kab: Key;
|
||||
|
||||
send_1 (B,A, B,{ nb,B }pk(A) );
|
||||
recv_2 (A,B, { hash(nb),na,A,kab }pk(B) );
|
||||
send_3 (B,A, { hash(na) }kab );
|
||||
}
|
||||
|
||||
role A
|
||||
{
|
||||
var nb: Nonce;
|
||||
fresh na: Nonce;
|
||||
fresh kab: Key;
|
||||
|
||||
recv_1 (B,A, B,{ nb,B }pk(A) );
|
||||
send_2 (A,B, { hash(nb),na,A,kab }pk(B) );
|
||||
recv_3 (B,A, { hash(na) }kab );
|
||||
}
|
||||
|
||||
role testnonce
|
||||
{
|
||||
var n: Nonce;
|
||||
|
||||
recv_!4 (testnonce,testnonce, n);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve;
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,49 +0,0 @@
|
||||
/*
|
||||
* Boyd fix for NS(L)
|
||||
*
|
||||
* From the paper "Towards Extensional Goals in Authentication
|
||||
* Protocols"
|
||||
*
|
||||
* Broken. Best shown by attack id 4.
|
||||
*/
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
const hash: Function;
|
||||
secret unhash: Function;
|
||||
inversekeys (hash,unhash);
|
||||
|
||||
protocol boydNS(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {ni}pk(R),I );
|
||||
recv_2(R,I, {nr}pk(I),hash(ni,R) );
|
||||
send_3(I,R, hash(nr, I,R) );
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {ni}pk(R),I );
|
||||
send_2(R,I, {nr}pk(I),hash(ni,R) );
|
||||
recv_3(I,R, hash(nr, I,R) );
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,60 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
usertype Macseed;
|
||||
const m: Function;
|
||||
secret unm: Function;
|
||||
const f: Function;
|
||||
|
||||
inversekeys (m, unm);
|
||||
|
||||
/*
|
||||
* Boyd key agreement
|
||||
*
|
||||
* Boyd & Mathuria: Protocols for authentication and key establishment
|
||||
* (2003) p. 101
|
||||
*
|
||||
* Note that MAC_ks(x) has been interpreted as MAC(x,ks); this
|
||||
* assumption causes some possible false attacks.
|
||||
*/
|
||||
|
||||
protocol boyd(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var ks: Macseed;
|
||||
|
||||
send_1 (I,S, I,R, ni );
|
||||
recv_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr );
|
||||
send_4 (I,R, m(nr, m(ks,ni,nr)) );
|
||||
|
||||
claim_6 (I, Secret, m(ks,ni,nr) );
|
||||
claim_7 (I, Niagree);
|
||||
claim_8 (I, Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
var ks: Macseed;
|
||||
|
||||
recv_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni );
|
||||
send_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr );
|
||||
recv_4 (I,R, m(nr, m(ks,ni,nr)) );
|
||||
|
||||
claim_10 (R, Secret, m(ks,ni,nr));
|
||||
claim_11 (R, Niagree);
|
||||
claim_12 (R, Nisynch);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var ni,nr: Nonce;
|
||||
fresh ks: Macseed;
|
||||
|
||||
recv_1 (I,S, I,R, ni );
|
||||
send_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni );
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,39 +0,0 @@
|
||||
/*
|
||||
* 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;
|
||||
|
||||
protocol broken1(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
send_1(I, R, PlainSight, {HelloWorld, I, R}k );
|
||||
send_2(I, S, {HelloServer, I, S}k );
|
||||
}
|
||||
role R
|
||||
{
|
||||
recv_3(S, R, {HelloWorld, S, I, R}k );
|
||||
recv_1(I, R, PlainSight, {HelloWorld, I, R}k );
|
||||
claim_4(R, Secret, PlainSight);
|
||||
}
|
||||
role S
|
||||
{
|
||||
recv_2(I, S, {HelloServer, I, S}k );
|
||||
send_3(S, R, {HelloWorld, S, I, R}k );
|
||||
}
|
||||
}
|
||||
|
||||
const a, b, S: Agent;
|
||||
|
||||
run broken1.I(a, b, S);
|
||||
run broken1.R(a, b, S);
|
||||
run broken1.S(a, b, S);
|
||||
|
||||
@@ -1,74 +0,0 @@
|
||||
# Buttyan Nagy Vajda protocol 1 (3-party)
|
||||
#
|
||||
# Modelled after the description in the paper
|
||||
# "Efficient multi-party challenge-response protocols for entity
|
||||
# authentication"
|
||||
#
|
||||
# Attacks:
|
||||
# Does not satisfy ni-agree, because when Alice in the R0 role terminates
|
||||
# it cannot be sure that the agent in role R1 is aware of having sent a
|
||||
# reply for Alice.
|
||||
# R0 type flaw attack exists in which there are only two agents active.
|
||||
#
|
||||
|
||||
secret k: Function;
|
||||
|
||||
protocol intruderhelp(Swap)
|
||||
{
|
||||
role Swap
|
||||
{
|
||||
var T: Ticket;
|
||||
var R0,R1: Agent;
|
||||
|
||||
recv_!1(Swap,Swap, { T }k(R0,R1) );
|
||||
send_!2(Swap,Swap, { T }k(R1,R0) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol bunava13(R0,R1,R2)
|
||||
{
|
||||
role R0
|
||||
{
|
||||
fresh n0: Nonce;
|
||||
var n1,n2: Nonce;
|
||||
|
||||
send_1(R0,R1, n0);
|
||||
recv_3(R2,R0, n2,{R2,n1,R1,n0}k(R0,R2) );
|
||||
send_4(R0,R1, {R0,n2,R2,n1}k(R0,R1) );
|
||||
|
||||
claim_A1(R0, Niagree);
|
||||
claim_A2(R0, Nisynch);
|
||||
}
|
||||
|
||||
role R1
|
||||
{
|
||||
fresh n1: Nonce;
|
||||
var n0,n2: Nonce;
|
||||
|
||||
recv_1(R0,R1, n0);
|
||||
send_2(R1,R2, n1,{R1,n0}k(R1,R2) );
|
||||
recv_4(R0,R1, {R0,n2,R2,n1}k(R0,R1) );
|
||||
send_5(R1,R2, {R1,R0,n2}k(R1,R2) );
|
||||
|
||||
claim_B1(R1, Niagree);
|
||||
claim_B2(R1, Nisynch);
|
||||
}
|
||||
|
||||
role R2
|
||||
{
|
||||
fresh n2: Nonce;
|
||||
var n0,n1: Nonce;
|
||||
|
||||
recv_2(R1,R2, n1,{R1,n0}k(R1,R2) );
|
||||
send_3(R2,R0, n2,{R2,n1,R1,n0}k(R0,R2) );
|
||||
recv_5(R1,R2, {R1,R0,n2}k(R1,R2) );
|
||||
|
||||
claim_C1(R2, Niagree);
|
||||
claim_C2(R2, Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
# General scenario, 2 parallel runs of the protocol
|
||||
|
||||
@@ -1,89 +0,0 @@
|
||||
# Buttyan Nagy Vajda protocol 1 (4-party)
|
||||
#
|
||||
# Modelled after the description in the paper
|
||||
# "Efficient multi-party challenge-response protocols for entity
|
||||
# authentication"
|
||||
#
|
||||
# Attacks:
|
||||
# Does not satisfy ni-agree, because when Alice in the A role terminates
|
||||
# it cannot be sure that the agent in role B is aware of having sent a
|
||||
# reply for Alice.
|
||||
# A type flaw attack exists in which there are only three agents active.
|
||||
# Especially -m2 attack 17 is nice, I think.
|
||||
#
|
||||
|
||||
secret k: Function;
|
||||
|
||||
protocol intruderhelp(Swap)
|
||||
{
|
||||
role Swap
|
||||
{
|
||||
var T: Ticket;
|
||||
var A,B: Agent;
|
||||
|
||||
recv_!1(Swap,Swap, { T }k(A,B) );
|
||||
send_!2(Swap,Swap, { T }k(B,A) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol bunava14(A,B,C,D)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh ra: Nonce;
|
||||
var rb,rc,rd: Nonce;
|
||||
|
||||
send_1(A,B, ra);
|
||||
recv_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) );
|
||||
send_5(A,B, {A,rd,D,rc,C,rb}k(A,B) );
|
||||
|
||||
claim_A1(A, Niagree);
|
||||
claim_A2(A, Nisynch);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
fresh rb: Nonce;
|
||||
var ra,rc,rd: Nonce;
|
||||
|
||||
recv_1(A,B, ra);
|
||||
send_2(B,C, rb,{B,ra}k(B,C) );
|
||||
recv_5(A,B, {A,rd,D,rc,C,rb}k(A,B) );
|
||||
send_6(B,C, {B,A,rd,D,rc}k(B,C) );
|
||||
|
||||
claim_B1(B, Niagree);
|
||||
claim_B2(B, Nisynch);
|
||||
}
|
||||
|
||||
role C
|
||||
{
|
||||
fresh rc: Nonce;
|
||||
var ra,rb,rd: Nonce;
|
||||
|
||||
recv_2(B,C, rb,{B,ra}k(B,C) );
|
||||
send_3(C,D, rc,{C,rb,B,ra}k(C,D) );
|
||||
recv_6(B,C, {B,A,rd,D,rc}k(B,C) );
|
||||
send_7(C,D, {C,B,A,rd}k(C,D) );
|
||||
|
||||
claim_C1(C, Niagree);
|
||||
claim_C2(C, Nisynch);
|
||||
}
|
||||
|
||||
role D
|
||||
{
|
||||
fresh rd: Nonce;
|
||||
var ra,rb,rc: Nonce;
|
||||
|
||||
recv_3(C,D, rc,{C,rb,B,ra}k(C,D) );
|
||||
send_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) );
|
||||
recv_7(C,D, {C,B,A,rd}k(C,D) );
|
||||
|
||||
claim_D1(D, Niagree);
|
||||
claim_D2(D, Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
# General scenario, 2 parallel runs of the protocol
|
||||
|
||||
@@ -1,73 +0,0 @@
|
||||
# Buttyan Nagy Vajda protocol 2 (3-party)
|
||||
#
|
||||
# Modelled after the description in the paper
|
||||
# "Efficient multi-party challenge-response protocols for entity
|
||||
# authentication"
|
||||
#
|
||||
# Attacks:
|
||||
#
|
||||
|
||||
secret k: Function;
|
||||
|
||||
protocol intruderhelp(Swap)
|
||||
{
|
||||
role Swap
|
||||
{
|
||||
var T: Ticket;
|
||||
var R0,R1: Agent;
|
||||
|
||||
recv_!1(Swap,Swap, { T }k(R0,R1) );
|
||||
send_!2(Swap,Swap, { T }k(R1,R0) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol bunava23(R0,R1,R2)
|
||||
{
|
||||
role R0
|
||||
{
|
||||
fresh n0: Nonce;
|
||||
var n1,n2: Nonce;
|
||||
var T0: Ticket;
|
||||
|
||||
send_1(R0,R1, n0);
|
||||
recv_3(R2,R0, n2, T0, { R2,{ R1,n0 }k(R0,R1) }k(R0,R2) );
|
||||
send_4(R0,R1, { R0,n2 }k(R0,R2), { R0, T0 }k(R0,R1) );
|
||||
|
||||
claim_A1(R0, Niagree);
|
||||
claim_A2(R0, Nisynch);
|
||||
}
|
||||
|
||||
role R1
|
||||
{
|
||||
fresh n1: Nonce;
|
||||
var n0,n2: Nonce;
|
||||
var T1: Ticket;
|
||||
|
||||
recv_1(R0,R1, n0);
|
||||
send_2(R1,R2, n1,{R1,n0}k(R1,R2) );
|
||||
recv_4(R0,R1, T1, { R0, { R2,n1 }k(R1,R2) }k(R0,R1) );
|
||||
send_5(R1,R2, { R1, T1 }k(R1,R2) );
|
||||
|
||||
claim_B1(R1, Niagree);
|
||||
claim_B2(R1, Nisynch);
|
||||
}
|
||||
|
||||
role R2
|
||||
{
|
||||
fresh n2: Nonce;
|
||||
var n0,n1: Nonce;
|
||||
var T2: Ticket;
|
||||
|
||||
recv_2(R1,R2, n1, T2 );
|
||||
send_3(R2,R0, n2,{ R2,n1 }k(R1,R2), { R2, T2 }k(R0,R2) );
|
||||
recv_5(R1,R2, { R1, { R0,n2 }k(R0,R2) }k(R1,R2) );
|
||||
|
||||
claim_C1(R2, Niagree);
|
||||
claim_C2(R2, Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
# General scenario
|
||||
|
||||
@@ -1,121 +0,0 @@
|
||||
# Buttyan Nagy Vajda protocol 2 (4-party)
|
||||
#
|
||||
# Modelled after the description in the paper
|
||||
# "Efficient multi-party challenge-response protocols for entity
|
||||
# authentication"
|
||||
#
|
||||
# Note:
|
||||
# Does not seem to reach the claim. I don't know why yet. TODO
|
||||
# investigate.
|
||||
#
|
||||
|
||||
secret k: Function;
|
||||
|
||||
# protocol intruderhelp(Swap)
|
||||
# {
|
||||
# role Swap
|
||||
# {
|
||||
# var T: Ticket;
|
||||
# var A,B: Agent;
|
||||
#
|
||||
# recv_1(Swap,Swap, { T }k(A,B) );
|
||||
# send_2(Swap,Swap, { T }k(B,A) );
|
||||
# }
|
||||
# }
|
||||
|
||||
protocol bunava24(A,B,C,D)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh ra: Nonce;
|
||||
var rb,rc,rd: Nonce;
|
||||
var Tacd, Tabd: Ticket;
|
||||
|
||||
send_1(A,B, ra);
|
||||
recv_4(D,A, rd,
|
||||
Tacd,
|
||||
Tabd,
|
||||
{ D, { C, { B,ra }k(A,B) }k(A,C) }k(A,D)
|
||||
);
|
||||
# send_5(A,B,
|
||||
# { A, rd }k(A,D),
|
||||
# { A, Tacd }k(A,C),
|
||||
# { A, Tabd }k(A,B)
|
||||
# );
|
||||
|
||||
claim_A1(A, Niagree);
|
||||
claim_A2(A, Nisynch);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
fresh rb: Nonce;
|
||||
var ra,rc,rd: Nonce;
|
||||
var Tbad, Tbac: Ticket;
|
||||
|
||||
recv_1(A,B, ra);
|
||||
send_2(B,C, rb,
|
||||
{ B,ra }k(A,B)
|
||||
);
|
||||
# recv_5(A,B,
|
||||
# Tbad,
|
||||
# Tbac,
|
||||
# { A, { D, { C,rb }k(B,C) }k(B,D) }k(A,B)
|
||||
# );
|
||||
# send_6(B,C,
|
||||
# { B, Tbad }k(B,D),
|
||||
# { B, Tbac }k(B,C)
|
||||
# );
|
||||
#
|
||||
# claim_B1(B, Niagree);
|
||||
# claim_B2(B, Nisynch);
|
||||
}
|
||||
|
||||
role C
|
||||
{
|
||||
fresh rc: Nonce;
|
||||
var ra,rb,rd: Nonce;
|
||||
var Tcab,Tcbd: Ticket;
|
||||
|
||||
recv_2(B,C, rb, Tcab );
|
||||
send_3(C,D, rc,
|
||||
{ C, rb }k(B,C),
|
||||
{ C, Tcab }k(A,C)
|
||||
);
|
||||
# recv_6(B,C,
|
||||
# Tcbd,
|
||||
# { B, { A,{ D,rc }k(C,D) }k(A,C) }k(B,C)
|
||||
# );
|
||||
# send_7(C,D,
|
||||
# { C, Tcbd }k(C,D)
|
||||
# );
|
||||
#
|
||||
# claim_C1(C, Niagree);
|
||||
# claim_C2(C, Nisynch);
|
||||
}
|
||||
|
||||
role D
|
||||
{
|
||||
fresh rd: Nonce;
|
||||
var ra,rb,rc: Nonce;
|
||||
var Tdbc,Tdac: Ticket;
|
||||
|
||||
recv_3(C,D, rc, Tdbc, Tdac );
|
||||
send_4(D,A, rd,
|
||||
{ D, rc }k(C,D),
|
||||
{ D, Tdbc }k(B,D),
|
||||
{ D, Tdac }k(A,D)
|
||||
);
|
||||
# recv_7(C,D,
|
||||
# { C, { B,{ A,rd }k(A,D) }k(B,D) }k(C,D)
|
||||
# );
|
||||
#
|
||||
# claim_D1(D, Niagree);
|
||||
# claim_D2(D, Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
# General scenario
|
||||
|
||||
@@ -1,24 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol carkeybrokenlim(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
send_1(I,R, I,R );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
|
||||
recv_1(I,R, I,R );
|
||||
claim_2(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,24 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol carkeybroken(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
send_1(I,R, {ni}sk(I) );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
|
||||
recv_1(I,R, {ni}sk(I) );
|
||||
claim_2(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,24 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol carkeyni(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
send_1(I,R, {R,ni}sk(I) );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
|
||||
recv_1(I,R, {R,ni}sk(I) );
|
||||
claim_2(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,26 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol carkeyni2(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
send_1(I,R, {R,ni}sk(I) );
|
||||
send_2(I,R, {R,ni}sk(I) );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
|
||||
recv_1(I,R, {R,ni}sk(I) );
|
||||
recv_2(I,R, {R,ni}sk(I) );
|
||||
claim_4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,45 +0,0 @@
|
||||
usertype Data;
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol ccitt509(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh xi,yi: Data;
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var yr,xr: Data;
|
||||
|
||||
send_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) );
|
||||
recv_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
|
||||
send_3(I,R, I,{R,nr}sk(I) );
|
||||
|
||||
claim_4(I,Secret,yi);
|
||||
claim_5(I,Secret,yr);
|
||||
claim_6(I,Nisynch);
|
||||
claim_7(I,Niagree);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var xi,yi: Data;
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh yr,xr: Data;
|
||||
|
||||
recv_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) );
|
||||
send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
|
||||
recv_3(I,R, I,{R,nr}sk(I) );
|
||||
|
||||
claim_8(R,Secret,yi);
|
||||
claim_9(R,Secret,yr);
|
||||
claim_10(R,Nisynch);
|
||||
claim_11(R,Niagree);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const de: Data;
|
||||
|
||||
@@ -1,36 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
const P1;
|
||||
|
||||
protocol nsl3th1(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {P1,I,ni}pk(R) );
|
||||
recv_1b(R,I, {nr}pk(I) );
|
||||
recv_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
send_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
claim_i(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {P1,I,ni}pk(R) );
|
||||
send_1b(R,I, {nr}pk(I) );
|
||||
send_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
claim_r(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,70 +0,0 @@
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
const P1;
|
||||
const P2;
|
||||
|
||||
protocol nsl3th1(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {P1,I,ni}pk(R) );
|
||||
recv_1b(R,I, {nr}pk(I) );
|
||||
recv_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
send_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
claim_i(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {P1,I,ni}pk(R) );
|
||||
send_1b(R,I, {nr}pk(I) );
|
||||
send_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
claim_r(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
protocol nsl3th2(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {P2,I,ni}pk(R) );
|
||||
recv_1b(R,I, {nr}pk(I) );
|
||||
recv_2(R,I, {P2,ni,nr,R}pk(I) );
|
||||
send_3(I,R, {P2,nr}pk(R) );
|
||||
|
||||
claim_i(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {P2,I,ni}pk(R) );
|
||||
send_1b(R,I, {nr}pk(I) );
|
||||
send_2(R,I, {P2,ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {P2,nr}pk(R) );
|
||||
|
||||
claim_r(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,52 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
const P1;
|
||||
const P2;
|
||||
|
||||
protocol nsl3th3ni(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni,ni: Nonce;
|
||||
var nr,nr2: Nonce;
|
||||
|
||||
send_1(I,R, {P1,I,ni}pk(R) );
|
||||
recv_1b(R,I, {nr}pk(I) );
|
||||
recv_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
send_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
//claim_i(I,Nisynch);
|
||||
|
||||
send_21(I,R, {P2,I,ni}pk(R) );
|
||||
recv_21b(R,I, {nr2}pk(I) );
|
||||
recv_22(R,I, {P2,ni,nr2,R}pk(I) );
|
||||
send_23(I,R, {P2,nr2}pk(R) );
|
||||
|
||||
claim_i2(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni,ni: Nonce;
|
||||
fresh nr,nr2: Nonce;
|
||||
|
||||
recv_1(I,R, {P1,I,ni}pk(R) );
|
||||
send_1b(R,I, {nr}pk(I) );
|
||||
send_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
//claim_r(R,Nisynch);
|
||||
|
||||
recv_21(I,R, {P2,I,ni}pk(R) );
|
||||
send_21b(R,I, {nr2}pk(I) );
|
||||
send_22(R,I, {P2,ni,nr2,R}pk(I) );
|
||||
recv_23(I,R, {P2,nr2}pk(R) );
|
||||
|
||||
claim_r2(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,52 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
const P1;
|
||||
const P2;
|
||||
|
||||
protocol nsl3th3nr(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni,ni2: Nonce;
|
||||
var nr,nr: Nonce;
|
||||
|
||||
send_1(I,R, {P1,I,ni}pk(R) );
|
||||
recv_1b(R,I, {nr}pk(I) );
|
||||
recv_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
send_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
//claim_i(I,Nisynch);
|
||||
|
||||
send_21(I,R, {P2,I,ni2}pk(R) );
|
||||
recv_21b(R,I, {nr}pk(I) );
|
||||
recv_22(R,I, {P2,ni2,nr,R}pk(I) );
|
||||
send_23(I,R, {P2,nr}pk(R) );
|
||||
|
||||
claim_i2(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni,ni2: Nonce;
|
||||
fresh nr,nr: Nonce;
|
||||
|
||||
recv_1(I,R, {P1,I,ni}pk(R) );
|
||||
send_1b(R,I, {nr}pk(I) );
|
||||
send_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
//claim_r(R,Nisynch);
|
||||
|
||||
recv_21(I,R, {P2,I,ni2}pk(R) );
|
||||
send_21b(R,I, {nr}pk(I) );
|
||||
send_22(R,I, {P2,ni2,nr,R}pk(I) );
|
||||
recv_23(I,R, {P2,nr}pk(R) );
|
||||
|
||||
claim_r2(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,52 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
const P1;
|
||||
const P2;
|
||||
|
||||
protocol nsl3th3(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni,ni2: Nonce;
|
||||
var nr,nr2: Nonce;
|
||||
|
||||
send_1(I,R, {P1,I,ni}pk(R) );
|
||||
recv_1b(R,I, {nr}pk(I) );
|
||||
recv_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
send_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
//claim_i(I,Nisynch);
|
||||
|
||||
send_21(I,R, {P2,I,ni2}pk(R) );
|
||||
recv_21b(R,I, {nr2}pk(I) );
|
||||
recv_22(R,I, {P2,ni2,nr2,R}pk(I) );
|
||||
send_23(I,R, {P2,nr2}pk(R) );
|
||||
|
||||
claim_i2(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni,ni2: Nonce;
|
||||
fresh nr,nr2: Nonce;
|
||||
|
||||
recv_1(I,R, {P1,I,ni}pk(R) );
|
||||
send_1b(R,I, {nr}pk(I) );
|
||||
send_2(R,I, {P1,ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {P1,nr}pk(R) );
|
||||
|
||||
//claim_r(R,Nisynch);
|
||||
|
||||
recv_21(I,R, {P2,I,ni2}pk(R) );
|
||||
send_21b(R,I, {nr2}pk(I) );
|
||||
send_22(R,I, {P2,ni2,nr2,R}pk(I) );
|
||||
recv_23(I,R, {P2,nr2}pk(R) );
|
||||
|
||||
claim_r2(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,36 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
const P2;
|
||||
|
||||
protocol nsl3th2(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {P2,I,ni}pk(R) );
|
||||
recv_1b(R,I, {nr}pk(I) );
|
||||
recv_2(R,I, {P2,ni,nr,R}pk(I) );
|
||||
send_3(I,R, {P2,nr}pk(R) );
|
||||
|
||||
claim_i(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {P2,I,ni}pk(R) );
|
||||
send_1b(R,I, {nr}pk(I) );
|
||||
send_2(R,I, {P2,ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {P2,nr}pk(R) );
|
||||
|
||||
claim_r(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,72 +0,0 @@
|
||||
/*
|
||||
* Denning-Sacco shared key
|
||||
* CJ, but modeled after Sjouke's protocol list
|
||||
*/
|
||||
|
||||
/* default includes */
|
||||
|
||||
/* asymmetric */
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
|
||||
/* symmetric */
|
||||
|
||||
usertype SessionKey, Time, Ticket;
|
||||
secret k: Function;
|
||||
|
||||
/* agents */
|
||||
|
||||
|
||||
|
||||
/* untrusted e */
|
||||
|
||||
untrusted e;
|
||||
const kee: SessionKey;
|
||||
|
||||
compromised k(e,e);
|
||||
compromised k(e,a);
|
||||
compromised k(e,b);
|
||||
compromised k(a,e);
|
||||
compromised k(b,e);
|
||||
|
||||
protocol denningsaccosh(A,S,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var t: Time;
|
||||
var T: Ticket;
|
||||
var kab: SessionKey;
|
||||
|
||||
send_1 (A,S, A,S );
|
||||
recv_2 (S,A, {B, kab, t, T}k(A,S) );
|
||||
send_3 (A,B, T);
|
||||
|
||||
claim_4 (A, Secret, kab);
|
||||
claim_5 (A, Nisynch);
|
||||
claim_6 (A, Niagree);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh t: Time;
|
||||
fresh kab: SessionKey;
|
||||
|
||||
recv_1 (A,S, A,S );
|
||||
send_2 (S,A, {B, kab, t, { kab, A,t }k(B,S) }k(A,S) );
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var t: Time;
|
||||
var kab: SessionKey;
|
||||
|
||||
recv_3 (A,B, { kab, A,t }k(B,S) );
|
||||
|
||||
claim_7 (B, Secret, kab);
|
||||
claim_8 (B, Nisynch);
|
||||
claim_9 (B, Niagree);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,38 +0,0 @@
|
||||
/*
|
||||
* f4.spdl
|
||||
*
|
||||
* Tailored protocol to show that any number of runs can be required to
|
||||
* find an attack.
|
||||
*
|
||||
* For this version, -m2 and -r4 are needed.
|
||||
*
|
||||
* April 2005, Cas Cremers
|
||||
*/
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol f4(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
var nr: Nonce;
|
||||
|
||||
recv_!1(R,I, nr );
|
||||
send_!2(I,R, { nr }sk(I) );
|
||||
recv_!3(R,I, {{{{ nr }sk(R)}sk(R)}sk(R)}sk(R) );
|
||||
|
||||
claim_i1(I,Reachable);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
fresh nr: Nonce;
|
||||
send_!1(R,I, nr );
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,38 +0,0 @@
|
||||
/*
|
||||
* f5.spdl
|
||||
*
|
||||
* Tailored protocol to show that any number of runs can be required to
|
||||
* find an attack.
|
||||
*
|
||||
* For this version, -m2 and -r5 are needed.
|
||||
*
|
||||
* April 2005, Cas Cremers
|
||||
*/
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol f5(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
var nr: Nonce;
|
||||
|
||||
recv_!1(R,I, nr );
|
||||
send_!2(I,R, { nr }sk(I) );
|
||||
recv_!3(R,I, {{{{{ nr }sk(R)}sk(R)}sk(R)}sk(R)}sk(R) );
|
||||
|
||||
claim_i1(I,Reachable);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
fresh nr: Nonce;
|
||||
send_!1(R,I, nr );
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,104 +0,0 @@
|
||||
#!/usr/bin/python
|
||||
"""
|
||||
Scyther : An automatic verifier for security protocols.
|
||||
Copyright (C) 2007 Cas Cremers
|
||||
|
||||
This program is free software; you can redistribute it and/or
|
||||
modify it under the terms of the GNU General Public License
|
||||
as published by the Free Software Foundation; either version 2
|
||||
of the License, or (at your option) any later version.
|
||||
|
||||
This program is distributed in the hope that it will be useful,
|
||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
GNU General Public License for more details.
|
||||
|
||||
You should have received a copy of the GNU General Public License
|
||||
along with this program; if not, write to the Free Software
|
||||
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
|
||||
"""
|
||||
|
||||
import sys
|
||||
|
||||
def nlist(pref,post,si,ei):
|
||||
s = ""
|
||||
for x in range(si,ei+1):
|
||||
if s != "":
|
||||
s += ","
|
||||
s += "%s%i" % (pref,x)
|
||||
s += post
|
||||
return s
|
||||
|
||||
def ffgg(n):
|
||||
s = """
|
||||
|
||||
/*
|
||||
* ffgg%i protocol
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol ffgg%i(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
""" % (n,n)
|
||||
|
||||
nonces1 = nlist("n","",1,n)
|
||||
nonces1b = nlist("n","",2,n)
|
||||
nonces2 = nlist("n","b",2,n)
|
||||
ivar = nonces1
|
||||
rvar = nonces2
|
||||
rconst = nonces1
|
||||
|
||||
s += """
|
||||
const M: Nonce;
|
||||
var %s: Nonce;
|
||||
|
||||
send_1(A,B, A );
|
||||
read_2(B,A, B,%s );
|
||||
send_3(A,B, A,{%s,M}pk(B) );
|
||||
read_4(B,A, n1,n2,{%s,M,n1}pk(B) );
|
||||
|
||||
claim_i1(A,Secret,M);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var M,%s: Nonce;
|
||||
const %s: Nonce;
|
||||
|
||||
read_1(A,B, A );
|
||||
send_2(B,A, B,%s );
|
||||
read_3(A,B, A,{n1,%s,M}pk(B) );
|
||||
send_4(B,A, n1,n2b,{%s,M,n1}pk(B) );
|
||||
}
|
||||
}
|
||||
|
||||
// The agents in the system
|
||||
|
||||
const Alice,Bob: Agent;
|
||||
|
||||
// An untrusted agent, with leaked information
|
||||
|
||||
const Eve: Agent;
|
||||
untrusted Eve;
|
||||
const ne: Nonce;
|
||||
compromised sk(Eve);
|
||||
|
||||
""" % (ivar,nonces1,nonces1,nonces1b,rvar,rconst,nonces1,nonces2,nonces2)
|
||||
|
||||
return s
|
||||
|
||||
if __name__ == '__main__':
|
||||
if len(sys.argv) > 1:
|
||||
print ffgg(int(sys.argv[1]))
|
||||
else:
|
||||
print "Please provide a number n to generate ffgg_n"
|
||||
|
||||
@@ -1,22 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol r5bound(I,R)
|
||||
{
|
||||
role R
|
||||
{
|
||||
var k1: Nonce;
|
||||
var ni: Nonce;
|
||||
fresh k2: Nonce;
|
||||
|
||||
recv_!1 (I,R, ni );
|
||||
send_!2 (R,I, { ni }sk(R) );
|
||||
recv_!3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) );
|
||||
send_!4 (R,I, {k2}k1 );
|
||||
|
||||
claim_6 (R, Secret, k2);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,53 +0,0 @@
|
||||
/*
|
||||
* This is a model of a version of the four-way handshake protocol as modeled
|
||||
* by He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular
|
||||
* correctness proof of IEEE 802.11i and TLS".
|
||||
*/
|
||||
#define ptk hash( pmk(X,Y),x,y )
|
||||
|
||||
/* below is just Scyther input and no further macro definitions */
|
||||
|
||||
usertype Params, String;
|
||||
|
||||
const hash: Function;
|
||||
secret unhash: Function;
|
||||
inversekeys(hash,unhash);
|
||||
secret pmk: Function;
|
||||
|
||||
const msg1,msg2,msg3,msg4: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
|
||||
protocol fourway(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh x: Nonce;
|
||||
var y: Nonce;
|
||||
|
||||
send_1( X,Y, x,msg1 );
|
||||
recv_2( Y,X, y,msg2,hash( ptk,y,msg2 ) );
|
||||
send_3( X,Y, x,msg3,hash( ptk,x,msg3 ) );
|
||||
recv_4( Y,X, msg4,hash( ptk,msg4 ) );
|
||||
|
||||
claim_X1( X, Secret, ptk );
|
||||
claim_X2( X, Niagree );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var x: Nonce;
|
||||
fresh y: Nonce;
|
||||
|
||||
recv_1( X,Y, x,msg1 );
|
||||
send_2( Y,X, y,msg2,hash( ptk,y,msg2 ) );
|
||||
recv_3( X,Y, x,msg3,hash( ptk,x,msg3 ) );
|
||||
send_4( Y,X, msg4,hash( ptk,msg4 ) );
|
||||
|
||||
claim_Y1( Y, Secret, ptk );
|
||||
claim_Y2( Y, Niagree );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,48 +0,0 @@
|
||||
# 1 "fourway-HSDDM05.cpp"
|
||||
# 1 "<built-in>"
|
||||
# 1 "<command line>"
|
||||
# 1 "fourway-HSDDM05.cpp"
|
||||
# 10 "fourway-HSDDM05.cpp"
|
||||
usertype Params, String;
|
||||
|
||||
const hash: Function;
|
||||
secret unhash: Function;
|
||||
inversekeys(hash,unhash);
|
||||
secret pmk: Function;
|
||||
|
||||
const msg1,msg2,msg3,msg4: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
|
||||
protocol fourway(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh x: Nonce;
|
||||
var y: Nonce;
|
||||
|
||||
send_1( X,Y, x,msg1 );
|
||||
recv_2( Y,X, y,msg2,hash( hash( pmk(X,Y),x,y ),y,msg2 ) );
|
||||
send_3( X,Y, x,msg3,hash( hash( pmk(X,Y),x,y ),x,msg3 ) );
|
||||
recv_4( Y,X, msg4,hash( hash( pmk(X,Y),x,y ),msg4 ) );
|
||||
|
||||
claim_X1( X, Secret, hash( pmk(X,Y),x,y ) );
|
||||
claim_X2( X, Niagree );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var x: Nonce;
|
||||
fresh y: Nonce;
|
||||
|
||||
recv_1( X,Y, x,msg1 );
|
||||
send_2( Y,X, y,msg2,hash( hash( pmk(X,Y),x,y ),y,msg2 ) );
|
||||
recv_3( X,Y, x,msg3,hash( hash( pmk(X,Y),x,y ),x,msg3 ) );
|
||||
send_4( Y,X, msg4,hash( hash( pmk(X,Y),x,y ),msg4 ) );
|
||||
|
||||
claim_Y1( Y, Secret, hash( pmk(X,Y),x,y ) );
|
||||
claim_Y2( Y, Niagree );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,65 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
usertype Keypart;
|
||||
secret k: Function;
|
||||
const f: Function;
|
||||
|
||||
/*
|
||||
* Gong nonce based alternative
|
||||
*
|
||||
* Boyd & Mathuria: Protocols for authentication and key establishment
|
||||
* (2003) p. 101
|
||||
*/
|
||||
|
||||
protocol gongnonceb(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
fresh ki: Keypart;
|
||||
var kr: Keypart;
|
||||
|
||||
send_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni );
|
||||
recv_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr );
|
||||
send_5 (I,R, { I,R,nr }f(ki,kr) );
|
||||
|
||||
claim_6 (I, Secret, ki);
|
||||
claim_7 (I, Secret, kr);
|
||||
claim_8 (I, Nisynch);
|
||||
claim_9 (I, Niagree);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh kr: Keypart;
|
||||
var ki: Keypart;
|
||||
|
||||
recv_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni );
|
||||
send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr );
|
||||
recv_5 (I,R, { I,R,nr }f(ki,kr) );
|
||||
|
||||
claim_10 (R, Secret, ki);
|
||||
claim_11 (R, Secret, kr);
|
||||
claim_12 (R, Nisynch);
|
||||
claim_13 (R, Niagree);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var ni,nr: Nonce;
|
||||
var ki,kr: Keypart;
|
||||
var T;
|
||||
|
||||
recv_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni );
|
||||
send_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni );
|
||||
recv_3 (R,S, { R,S,R,kr,I }k(R,S), T, nr );
|
||||
send_4 (S,I, { S,I,R,kr,I }k(I,S), T, nr );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const kpe: Keypart;
|
||||
const ke: Sessionkey;
|
||||
|
||||
@@ -1,56 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
usertype Keypart;
|
||||
secret k: Function;
|
||||
|
||||
protocol gongnonce(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
fresh ki: Keypart;
|
||||
var kr: Keypart;
|
||||
|
||||
send_1 (I,R, I,R,ni );
|
||||
recv_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr);
|
||||
send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) );
|
||||
|
||||
claim_6 (I, Secret, ki);
|
||||
claim_7 (I, Secret, kr);
|
||||
claim_8 (I, Nisynch);
|
||||
claim_9 (I, Niagree);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh kr: Keypart;
|
||||
var ki: Keypart;
|
||||
|
||||
recv_1 (I,R, I,R,ni );
|
||||
send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S));
|
||||
recv_5 (S,R, { S,R,I, ki, R, nr }k(R,S) );
|
||||
|
||||
claim_10 (R, Secret, ki);
|
||||
claim_11 (R, Secret, kr);
|
||||
claim_12 (R, Nisynch);
|
||||
claim_13 (R, Niagree);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var ni,nr: Nonce;
|
||||
var ki,kr: Keypart;
|
||||
|
||||
recv_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S));
|
||||
send_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr);
|
||||
recv_4 (I,S, { I,S,I, ki, R, nr }k(I,S) );
|
||||
send_5 (S,R, { S,R,I, ki, R, nr }k(R,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const kpe: Keypart;
|
||||
const ke: Sessionkey;
|
||||
|
||||
@@ -1,17 +0,0 @@
|
||||
usertype String, World;
|
||||
secret HelloWorld, k: String;
|
||||
|
||||
protocol hw(initiator,world)
|
||||
{
|
||||
role initiator
|
||||
{
|
||||
send_1(initiator, world, HelloWorld);
|
||||
/* claim_2(initiator, Secret, HelloWorld); */
|
||||
}
|
||||
}
|
||||
|
||||
const Alice, Bob: Agent;
|
||||
const Earth, Mars: World;
|
||||
|
||||
run hw.initiator(Agent,World);
|
||||
|
||||
@@ -1,61 +0,0 @@
|
||||
// 12/05/06
|
||||
// S. Mauw
|
||||
// Using Identity Based Encryption primitive to make NSL authentication.
|
||||
// The only requirement on the server communications is that the
|
||||
// sending of the private key is secret.
|
||||
|
||||
const ibepublic: Function; //publicly known key construction from server
|
||||
//parameters and recipient name
|
||||
secret ibesecret: Function;//secret key determined by server for recipient
|
||||
const param: Function; //public security parameter of server
|
||||
inversekeys (ibepublic,ibesecret);
|
||||
|
||||
protocol ibe(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
//Note that we are not interested in the order of server messages.
|
||||
recv_!1(S,I, param(S) );
|
||||
send_3(I,R, {I,ni}ibepublic(param(S),R) );
|
||||
recv_4(R,I, {ni,nr,R}ibepublic(param(S),I) );
|
||||
send_5(I,R, {nr}ibepublic(param(S),R) );
|
||||
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_!2(S,R, {ibesecret(param(S),R)}pk(R) );
|
||||
recv_3(I,R, {I,ni}ibepublic(param(S),R) );
|
||||
send_4(R,I, {ni,nr,R}ibepublic(param(S),I) );
|
||||
recv_5(I,R, {nr}ibepublic(param(S),R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
recv_!0(S,S, R,S); // workaround for the fact that R & S are roles, so Scyther should not jump to conclusions (remove it and see what happens)
|
||||
send_!1(S,I, param(S) );
|
||||
send_!2(S,R, {ibesecret(param(S),R)}pk(R) );
|
||||
|
||||
claim_s1(S,Secret,ibesecret(param(S),R));
|
||||
}
|
||||
}
|
||||
|
||||
compromised ibesecret(param(Eve),Alice);
|
||||
compromised ibesecret(param(Eve),Bob);
|
||||
compromised ibesecret(param(Eve),Carol);
|
||||
@@ -1,46 +0,0 @@
|
||||
// 12/05/06
|
||||
// S. Mauw
|
||||
// Modeling of Identity Based Encryption primitive.
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
const ibepublic: Function;
|
||||
secret ibesecret: Function;
|
||||
const param: Function;
|
||||
inversekeys (pk,sk);
|
||||
inversekeys (ibepublic,ibesecret);
|
||||
|
||||
protocol ibe(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
recv_1(S,I, param(S) );
|
||||
send_3(I,R, {ni}ibepublic(param(S),R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
|
||||
recv_2(S,R, {ibesecret(param(S),R)}pk(R) );
|
||||
recv_3(I,R, {ni}ibepublic(param(S),R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
//of course this claim is invalid
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
send_1(S,I, param(S) );
|
||||
send_2(S,R, {ibesecret(param(S),R)}pk(R) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
compromised ibesecret(param(Eve),Alice);
|
||||
compromised ibesecret(param(Eve),Bob);
|
||||
compromised ibesecret(param(Eve),Carol);
|
||||
@@ -1,47 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
usertype Ticket;
|
||||
secret k: Function;
|
||||
|
||||
protocol isoiec11770213(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Sessionkey;
|
||||
|
||||
send_1 (I,R, ni);
|
||||
recv_4 (R,I, { ni,kir,R }k(I,S) );
|
||||
|
||||
claim_5 (I, Secret, kir);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh kir: Sessionkey;
|
||||
var T;
|
||||
|
||||
recv_1 (I,R, ni);
|
||||
send_2 (R,S, { nr,ni,I,kir }k(R,S) );
|
||||
recv_3 (S,R, { nr, I }k(R,S), T );
|
||||
send_4 (R,I, T );
|
||||
|
||||
claim_6 (R, Secret, kir);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var ni,nr: Nonce;
|
||||
var kir: Sessionkey;
|
||||
|
||||
recv_2 (R,S, { nr,ni,I,kir }k(R,S) );
|
||||
send_3 (S,R, { nr, I }k(R,S), { ni,kir,R }k(I,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const te: Ticket;
|
||||
const ke: Sessionkey;
|
||||
|
||||
@@ -1,51 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
usertype Ticket;
|
||||
secret k: Function;
|
||||
|
||||
protocol kaochowPalm(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Sessionkey;
|
||||
|
||||
send_1 (I,S, I,R,ni);
|
||||
recv_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
|
||||
send_4 (I,R, {nr}kir );
|
||||
|
||||
claim_5 (I, Nisynch);
|
||||
claim_6 (I, Niagree);
|
||||
claim_7 (I, Secret, kir);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
var kir: Sessionkey;
|
||||
var T;
|
||||
|
||||
recv_2 (S,R, { T, { I,R,ni,kir }k(R,S) }k(R,S) );
|
||||
send_3 (R,I, T, {ni}kir, nr );
|
||||
recv_4 (I,R, {nr}kir );
|
||||
|
||||
claim_8 (R, Nisynch);
|
||||
claim_9 (R, Niagree);
|
||||
claim_10 (R, Secret, kir);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh kir: Sessionkey;
|
||||
|
||||
recv_1 (I,S, I,R,ni);
|
||||
send_2 (S,R, { {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) }k(R,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const te: Ticket;
|
||||
const ke: Sessionkey;
|
||||
|
||||
@@ -1,51 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
usertype Ticket;
|
||||
secret k: Function;
|
||||
|
||||
protocol kaochow2(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir,kt: Sessionkey;
|
||||
|
||||
send_1 (I,S, I,R,ni);
|
||||
recv_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
|
||||
send_4 (I,R, {nr,kir}kt );
|
||||
|
||||
claim_5 (I, Nisynch);
|
||||
claim_6 (I, Niagree);
|
||||
claim_7 (I, Secret, kir);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
var kir,kt: Sessionkey;
|
||||
var T: Ticket;
|
||||
|
||||
recv_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
|
||||
send_3 (R,I, R, T, {ni, kir}kt, nr );
|
||||
recv_4 (I,R, {nr,kir}kt );
|
||||
|
||||
claim_8 (R, Nisynch);
|
||||
claim_9 (R, Niagree);
|
||||
claim_10 (R, Secret, kir);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh kir, kt: Sessionkey;
|
||||
|
||||
recv_1 (I,S, I,R,ni);
|
||||
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const te: Ticket;
|
||||
const ke: Sessionkey;
|
||||
|
||||
@@ -1,54 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
usertype Ticket;
|
||||
usertype Timestamp;
|
||||
secret k: Function;
|
||||
|
||||
protocol kaochow3(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir,kt: Sessionkey;
|
||||
var T2: Ticket;
|
||||
|
||||
send_1 (I,S, I,R,ni);
|
||||
recv_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
|
||||
send_4 (I,R, {nr,kir}kt, T2 );
|
||||
|
||||
claim_5 (I, Nisynch);
|
||||
claim_6 (I, Niagree);
|
||||
claim_7 (I, Secret, kir);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
var kir,kt: Sessionkey;
|
||||
var T: Ticket;
|
||||
fresh tr: Timestamp;
|
||||
|
||||
recv_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
|
||||
send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
|
||||
recv_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
|
||||
|
||||
claim_8 (R, Nisynch);
|
||||
claim_9 (R, Niagree);
|
||||
claim_10 (R, Secret, kir);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh kir, kt: Sessionkey;
|
||||
|
||||
recv_1 (I,S, I,R,ni);
|
||||
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const te: Ticket;
|
||||
const ke: Sessionkey;
|
||||
|
||||
@@ -1,51 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
usertype Ticket;
|
||||
secret k: Function;
|
||||
|
||||
protocol kaochow(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Sessionkey;
|
||||
|
||||
send_1 (I,S, I,R,ni);
|
||||
recv_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
|
||||
send_4 (I,R, {nr}kir );
|
||||
|
||||
claim_5 (I, Nisynch);
|
||||
claim_6 (I, Niagree);
|
||||
claim_7 (I, Secret, kir);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
var kir: Sessionkey;
|
||||
var T;
|
||||
|
||||
recv_2 (S,R, T, { I,R,ni,kir }k(R,S) );
|
||||
send_3 (R,I, T, {ni}kir, nr );
|
||||
recv_4 (I,R, {nr}kir );
|
||||
|
||||
claim_8 (R, Nisynch);
|
||||
claim_9 (R, Niagree);
|
||||
claim_10 (R, Secret, kir);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh kir: Sessionkey;
|
||||
|
||||
recv_1 (I,S, I,R,ni);
|
||||
send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const te: Ticket;
|
||||
const ke: Sessionkey;
|
||||
|
||||
@@ -1,154 +0,0 @@
|
||||
/*
|
||||
* Scyther description of Kerberos as in RDDM'07
|
||||
*
|
||||
*/
|
||||
|
||||
usertype Sessionkey;
|
||||
usertype Text;
|
||||
secret ktk: Function;
|
||||
secret kck: Function;
|
||||
secret kst: Function;
|
||||
|
||||
protocol @swapkey-ktk(I,R)
|
||||
{
|
||||
# Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
|
||||
role I
|
||||
{
|
||||
var T:Ticket;
|
||||
|
||||
|
||||
recv_!X1(R,I,{T}ktk(I,R));
|
||||
send_!X2(I,R,{T}ktk(R,I));
|
||||
}
|
||||
role R
|
||||
{
|
||||
}
|
||||
}
|
||||
protocol @swapkey-kck(I,R)
|
||||
{
|
||||
# Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
|
||||
role I
|
||||
{
|
||||
var T:Ticket;
|
||||
|
||||
|
||||
recv_!X1(R,I,{T}kck(I,R));
|
||||
send_!X2(I,R,{T}kck(R,I));
|
||||
}
|
||||
role R
|
||||
{
|
||||
}
|
||||
}
|
||||
protocol @swapkey-kst(I,R)
|
||||
{
|
||||
# Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
|
||||
role I
|
||||
{
|
||||
var T:Ticket;
|
||||
|
||||
|
||||
recv_!X1(R,I,{T}kst(I,R));
|
||||
send_!X2(I,R,{T}kst(R,I));
|
||||
}
|
||||
role R
|
||||
{
|
||||
}
|
||||
}
|
||||
|
||||
protocol kerberos(C,K,T,S) {
|
||||
|
||||
role C {
|
||||
fresh n1: Nonce;
|
||||
fresh n2: Nonce;
|
||||
var tgt: Ticket;
|
||||
var st: Ticket;
|
||||
var AKey: Sessionkey;
|
||||
var SKey: Sessionkey;
|
||||
fresh t: Text;
|
||||
|
||||
send_1(C,K, C,T,n1);
|
||||
recv_2(K,C, tgt, { AKey,n1,T }kck(C,K) );
|
||||
|
||||
// Stage boundary
|
||||
|
||||
send_3(C,T, tgt, { C }AKey,C,S,n2 );
|
||||
recv_4(T,C, C, st, { SKey, n2, S }AKey );
|
||||
|
||||
// Stage boundary
|
||||
|
||||
send_5(C,S, st, { C,t }SKey );
|
||||
recv_6(S,C, { t }SKey );
|
||||
|
||||
// Theorem 5 (a)
|
||||
// If C,K are honest
|
||||
claim(C,Reachable);
|
||||
// Theorem 6 (a)
|
||||
// If C,K,T are all honest
|
||||
claim(C,Secret,AKey);
|
||||
// Theorem 7 (a)
|
||||
// If C,K,S are all honest
|
||||
claim(C, Reachable);
|
||||
// Theorem 8
|
||||
// If C,K,S are all honest
|
||||
claim(C, Secret, SKey);
|
||||
}
|
||||
role K {
|
||||
var n1: Nonce;
|
||||
fresh AKey: Sessionkey;
|
||||
|
||||
recv_1(C,K, C,T,n1);
|
||||
send_2(K,C, { AKey, C }ktk(T,K), { AKey,n1,T }kck(C,K) );
|
||||
// Theorem 6 (a)
|
||||
// If C,K,T are all honest
|
||||
claim_K1(K,Secret,AKey);
|
||||
}
|
||||
|
||||
role T {
|
||||
var AKey: Sessionkey;
|
||||
var n2: Nonce;
|
||||
fresh SKey: Sessionkey;
|
||||
|
||||
recv_3(C,T, { AKey, C }ktk(T,K), { C }AKey,C,S,n2 );
|
||||
send_4(T,C, C,{ SKey, C }kst(S,T), { SKey, n2, S }AKey );
|
||||
|
||||
// Theorem 5 (a)
|
||||
// If C,K are honest
|
||||
claim(T,Reachable);
|
||||
// Theorem 6 (a)
|
||||
// If C,K,T are all honest
|
||||
claim(T,Secret,AKey);
|
||||
|
||||
// My own
|
||||
claim(T,Secret,SKey);
|
||||
}
|
||||
role S {
|
||||
var t: Text;
|
||||
var SKey: Sessionkey;
|
||||
|
||||
recv_5(C,S, { SKey, C }kst(S,T), { C,t }SKey );
|
||||
send_6(S,C, { t }SKey );
|
||||
// Theorem 7 (b)
|
||||
// If C,K,S,T are honest
|
||||
claim(S, Reachable);
|
||||
|
||||
// My own
|
||||
claim(S, Secret, t);
|
||||
claim(S, Secret, SKey);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Charlie,Eve: Agent;
|
||||
|
||||
// C untrusted
|
||||
|
||||
// K untrusted
|
||||
|
||||
// T untrusted
|
||||
|
||||
// S untrusted
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,78 +0,0 @@
|
||||
/*
|
||||
* KSL from SPORE
|
||||
*
|
||||
* Messages 6-8 are intended for repeated authentication, and there are
|
||||
* known attacks on this. However, we don't model that yet.
|
||||
*
|
||||
* Furthermore, it is interesting to experiment here with key
|
||||
* compromise (of kab), when this is implemented in Scyther.
|
||||
*/
|
||||
|
||||
usertype Server, SessionKey, GeneralizedTimestamp, Ticket, TicketKey;
|
||||
secret k: Function;
|
||||
|
||||
const s: Server;
|
||||
|
||||
/* give the intruder something to work with */
|
||||
|
||||
const kee: SessionKey;
|
||||
untrusted e;
|
||||
compromised k(e,s);
|
||||
|
||||
protocol ksl(A,B,S)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Na, Ma: Nonce;
|
||||
var Nc, Mb: Nonce;
|
||||
var T: Ticket;
|
||||
var Kab: SessionKey;
|
||||
|
||||
send_1(A,B, Na, A);
|
||||
recv_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab );
|
||||
send_5(A,B, { Nc }Kab );
|
||||
|
||||
send_6(A,B, Ma,T );
|
||||
recv_7(B,A, Mb,{Ma}Kab );
|
||||
send_8(A,B, {Mb}Kab );
|
||||
|
||||
claim_A1(A,Secret, Kab);
|
||||
claim_A2(A,Niagree);
|
||||
claim_A3(A,Nisynch);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var Na,Ma: Nonce;
|
||||
fresh Nb,Nc,Mb: Nonce;
|
||||
var Kab: SessionKey;
|
||||
fresh Kbb: TicketKey;
|
||||
fresh Tb: GeneralizedTimestamp;
|
||||
var T: Ticket;
|
||||
|
||||
recv_1(A,B, Na, A);
|
||||
send_2(B,S, Na, A, Nb, B );
|
||||
recv_3(S,B, { Nb, A, Kab }k(B,S), T );
|
||||
send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab );
|
||||
recv_5(A,B, { Nc }Kab );
|
||||
|
||||
recv_6(A,B, Ma,{ Tb, A, Kab }Kbb );
|
||||
send_7(B,A, Mb,{Ma}Kab );
|
||||
recv_8(A,B, {Mb}Kab );
|
||||
|
||||
claim_B1(B,Secret, Kab);
|
||||
claim_B2(B,Niagree);
|
||||
claim_B3(B,Nisynch);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var Na, Nb: Nonce;
|
||||
fresh Kab: SessionKey;
|
||||
|
||||
recv_2(B,S, Na, A, Nb, B );
|
||||
send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,52 +0,0 @@
|
||||
/*
|
||||
* Breaker for localclaims protocol
|
||||
*
|
||||
* Starts out as NSL3; last message (label3) has added name to avoid
|
||||
* confusion with the later messages.
|
||||
*
|
||||
* Added messages labeled with x1 and x2 to allow for breaking the other
|
||||
* protocol.
|
||||
*/
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol lcbreaker(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var x: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr,I}pk(R) );
|
||||
|
||||
recv_x1(R,I, { x }pk(I) );
|
||||
send_x2(I,R, { x }ni );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh x: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {nr,I}pk(R) );
|
||||
|
||||
send_x1(R,I, { x }pk(I) );
|
||||
recv_x2(I,R, { x }ni );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,59 +0,0 @@
|
||||
/*
|
||||
* Breaker for localclaims protocol; sequential composition variant 1
|
||||
*
|
||||
* Starts out as NSL3; last message (label3) has added name to avoid
|
||||
* confusion with the later messages.
|
||||
*
|
||||
* Added messages labeled with x1 and x2 to allow for breaking the other
|
||||
* protocol.
|
||||
*/
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol lcbreakerS1(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni,ni2: Nonce;
|
||||
var nr: Nonce;
|
||||
var x: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr,I}pk(R) );
|
||||
|
||||
recv_x1(R,I, { x }pk(I) );
|
||||
send_x2(I,R, { x }ni );
|
||||
|
||||
send_lc(I,R, {ni2}pk(R) );
|
||||
|
||||
claim_i0(I,Secret,ni2);
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni,ni2: Nonce;
|
||||
fresh nr: Nonce;
|
||||
fresh x: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {nr,I}pk(R) );
|
||||
|
||||
send_x1(R,I, { x }pk(I) );
|
||||
recv_x2(I,R, { x }ni );
|
||||
|
||||
recv_lc(I,R, {ni2}pk(R) );
|
||||
|
||||
claim_r0(R,Secret,ni2);
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,40 +0,0 @@
|
||||
/*
|
||||
* Local claims
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol localclaims(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
send_1(I,R, {ni}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
|
||||
recv_1(I,R, {ni}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
}
|
||||
}
|
||||
|
||||
// The agents in the system
|
||||
|
||||
|
||||
// An untrusted agent, with leaked information
|
||||
|
||||
|
||||
|
||||
@@ -1,81 +0,0 @@
|
||||
/*
|
||||
* Needham-Schroeder symmetric
|
||||
* Amended version (from Sjouke's interpret.)
|
||||
*/
|
||||
|
||||
/* symmetric */
|
||||
|
||||
usertype SessionKey;
|
||||
secret k: Function;
|
||||
|
||||
/* agents */
|
||||
|
||||
|
||||
|
||||
/* untrusted e */
|
||||
|
||||
untrusted e;
|
||||
const kee: SessionKey;
|
||||
|
||||
compromised k(e,e);
|
||||
compromised k(e,a);
|
||||
compromised k(e,b);
|
||||
compromised k(a,e);
|
||||
compromised k(b,e);
|
||||
|
||||
/* {}x used for public (invertible) function modeling */
|
||||
|
||||
usertype PseudoFunction;
|
||||
const succ: PseudoFunction;
|
||||
|
||||
usertype Ticket;
|
||||
|
||||
protocol nssymmetricamended(A,S,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh na: Nonce;
|
||||
var T1: Ticket;
|
||||
var T2: Ticket;
|
||||
var kab: SessionKey;
|
||||
var nb: Nonce;
|
||||
|
||||
send_1(A,B, A );
|
||||
recv_2(B,A, T1 );
|
||||
send_3(A,S, A,B,na,T1 );
|
||||
recv_4(S,A, { na,B,kab,T2 }k(A,S) );
|
||||
send_5(A,B, T2 );
|
||||
recv_6(B,A, { nb }kab );
|
||||
send_7(A,B, { {nb}succ }kab );
|
||||
|
||||
claim_8(A, Secret, kab);
|
||||
claim_8a(A, Niagree);
|
||||
claim_8b(A, Nisynch);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh kab: SessionKey;
|
||||
var na: Nonce;
|
||||
var nb: Nonce;
|
||||
|
||||
recv_3(A,S, A,B,na, { A,nb }k(B,S) );
|
||||
send_4(S,A, { na,B,kab, { kab,A }k(B,S) }k(A,S) );
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var kab: SessionKey;
|
||||
fresh nb: Nonce;
|
||||
|
||||
recv_1(A,B, A );
|
||||
send_2(B,A, { A,nb }k(B,S) );
|
||||
recv_5(A,B, { kab,A }k(B,S) );
|
||||
send_6(B,A, { nb }kab );
|
||||
recv_7(A,B, { {nb}succ }kab );
|
||||
|
||||
claim_9(B, Secret, kab);
|
||||
claim_9a(B, Niagree);
|
||||
claim_9b(B, Nisynch);
|
||||
}
|
||||
}
|
||||
@@ -1,70 +0,0 @@
|
||||
/*
|
||||
* Needham-Schroeder symmetric
|
||||
*/
|
||||
|
||||
/* symmetric */
|
||||
|
||||
usertype SessionKey;
|
||||
secret k: Function;
|
||||
|
||||
/* agents */
|
||||
|
||||
|
||||
|
||||
/* untrusted e */
|
||||
|
||||
untrusted e;
|
||||
const kee: SessionKey;
|
||||
|
||||
compromised k(e,e);
|
||||
compromised k(e,a);
|
||||
compromised k(e,b);
|
||||
compromised k(a,e);
|
||||
compromised k(b,e);
|
||||
|
||||
/* {}x used for public (invertible) function modeling */
|
||||
|
||||
usertype PseudoFunction;
|
||||
const succ: PseudoFunction;
|
||||
|
||||
usertype Ticket;
|
||||
|
||||
protocol nssymmetric(A,S,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh na: Nonce;
|
||||
var T: Ticket;
|
||||
var kab: SessionKey;
|
||||
var nb: Nonce;
|
||||
|
||||
send_1(A,S, A,B,na );
|
||||
recv_2(S,A, { na,B,kab,T }k(A,S) );
|
||||
send_3(A,B, T );
|
||||
recv_4(B,A, { nb }kab );
|
||||
send_5(A,B, { {nb}succ }kab );
|
||||
|
||||
claim_6(A, Secret, kab);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh kab: SessionKey;
|
||||
var na: Nonce;
|
||||
|
||||
recv_1(A,S, A,B,na );
|
||||
send_2(S,A, { na,B,kab, { kab,A }k(B,S) }k(A,S) );
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var kab: SessionKey;
|
||||
fresh nb: Nonce;
|
||||
|
||||
recv_3(A,B, { kab,A }k(B,S) );
|
||||
send_4(B,A, { nb }kab );
|
||||
recv_5(A,B, { {nb}succ }kab );
|
||||
|
||||
claim_7(B, Secret, kab);
|
||||
}
|
||||
}
|
||||
@@ -1,43 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol ns3brutus(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim_4(I,Secret,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
claim_5(R,Secret,ni);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve : Agent;
|
||||
|
||||
/* something like this will later on all be implied by 'untrusted Eve' */
|
||||
|
||||
/* fresh nc: Nonce; */
|
||||
|
||||
/* pre-defined 10 runs, limit using --max-runs parameters */
|
||||
/* to be nice to brutus, stupid scenario :( */
|
||||
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
@@ -1,52 +0,0 @@
|
||||
/*
|
||||
* Needham-Schroeder protocol
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol ns3(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
// The agents in the system
|
||||
|
||||
|
||||
// An untrusted agent, with leaked information
|
||||
|
||||
|
||||
// The runs (only needed for the modelchecker algorithm)
|
||||
|
||||
|
||||
@@ -1,35 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol nsl3rep(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
send_6(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim_4(I,Niagree);
|
||||
claim_7(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
recv_6(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
claim_5(R,Niagree);
|
||||
claim_8(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,39 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol nsl3(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,75 +0,0 @@
|
||||
# Neumann Stubblebine
|
||||
#
|
||||
# Modelled after the description in the SPORE library
|
||||
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
||||
#
|
||||
# Note:
|
||||
# In SPORE this protocol is not described correctly, there are in fact 2
|
||||
# different protocols (the key establishment protocol and the repeated
|
||||
# authentication protocol)
|
||||
|
||||
usertype Server, SessionKey, TimeStamp, TicketKey;
|
||||
usertype ExpiredTimeStamp;
|
||||
secret k: Function;
|
||||
|
||||
const Fresh: Function;
|
||||
const Compromised: Function;
|
||||
|
||||
const kee: SessionKey;
|
||||
|
||||
protocol neustub(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh Ni: Nonce;
|
||||
var Nr: Nonce;
|
||||
var T: Ticket;
|
||||
var Tb: TimeStamp;
|
||||
var Kir: SessionKey;
|
||||
|
||||
send_1(I,R, I, Ni);
|
||||
recv_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
|
||||
send_4(I,R,T,{Nr}Kir);
|
||||
|
||||
send_!chain(I,R, { R,Tb,Kir }k(I,S), T);
|
||||
|
||||
claim_I1(I,Secret, Kir);
|
||||
claim_I2(I,Niagree);
|
||||
claim_I3(I,Nisynch);
|
||||
claim_I4(I,Empty,(Fresh,Kir));
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var Ni,Mi: Nonce;
|
||||
fresh Nr,Mr: Nonce;
|
||||
var Kir: SessionKey;
|
||||
fresh Tb: TimeStamp;
|
||||
var T: Ticket;
|
||||
|
||||
fresh g: Ticket;
|
||||
|
||||
recv_1(I,R, I, Ni);
|
||||
send_!2(R,S, R, {I, Ni, Tb, g}k(R,S),Nr);
|
||||
recv_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
|
||||
|
||||
claim_R1(R,Secret, Kir);
|
||||
claim_R5(R,Secret, g);
|
||||
claim_R2(R,Niagree);
|
||||
claim_R3(R,Nisynch);
|
||||
claim_R4(R,Empty,(Fresh,Kir));
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var Ni, Nr: Nonce;
|
||||
fresh Kir: SessionKey;
|
||||
var Tb: TimeStamp;
|
||||
|
||||
var g: Ticket;
|
||||
|
||||
recv_!2(R,S, R, {I,Ni,Tb, g}k(R,S), Nr);
|
||||
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,75 +0,0 @@
|
||||
# Neumann Stubblebine
|
||||
#
|
||||
# Modelled after the description in the SPORE library
|
||||
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
||||
#
|
||||
# Note:
|
||||
# In SPORE this protocol is not described correctly, there are in fact 2
|
||||
# different protocols (the key establishment protocol and the repeated
|
||||
# authentication protocol)
|
||||
|
||||
usertype Server, SessionKey, TimeStamp, TicketKey;
|
||||
usertype ExpiredTimeStamp;
|
||||
secret k: Function;
|
||||
|
||||
const Fresh: Function;
|
||||
const Compromised: Function;
|
||||
|
||||
const kee: SessionKey;
|
||||
|
||||
protocol neustub^Repeat(I,R,S)
|
||||
{
|
||||
fresh Kir: SessionKey;
|
||||
|
||||
role I
|
||||
{
|
||||
fresh Mi: Nonce;
|
||||
var Mr: Nonce;
|
||||
var Kir: SessionKey;
|
||||
var Tr: TimeStamp;
|
||||
|
||||
var Tb: Ticket;
|
||||
fresh g: Ticket;
|
||||
var h: Ticket;
|
||||
|
||||
recv_!chain(R,I, { R,Tr,Kir }k(I,S), Tb);
|
||||
|
||||
send_5(I,R,Mi,{I,Kir,Tr}k(R,S),g);
|
||||
recv_6(R,I,{Mi,Mr,g,h}Kir);
|
||||
send_7(I,R,{I,Mr}Kir);
|
||||
|
||||
claim_I0(I,Secret, g);
|
||||
claim_I5(I,Secret, h);
|
||||
claim_I1(I,Secret, Kir);
|
||||
claim_I2(I,Niagree);
|
||||
claim_I3(I,Nisynch);
|
||||
claim_I4(I,Empty,(Fresh,Kir));
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
fresh Mr: Nonce;
|
||||
var Tr: TimeStamp;
|
||||
var Kir: SessionKey;
|
||||
var Mi: Nonce;
|
||||
|
||||
var g: Ticket;
|
||||
fresh h: Ticket;
|
||||
|
||||
recv_5(I,R,Mi,{I,Kir,Tr}k(R,S),g);
|
||||
send_6(R,I,{Mi,Mr,g,h}Kir);
|
||||
recv_7(I,R,{I,Mr}Kir);
|
||||
|
||||
claim_R1(R,Secret, Kir);
|
||||
claim_R5(R,Secret, g);
|
||||
claim_R6(R,Secret, h);
|
||||
claim_R2(R,Niagree);
|
||||
claim_R3(R,Nisynch);
|
||||
claim_R4(R,Empty,(Fresh,Kir));
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,18 +0,0 @@
|
||||
usertype String;
|
||||
|
||||
const Alice,Bob,Charlie: Agent;
|
||||
const Hallo: String;
|
||||
|
||||
protocol onetrace(I)
|
||||
{
|
||||
role I
|
||||
{
|
||||
var input: String;
|
||||
|
||||
recv_!1(I,I, input);
|
||||
send_!2(I,I, Hallo);
|
||||
recv_!3(I,I, input);
|
||||
claim_4(I, Secret, input);
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,58 +0,0 @@
|
||||
secret fresh k : Function;
|
||||
|
||||
/* Version from the Spore Librairy
|
||||
http://www.lsv.ens-cachan.fr/spore/otwayRees.html
|
||||
*/
|
||||
|
||||
usertype String, SesKey, Ticket, Server;
|
||||
|
||||
protocol otwayrees(A,B,S)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh na : Nonce;
|
||||
fresh M : String;
|
||||
var kab : SesKey;
|
||||
|
||||
send_1(A,B, M,A,B, { na,M,A,B }k(A,S) );
|
||||
recv_4(B,A, M, { na,kab }k(A,S) );
|
||||
|
||||
claim_5(A, Secret,kab);
|
||||
claim_5b(A, Niagree);
|
||||
claim_5c(A, Nisynch);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var M : String;
|
||||
fresh nb : Nonce;
|
||||
var kab : SesKey;
|
||||
var t1,t2;
|
||||
|
||||
recv_1(A,B, M,A,B, t1 );
|
||||
send_2(B,S, M,A,B, t1, { nb,M,A,B }k(B,S) );
|
||||
recv_3(S,B, M, t2, { nb,kab }k(B,S) );
|
||||
send_4(B,A, M, t2 );
|
||||
|
||||
claim_6(B, Secret,kab);
|
||||
claim_6a(B, Niagree);
|
||||
claim_6b(B, Nisynch);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var na,nb : Nonce;
|
||||
var M : String;
|
||||
fresh kab : SesKey;
|
||||
|
||||
recv_2(B,S, M,A,B, { na,M,A,B }k(A,S), { nb,M,A,B }k(B,S) );
|
||||
send_3(S,B, M, { na,kab }k(A,S) , { nb,kab }k(B,S) );
|
||||
}
|
||||
}
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Simon: Server;
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,52 +0,0 @@
|
||||
# List of protocols to test
|
||||
#
|
||||
andrew-ban.spdl
|
||||
andrew-lowe-ban.spdl
|
||||
#bke-broken.spdl
|
||||
#bke-one.spdl
|
||||
#bkepk-ce2.spdl
|
||||
#bkepk-ce.spdl
|
||||
#bkepk.spdl
|
||||
bke.spdl
|
||||
#boyd.spdl
|
||||
broken1.spdl
|
||||
#carkey-broken-limited.spdl
|
||||
#carkey-broken.spdl
|
||||
carkey-ni2.spdl
|
||||
carkey-ni.spdl
|
||||
ccitt509-ban.spdl
|
||||
denning-sacco-shared.spdl
|
||||
five-run-bound.spdl
|
||||
#gong-nonce-b.spdl
|
||||
#gong-nonce.spdl
|
||||
helloworld.spdl
|
||||
isoiec11770-2-13.spdl
|
||||
#kaochow-palm.spdl
|
||||
kaochow.spdl
|
||||
ns-symmetric.spdl
|
||||
ns-symmetric-amended.spdl
|
||||
ns3-brutus.spdl
|
||||
ns3.spdl
|
||||
nsl3-nisynch-rep.spdl
|
||||
nsl3.spdl
|
||||
nsl7.spdl
|
||||
#onetrace.spdl
|
||||
otwayrees.spdl
|
||||
#samasc-broken.spdl
|
||||
#simplest.spdl
|
||||
#soph-keyexch.spdl
|
||||
#soph.spdl
|
||||
#speedtest.spdl
|
||||
splice-as-hc-cj.spdl
|
||||
#splice-as-hc.spdl
|
||||
splice-as.spdl
|
||||
#tls-paulson.spdl
|
||||
tmn.spdl
|
||||
#unknown2.spdl
|
||||
wmf-brutus.spdl
|
||||
woolam-ce.spdl
|
||||
woolam-cmv.spdl
|
||||
yahalom-ban.spdl
|
||||
yahalom-lowe.spdl
|
||||
yahalom-paulson.spdl
|
||||
yahalom.spdl
|
||||
@@ -1,34 +0,0 @@
|
||||
/*
|
||||
Samasc broken
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol samascbroken(I,R)
|
||||
{
|
||||
role R
|
||||
{
|
||||
fresh nr: Nonce;
|
||||
var kir: Key;
|
||||
|
||||
recv_!1a (I,R, { kir,I }pk(R) );
|
||||
send_!1b (R,I, {nr,R}pk(I) );
|
||||
|
||||
/* Commenting out these two lines yields an attack: */
|
||||
recv_!2a (I,R, { nr }kir );
|
||||
send_!2b (R,I, { I,R,nr }kir );
|
||||
|
||||
recv_!3 (I,R, { I,R }kir );
|
||||
|
||||
claim_4 (R, Secret, kir );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
untrusted e;
|
||||
compromised sk(e);
|
||||
@@ -1,16 +0,0 @@
|
||||
|
||||
secret k: Nonce;
|
||||
|
||||
protocol simplest(I)
|
||||
{
|
||||
role I
|
||||
{
|
||||
var x: Nonce;
|
||||
fresh n: Nonce;
|
||||
|
||||
recv_!1(I,I, x);
|
||||
send_!2(I,I, n, {n, x}k );
|
||||
claim_3(I, Secret, n);
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,32 +0,0 @@
|
||||
usertype Sessionkey;
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol sophkx(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
fresh kir: Sessionkey;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, ni, {I,kir}pk(R) );
|
||||
recv_2(R,I, {ni}kir );
|
||||
claim_4(I,Secret,kir);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
var kir: Sessionkey;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, ni, {I,kir}pk(R) );
|
||||
send_2(R,I, {ni}kir );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const ke: Sessionkey;
|
||||
|
||||
@@ -1,26 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol soph(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, ni );
|
||||
claim_3(I,Niagree);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, ni );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -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);
|
||||
|
||||
|
||||
@@ -1,44 +0,0 @@
|
||||
|
||||
|
||||
protocol myintruder (encr,decr,tupl,proj,m0)
|
||||
{
|
||||
role encr
|
||||
{
|
||||
var R,X,Y: Ticket;
|
||||
|
||||
read_e1 (R,encr, X);
|
||||
read_e2 (R,encr, Y);
|
||||
send_e3 (encr,R, {X}Y );
|
||||
}
|
||||
|
||||
role decr
|
||||
{
|
||||
var R,X: Ticket;
|
||||
|
||||
read_d1 (R,decr, {X}pk(E));
|
||||
send_d2 (decr,R, X );
|
||||
}
|
||||
|
||||
role tupl
|
||||
{
|
||||
var R,X,Y: Ticket;
|
||||
|
||||
read_t1 (R,tupl, X);
|
||||
read_t2 (R,tupl, Y);
|
||||
send_t3 (tupl,R, X,Y );
|
||||
}
|
||||
|
||||
role proj
|
||||
{
|
||||
var R,X,Y: Ticket;
|
||||
|
||||
read_p1 (R,proj, X,Y );
|
||||
send_p2 (proj,R, X );
|
||||
send_p3 (proj,R, Y );
|
||||
}
|
||||
|
||||
singular role m0
|
||||
{
|
||||
send_m0 (m0,m0, pk, pk(A), pk(B), nE, sk(E), E);
|
||||
}
|
||||
}
|
||||
@@ -1,40 +0,0 @@
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol ns3speedtest(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
recv_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim_4(I,Secret,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
claim_5(R,Secret,ni);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/* something like this will later on all be implied by 'untrusted Eve' */
|
||||
|
||||
|
||||
/* pre-defined 10 runs, limit using --max-runs parameters */
|
||||
|
||||
run ns3speedtest.R(Alice,Bob);
|
||||
run ns3speedtest.R(Eve,Bob);
|
||||
run ns3speedtest.R(Bob,Alice);
|
||||
run ns3speedtest.R(Eve,Alice);
|
||||
run ns3speedtest.R(Bob,Bob);
|
||||
@@ -1,59 +0,0 @@
|
||||
usertype TimeStamp, LifeTime;
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol spliceAShcCJ(C,AS,S)
|
||||
{
|
||||
role C
|
||||
{
|
||||
fresh N1,N2: Nonce;
|
||||
fresh T: TimeStamp;
|
||||
fresh L: LifeTime;
|
||||
|
||||
send_1(C,AS, C, S, N1 );
|
||||
recv_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
|
||||
send_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) );
|
||||
recv_6(S,C, S, C, {N2}pk(C) );
|
||||
|
||||
claim_7(C, Secret, N2);
|
||||
claim_9(C, Niagree);
|
||||
claim_10(C, Nisynch);
|
||||
}
|
||||
|
||||
role AS
|
||||
{
|
||||
var N1,N3: Nonce;
|
||||
|
||||
recv_1(C,AS, C, S, N1 );
|
||||
send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
|
||||
recv_4(S,AS, S, C, N3 );
|
||||
send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh N3: Nonce;
|
||||
var N2: Nonce;
|
||||
var T: TimeStamp;
|
||||
var L: LifeTime;
|
||||
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) );
|
||||
send_4(S,AS, S, C, N3 );
|
||||
recv_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
|
||||
send_6(S,C, S, C, {N2}pk(C) );
|
||||
|
||||
claim_8(S, Secret, N2);
|
||||
claim_11(S, Niagree);
|
||||
claim_12(S, Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,59 +0,0 @@
|
||||
usertype TimeStamp, LifeTime;
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol spliceAShc(C,AS,S)
|
||||
{
|
||||
role C
|
||||
{
|
||||
fresh N1,N2: Nonce;
|
||||
fresh T: TimeStamp;
|
||||
fresh L: LifeTime;
|
||||
|
||||
send_1(C,AS, C, S, N1 );
|
||||
recv_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
|
||||
send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
|
||||
recv_6(S,C, S, C, {S, N2}pk(C) );
|
||||
|
||||
claim_7(C, Secret, N2);
|
||||
claim_9(C, Niagree);
|
||||
claim_10(C, Nisynch);
|
||||
}
|
||||
|
||||
role AS
|
||||
{
|
||||
var N1,N3: Nonce;
|
||||
|
||||
recv_1(C,AS, C, S, N1 );
|
||||
send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
|
||||
recv_4(S,AS, S, C, N3 );
|
||||
send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh N3: Nonce;
|
||||
var N2: Nonce;
|
||||
var T: TimeStamp;
|
||||
var L: LifeTime;
|
||||
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
|
||||
send_4(S,AS, S, C, N3 );
|
||||
recv_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
|
||||
send_6(S,C, S, C, {S, N2}pk(C) );
|
||||
|
||||
claim_8(S, Secret, N2);
|
||||
claim_11(S, Niagree);
|
||||
claim_12(S, Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,59 +0,0 @@
|
||||
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;
|
||||
|
||||
send_1(C,AS, C, S, N1 );
|
||||
recv_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) );
|
||||
send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
|
||||
recv_6(S,C, S, C, {S, N2}pk(C) );
|
||||
|
||||
claim_7(C, Secret, N2);
|
||||
claim_9(C, Niagree);
|
||||
claim_10(C, Nisynch);
|
||||
}
|
||||
|
||||
role AS
|
||||
{
|
||||
var N1,N3: Nonce;
|
||||
|
||||
recv_1(C,AS, C, S, N1 );
|
||||
send_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) );
|
||||
recv_4(S,AS, S, C, N3 );
|
||||
send_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) );
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh N3: Nonce;
|
||||
var N2: Nonce;
|
||||
var T: TimeStamp;
|
||||
var L: LifeTime;
|
||||
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
recv_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
|
||||
send_4(S,AS, S, C, N3 );
|
||||
recv_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) );
|
||||
send_6(S,C, S, C, {S, N2}pk(C) );
|
||||
|
||||
claim_8(S, Secret, N2);
|
||||
claim_11(S, Niagree);
|
||||
claim_12(S, Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,63 +0,0 @@
|
||||
/*
|
||||
* This is a model of a version of the TLS protocol as modeled in
|
||||
* Boyd, Mathuria "Protocols for Authentication and key establishment"
|
||||
*
|
||||
* It's a very simplified form.
|
||||
*/
|
||||
define(`msg1',`na')
|
||||
define(`msg2',`nb')
|
||||
define(`kab',`hash(pmk,na,nb)')
|
||||
define(`msg3a',`{ pmk }pk(B)')
|
||||
define(`M1',`hash(msg1,msg2,msg3a)')
|
||||
define(`msg3b',`{ M1 }sk(A)')
|
||||
define(`M2',`hash(msg1,msg2,msg3a,msg3b)')
|
||||
define(`msg3c',`{ M2 }kab')
|
||||
define(`msg3',`msg3a,msg3b,msg3c')
|
||||
define(`M3',`msg1,msg2,msg3')
|
||||
define(`msg4',`{ M3 }kab')
|
||||
|
||||
/* below is just Scyther input and no further macro definitions */
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-bm-1(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh na: Nonce;
|
||||
fresh pmk: Nonce;
|
||||
var nb: Nonce;
|
||||
|
||||
send_1( A,B, msg1 );
|
||||
recv_2( B,A, msg2 );
|
||||
send_3( A,B, msg3 );
|
||||
recv_4( B,A, msg4 );
|
||||
|
||||
claim_A1( A, Secret, kab );
|
||||
claim_A2( A, Nisynch );
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var na: Nonce;
|
||||
var pmk: Nonce;
|
||||
fresh nb: Nonce;
|
||||
|
||||
recv_1( A,B, msg1 );
|
||||
send_2( B,A, msg2 );
|
||||
recv_3( A,B, msg3 );
|
||||
send_4( B,A, msg4 );
|
||||
|
||||
claim_B1( B, Secret, kab );
|
||||
claim_B2( B, Nisynch );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,63 +0,0 @@
|
||||
/*
|
||||
* This is a model of a version of the TLS protocol as modeled in
|
||||
* Boyd, Mathuria "Protocols for Authentication and key establishment"
|
||||
*
|
||||
* It's a very simplified form.
|
||||
*/
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
/* below is just Scyther input and no further macro definitions */
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-bm-1(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh na: Nonce;
|
||||
fresh pmk: Nonce;
|
||||
var nb: Nonce;
|
||||
|
||||
send_1( A,B, na );
|
||||
recv_2( B,A, nb );
|
||||
send_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) );
|
||||
recv_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) );
|
||||
|
||||
claim_A1( A, Secret, hash(pmk,na,nb) );
|
||||
claim_A2( A, Nisynch );
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var na: Nonce;
|
||||
var pmk: Nonce;
|
||||
fresh nb: Nonce;
|
||||
|
||||
recv_1( A,B, na );
|
||||
send_2( B,A, nb );
|
||||
recv_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) );
|
||||
send_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) );
|
||||
|
||||
claim_B1( B, Secret, hash(pmk,na,nb) );
|
||||
claim_B2( B, Nisynch );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,82 +0,0 @@
|
||||
/*
|
||||
* This is an improved model of a version of the TLS protocol as modeled by
|
||||
* He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular
|
||||
* correctness proof of IEEE 802.11i and TLS".
|
||||
*
|
||||
* Modeled by: Cas Cremers
|
||||
*
|
||||
* The original model was broken: the secret was not part of the
|
||||
* handshake, and the handshakes were not hashed. After an e-mail
|
||||
* exchange with Anupam Datta this was cleared up.
|
||||
*
|
||||
* The .cpp file cannot be fed into scyther directly; rather, one needs
|
||||
* to type: (for *nix type systems with cpp)
|
||||
*
|
||||
* cpp tls-HSDDM05-2.cpp >tls-HSDDM05-2.spdl
|
||||
*
|
||||
* in order to generate a valid spdl file for the Scyther.
|
||||
*
|
||||
* This allows for macro expansion, as seen in the next part, which is
|
||||
* particularly useful for expanding the handshakes.
|
||||
*
|
||||
*/
|
||||
#define CERT(a) { a,pk(a) }sk(Terence)
|
||||
#define msg1 X,Nx,pa
|
||||
#define msg2 Ny,pb,CERT(Y)
|
||||
#define handShake1 hash(msg1,msg2,msecret)
|
||||
#define msg3 CERT(X),{handShake1}sk(X),{msecret}pk(Y),hash(msecret,handShake1,clientstring)
|
||||
#define handShake2 hash(msg1,msg2,msg3)
|
||||
#define msg4 hash(msecret,handShake2,serverstring)
|
||||
|
||||
|
||||
/* below is just Scyther input and no further macro definitions */
|
||||
|
||||
usertype Params, String;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const clientstring,serverstring: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-HSDDM05(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh Nx: Nonce;
|
||||
fresh msecret: Nonce;
|
||||
fresh pa: Params;
|
||||
var Ny: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( X,Y, msg1 );
|
||||
recv_2( Y,X, msg2 );
|
||||
send_3( X,Y, msg3 );
|
||||
recv_4( Y,X, msg4 );
|
||||
|
||||
claim_X1( X, Secret, msecret );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var Nx: Nonce;
|
||||
var msecret: Nonce;
|
||||
var pa: Params;
|
||||
fresh Ny: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( X,Y, msg1 );
|
||||
send_2( Y,X, msg2 );
|
||||
recv_3( X,Y, msg3 );
|
||||
send_4( Y,X, msg4 );
|
||||
|
||||
claim_Y1( Y, Secret, msecret );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,53 +0,0 @@
|
||||
# 1 "tls-HSDDM05-2.cpp"
|
||||
# 1 "<built-in>"
|
||||
# 1 "<command line>"
|
||||
# 1 "tls-HSDDM05-2.cpp"
|
||||
# 34 "tls-HSDDM05-2.cpp"
|
||||
usertype Params, String;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const clientstring,serverstring: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-HSDDM05(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh Nx: Nonce;
|
||||
fresh msecret: Nonce;
|
||||
fresh pa: Params;
|
||||
var Ny: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( X,Y, X,Nx,pa );
|
||||
recv_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
|
||||
send_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) );
|
||||
recv_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) );
|
||||
|
||||
claim_X1( X, Secret, msecret );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var Nx: Nonce;
|
||||
var msecret: Nonce;
|
||||
var pa: Params;
|
||||
fresh Ny: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( X,Y, X,Nx,pa );
|
||||
send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
|
||||
recv_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) );
|
||||
send_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) );
|
||||
|
||||
claim_Y1( Y, Secret, msecret );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,72 +0,0 @@
|
||||
/*
|
||||
* This is a model of a version of the TLS protocol as modeled by
|
||||
* He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular
|
||||
* correctness proof of IEEE 802.11i and TLS".
|
||||
*
|
||||
* This is the fixed version, with quite some differences:
|
||||
*
|
||||
* 1) new definition of handShake1
|
||||
* 2) changed order in msg3
|
||||
*
|
||||
* (These are the suggestions made by Cas to Anupam Datta)
|
||||
*/
|
||||
#define CERT(a) { a,pk(a) }sk(Terence)
|
||||
#define msg1 X,Nx,pa
|
||||
#define msg2 Ny,pb,CERT(Y)
|
||||
#define handShake1 msg1,msg2,{msecret}pk(Y)
|
||||
#define msg3 CERT(X),{msecret}pk(Y),{handShake1}sk(X),hash(msecret,handShake1,clientstring)
|
||||
#define handShake2 msg1,msg2,msg3
|
||||
#define msg4 hash(msecret,handShake2,serverstring)
|
||||
|
||||
|
||||
/* below is just Scyther input and no further macro definitions */
|
||||
|
||||
usertype Params, String;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const clientstring,serverstring: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-HSDDM05(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh Nx: Nonce;
|
||||
fresh msecret: Nonce;
|
||||
fresh pa: Params;
|
||||
var Ny: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( X,Y, msg1 );
|
||||
recv_2( Y,X, msg2 );
|
||||
send_3( X,Y, msg3 );
|
||||
recv_4( Y,X, msg4 );
|
||||
|
||||
claim_X1( X, Secret, msecret );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var Nx: Nonce;
|
||||
var msecret: Nonce;
|
||||
var pa: Params;
|
||||
fresh Ny: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( X,Y, msg1 );
|
||||
send_2( Y,X, msg2 );
|
||||
recv_3( X,Y, msg3 );
|
||||
send_4( Y,X, msg4 );
|
||||
|
||||
claim_Y1( Y, Secret, msecret );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,73 +0,0 @@
|
||||
/*
|
||||
* This is a model of a version of the TLS protocol as modeled by
|
||||
* He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular
|
||||
* correctness proof of IEEE 802.11i and TLS".
|
||||
*
|
||||
* This is the fixed version, with quite some differences:
|
||||
*
|
||||
* 1) new definition of handShake1 (including preceding tuples)
|
||||
* 2) new definition of both handshakes (now hashed)
|
||||
* 3) changed order in msg3 so msecret is part of handShake1
|
||||
*
|
||||
* (These are the suggestions made by Cas to Anupam Datta)
|
||||
*/
|
||||
define(`CERTY',`{ Y,pk(Y) }sk(Terence)')
|
||||
define(`CERTX',`{ X,pk(X) }sk(Terence)')
|
||||
define(`msg1',`X,Nx,pa')
|
||||
define(`msg2',`Ny,pb,CERTY')
|
||||
define(`handShake1',`hash(msg1,msg2,{msecret}pk(Y))')
|
||||
define(`msg3',`CERTX,{msecret}pk(Y),{handShake1}sk(X),hash(msecret,handShake1,clientstring)')
|
||||
define(`handShake2',`hash(msg1,msg2,msg3)')
|
||||
define(`msg4',`hash(msecret,handShake2,serverstring)')
|
||||
|
||||
/* below is just Scyther input and no further macro definitions */
|
||||
|
||||
usertype Params, String;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const clientstring,serverstring: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-HSDDM05(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh Nx: Nonce;
|
||||
fresh msecret: Nonce;
|
||||
fresh pa: Params;
|
||||
var Ny: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( X,Y, msg1 );
|
||||
recv_2( Y,X, msg2 );
|
||||
send_3( X,Y, msg3 );
|
||||
recv_4( Y,X, msg4 );
|
||||
|
||||
claim_X1( X, Secret, msecret );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var Nx: Nonce;
|
||||
var msecret: Nonce;
|
||||
var pa: Params;
|
||||
fresh Ny: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( X,Y, msg1 );
|
||||
send_2( Y,X, msg2 );
|
||||
recv_3( X,Y, msg3 );
|
||||
send_4( Y,X, msg4 );
|
||||
|
||||
claim_Y1( Y, Secret, msecret );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,73 +0,0 @@
|
||||
/*
|
||||
* This is a model of a version of the TLS protocol as modeled by
|
||||
* He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular
|
||||
* correctness proof of IEEE 802.11i and TLS".
|
||||
*
|
||||
* This is the fixed version, with quite some differences:
|
||||
*
|
||||
* 1) new definition of handShake1 (including preceding tuples)
|
||||
* 2) new definition of both handshakes (now hashed)
|
||||
* 3) changed order in msg3 so msecret is part of handShake1
|
||||
*
|
||||
* (These are the suggestions made by Cas to Anupam Datta)
|
||||
*/
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
/* below is just Scyther input and no further macro definitions */
|
||||
|
||||
usertype Params, String;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const clientstring,serverstring: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-HSDDM05(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh Nx: Nonce;
|
||||
fresh msecret: Nonce;
|
||||
fresh pa: Params;
|
||||
var Ny: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( X,Y, X,Nx,pa );
|
||||
recv_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
|
||||
send_3( X,Y, { X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring) );
|
||||
recv_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring)),serverstring) );
|
||||
|
||||
claim_X1( X, Secret, msecret );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var Nx: Nonce;
|
||||
var msecret: Nonce;
|
||||
var pa: Params;
|
||||
fresh Ny: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( X,Y, X,Nx,pa );
|
||||
send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
|
||||
recv_3( X,Y, { X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring) );
|
||||
send_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring)),serverstring) );
|
||||
|
||||
claim_Y1( Y, Secret, msecret );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,76 +0,0 @@
|
||||
/*
|
||||
* This is a model of a version of the TLS protocol as modeled by
|
||||
* He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular
|
||||
* correctness proof of IEEE 802.11i and TLS".
|
||||
*
|
||||
* The .cpp file cannot be fed into scyther directly; rather, one needs
|
||||
* to type: (for *nix type systems with cpp)
|
||||
*
|
||||
* cpp tls-HSDDM05.cpp >tls-HSDDM05.spdl
|
||||
*
|
||||
* in order to generate a valid spdl file for the Scyther.
|
||||
*
|
||||
* This allows for macro expansion, as seen in the next part, which is
|
||||
* particularly useful for expanding the handshakes.
|
||||
*
|
||||
*/
|
||||
#define CERT(a) { a,pk(a) }sk(Terence)
|
||||
#define msg1 X,Nx,pa
|
||||
#define msg2 Ny,pb,CERT(Y)
|
||||
#define handShake1 msg1,msg2
|
||||
#define msg3 CERT(X),{handShake1}sk(X),{msecret}pk(Y),hash(msecret,handShake1,clientstring)
|
||||
#define handShake2 msg1,msg2,msg3
|
||||
#define msg4 hash(msecret,handShake2,serverstring)
|
||||
|
||||
|
||||
/* below is just Scyther input and no further macro definitions */
|
||||
|
||||
usertype Params, String;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const clientstring,serverstring: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-HSDDM05(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh Nx: Nonce;
|
||||
fresh msecret: Nonce;
|
||||
fresh pa: Params;
|
||||
var Ny: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( X,Y, msg1 );
|
||||
recv_2( Y,X, msg2 );
|
||||
send_3( X,Y, msg3 );
|
||||
recv_4( Y,X, msg4 );
|
||||
|
||||
claim_X1( X, Secret, msecret );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var Nx: Nonce;
|
||||
var msecret: Nonce;
|
||||
var pa: Params;
|
||||
fresh Ny: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( X,Y, msg1 );
|
||||
send_2( Y,X, msg2 );
|
||||
recv_3( X,Y, msg3 );
|
||||
send_4( Y,X, msg4 );
|
||||
|
||||
claim_Y1( Y, Secret, msecret );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,53 +0,0 @@
|
||||
# 1 "tls-HSDDM05.cpp"
|
||||
# 1 "<built-in>"
|
||||
# 1 "<command line>"
|
||||
# 1 "tls-HSDDM05.cpp"
|
||||
# 28 "tls-HSDDM05.cpp"
|
||||
usertype Params, String;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const clientstring,serverstring: String;
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Terence: Agent;
|
||||
|
||||
protocol tls-HSDDM05(X,Y)
|
||||
{
|
||||
role X
|
||||
{
|
||||
fresh Nx: Nonce;
|
||||
fresh msecret: Nonce;
|
||||
fresh pa: Params;
|
||||
var Ny: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( X,Y, X,Nx,pa );
|
||||
recv_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
|
||||
send_3( X,Y, { X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring) );
|
||||
recv_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) );
|
||||
|
||||
claim_X1( X, Secret, msecret );
|
||||
}
|
||||
|
||||
role Y
|
||||
{
|
||||
var Nx: Nonce;
|
||||
var msecret: Nonce;
|
||||
var pa: Params;
|
||||
fresh Ny: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( X,Y, X,Nx,pa );
|
||||
send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
|
||||
recv_3( X,Y, { X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring) );
|
||||
send_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) );
|
||||
|
||||
claim_Y1( Y, Secret, msecret );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,91 +0,0 @@
|
||||
/*
|
||||
* This is a model of the TLS version as modeled by Paulson
|
||||
*
|
||||
* Slightly modified to correspond exactly to the version in the Avispa
|
||||
* repository by Paul Hankes Drielsma.
|
||||
*
|
||||
* The .cpp file cannot be fed into scyther directly; rather, one needs
|
||||
* to type:
|
||||
*
|
||||
* cpp tls-paulson.cpp >tls-paulson.spdl
|
||||
*
|
||||
* in order to generate a valid spdl file for scyther.
|
||||
*
|
||||
* This allows for macro expansion, as seen in the next part.
|
||||
*
|
||||
*/
|
||||
|
||||
#define CERT(a) { a,pk(a) }sk(Terence)
|
||||
#define MSG a,na,sid,pa,pb,nb,sid,pb,CERT(a),CERT(b),{pms}pk(b)
|
||||
#define M hash(pms,na,nb)
|
||||
#define F hash(M,MSG)
|
||||
#define CLIENTK keygen(a,na,nb,M)
|
||||
#define SERVERK keygen(b,na,nb,M)
|
||||
|
||||
usertype Params, Bool, SessionID;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const keygen: Function;
|
||||
secret unkeygen: Function;
|
||||
inversekeys(keygen, unkeygen);
|
||||
|
||||
const pa,pb: Params;
|
||||
const false,true: Bool;
|
||||
|
||||
|
||||
protocol tlspaulson-avispa(a,b)
|
||||
{
|
||||
role a
|
||||
{
|
||||
fresh na: Nonce;
|
||||
fresh sid: SessionID;
|
||||
fresh pms: Nonce;
|
||||
var nb: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( a,b, a,na,sid,pa );
|
||||
recv_2( b,a, nb,sid,pb );
|
||||
recv_3( b,a, CERT(b) );
|
||||
send_4( a,b, CERT(a) );
|
||||
send_5( a,b, { pms }pk(b) );
|
||||
send_6( a,b, { hash(nb,b,pms) }sk(a) );
|
||||
send_7( a,b, { F }CLIENTK );
|
||||
recv_8( b,a, { F }SERVERK );
|
||||
|
||||
claim_9a(a, Secret, SERVERK);
|
||||
claim_9b(a, Secret, CLIENTK);
|
||||
claim_9c(a, Niagree);
|
||||
|
||||
}
|
||||
|
||||
role b
|
||||
{
|
||||
var na: Nonce;
|
||||
var sid: SessionID;
|
||||
var pms: Nonce;
|
||||
fresh nb: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( a,b, a,na,sid,pa );
|
||||
send_2( b,a, nb,sid,pb );
|
||||
send_3( b,a, CERT(b) );
|
||||
recv_4( a,b, CERT(a) );
|
||||
recv_5( a,b, { pms }pk(b) );
|
||||
recv_6( a,b, { hash(nb,b,pms) }sk(a) );
|
||||
recv_7( a,b, { F }CLIENTK );
|
||||
send_8( b,a, { F }SERVERK );
|
||||
|
||||
claim_10a(b, Secret, SERVERK);
|
||||
claim_10b(b, Secret, CLIENTK);
|
||||
claim_10c(b, Niagree);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const side: SessionID;
|
||||
const pe: Params;
|
||||
|
||||
@@ -1,71 +0,0 @@
|
||||
# 1 "tls-paulson-avispa.cpp"
|
||||
# 1 "<built-in>"
|
||||
# 1 "<command line>"
|
||||
# 1 "tls-paulson-avispa.cpp"
|
||||
# 25 "tls-paulson-avispa.cpp"
|
||||
usertype Params, Bool, SessionID;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const keygen: Function;
|
||||
secret unkeygen: Function;
|
||||
inversekeys(keygen, unkeygen);
|
||||
|
||||
const pa,pb: Params;
|
||||
const false,true: Bool;
|
||||
|
||||
|
||||
protocol tlspaulson-avispa(a,b)
|
||||
{
|
||||
role a
|
||||
{
|
||||
fresh na: Nonce;
|
||||
fresh sid: SessionID;
|
||||
fresh pms: Nonce;
|
||||
var nb: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( a,b, a,na,sid,pa );
|
||||
recv_2( b,a, nb,sid,pb );
|
||||
recv_3( b,a, { b,pk(b) }sk(Terence) );
|
||||
send_4( a,b, { a,pk(a) }sk(Terence) );
|
||||
send_5( a,b, { pms }pk(b) );
|
||||
send_6( a,b, { hash(nb,b,pms) }sk(a) );
|
||||
send_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(a,na,nb,hash(pms,na,nb)) );
|
||||
recv_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(b,na,nb,hash(pms,na,nb)) );
|
||||
|
||||
claim_9a(a, Secret, keygen(b,na,nb,hash(pms,na,nb)));
|
||||
claim_9b(a, Secret, keygen(a,na,nb,hash(pms,na,nb)));
|
||||
claim_9c(a, Niagree);
|
||||
|
||||
}
|
||||
|
||||
role b
|
||||
{
|
||||
var na: Nonce;
|
||||
var sid: SessionID;
|
||||
var pms: Nonce;
|
||||
fresh nb: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( a,b, a,na,sid,pa );
|
||||
send_2( b,a, nb,sid,pb );
|
||||
send_3( b,a, { b,pk(b) }sk(Terence) );
|
||||
recv_4( a,b, { a,pk(a) }sk(Terence) );
|
||||
recv_5( a,b, { pms }pk(b) );
|
||||
recv_6( a,b, { hash(nb,b,pms) }sk(a) );
|
||||
recv_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(a,na,nb,hash(pms,na,nb)) );
|
||||
send_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(b,na,nb,hash(pms,na,nb)) );
|
||||
|
||||
claim_10a(b, Secret, keygen(b,na,nb,hash(pms,na,nb)));
|
||||
claim_10b(b, Secret, keygen(a,na,nb,hash(pms,na,nb)));
|
||||
claim_10c(b, Niagree);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const side: SessionID;
|
||||
const pe: Params;
|
||||
@@ -1,82 +0,0 @@
|
||||
/*
|
||||
* This is a model of the TLS version as modeled by Paulson
|
||||
*
|
||||
* The .cpp file cannot be fed into scyther directly; rather, one needs
|
||||
* to type:
|
||||
*
|
||||
* cpp tls-paulson.cpp >tls-paulson.spdl
|
||||
*
|
||||
* in order to generate a valid spdl file for scyther.
|
||||
*
|
||||
* This allows for macro expansion, as seen in the next part.
|
||||
*
|
||||
*/
|
||||
#define CERT(a) { a,pk(a) }sk(Terence)
|
||||
#define MSG a,na,sid,pa,pb,nb,sid,pb,CERT(a),CERT(b),{pms}pk(b)
|
||||
#define M hash(pms,na,nb)
|
||||
#define F hash(M,MSG)
|
||||
#define CLIENTK hash(sid,M,na,pa,a,nb,pb,b,false)
|
||||
#define SERVERK hash(sid,M,na,pa,a,nb,pb,b,true)
|
||||
|
||||
usertype Params, Bool, SessionID;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const pa,pb: Params;
|
||||
const false,true: Bool;
|
||||
|
||||
|
||||
protocol tlspaulson(a,b)
|
||||
{
|
||||
role a
|
||||
{
|
||||
fresh na: Nonce;
|
||||
fresh sid: SessionID;
|
||||
fresh pms: Nonce;
|
||||
var nb: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( a,b, a,na,sid,pa );
|
||||
recv_2( b,a, nb,sid,pb );
|
||||
recv_3( b,a, CERT(b) );
|
||||
send_4( a,b, CERT(a) );
|
||||
send_5( a,b, { pms }pk(b) );
|
||||
send_6( a,b, { hash(nb,b,pms) }sk(a) );
|
||||
send_7( a,b, { F }CLIENTK );
|
||||
recv_8( b,a, { F }SERVERK );
|
||||
|
||||
claim_9a(a, Secret, SERVERK);
|
||||
claim_9b(a, Secret, CLIENTK);
|
||||
|
||||
}
|
||||
|
||||
role b
|
||||
{
|
||||
var na: Nonce;
|
||||
var sid: SessionID;
|
||||
var pms: Nonce;
|
||||
fresh nb: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( a,b, a,na,sid,pa );
|
||||
send_2( b,a, nb,sid,pb );
|
||||
send_3( b,a, CERT(b) );
|
||||
recv_4( a,b, CERT(a) );
|
||||
recv_5( a,b, { pms }pk(b) );
|
||||
recv_6( a,b, { hash(nb,b,pms) }sk(a) );
|
||||
recv_7( a,b, { F }CLIENTK );
|
||||
send_8( b,a, { F }SERVERK );
|
||||
|
||||
claim_10a(b, Secret, SERVERK);
|
||||
claim_10b(b, Secret, CLIENTK);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const side: SessionID;
|
||||
const pe: Params;
|
||||
|
||||
|
||||
@@ -1,66 +0,0 @@
|
||||
# 1 "tls-paulson.cpp"
|
||||
# 1 "<built-in>"
|
||||
# 1 "<command line>"
|
||||
# 1 "tls-paulson.cpp"
|
||||
# 21 "tls-paulson.cpp"
|
||||
usertype Params, Bool, SessionID;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
inversekeys(pk,sk);
|
||||
inversekeys(hash,unhash);
|
||||
|
||||
const pa,pb: Params;
|
||||
const false,true: Bool;
|
||||
|
||||
|
||||
protocol tlspaulson(a,b)
|
||||
{
|
||||
role a
|
||||
{
|
||||
fresh na: Nonce;
|
||||
fresh sid: SessionID;
|
||||
fresh pms: Nonce;
|
||||
var nb: Nonce;
|
||||
var pb: Params;
|
||||
|
||||
send_1( a,b, a,na,sid,pa );
|
||||
recv_2( b,a, nb,sid,pb );
|
||||
recv_3( b,a, { b,pk(b) }sk(Terence) );
|
||||
send_4( a,b, { a,pk(a) }sk(Terence) );
|
||||
send_5( a,b, { pms }pk(b) );
|
||||
send_6( a,b, { hash(nb,b,pms) }sk(a) );
|
||||
send_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) );
|
||||
recv_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) );
|
||||
|
||||
claim_9a(a, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true));
|
||||
claim_9b(a, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false));
|
||||
|
||||
}
|
||||
|
||||
role b
|
||||
{
|
||||
var na: Nonce;
|
||||
var sid: SessionID;
|
||||
var pms: Nonce;
|
||||
fresh nb: Nonce;
|
||||
fresh pb: Params;
|
||||
|
||||
recv_1( a,b, a,na,sid,pa );
|
||||
send_2( b,a, nb,sid,pb );
|
||||
send_3( b,a, { b,pk(b) }sk(Terence) );
|
||||
recv_4( a,b, { a,pk(a) }sk(Terence) );
|
||||
recv_5( a,b, { pms }pk(b) );
|
||||
recv_6( a,b, { hash(nb,b,pms) }sk(a) );
|
||||
recv_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) );
|
||||
send_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) );
|
||||
|
||||
claim_10a(b, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true));
|
||||
claim_10b(b, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const side: SessionID;
|
||||
const pe: Params;
|
||||
|
||||
@@ -1,52 +0,0 @@
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys(pk,sk);
|
||||
|
||||
protocol tmn(A,B,S)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ka: Key;
|
||||
var Kb: Key;
|
||||
|
||||
send_1(A,S, B,{Ka}pk(S) );
|
||||
recv_4(S,A, B,{Kb}Ka );
|
||||
|
||||
#claim_5(A,Secret,Ka);
|
||||
#claim_8(A,Secret,Kb);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
fresh Kb: Key;
|
||||
|
||||
recv_2(S,B, A );
|
||||
send_3(B,S, A, { Kb }pk(S) );
|
||||
|
||||
claim_6(B,Secret,Kb);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var Ka,Kb: Key;
|
||||
|
||||
recv_1(A,S, B,{Ka}pk(S) );
|
||||
send_2(S,B, A );
|
||||
recv_3(B,S, A, { Kb }pk(S) );
|
||||
send_4(S,A, B,{Kb}Ka );
|
||||
|
||||
#claim_7(S,Secret,Ka);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve,Simon: Agent;
|
||||
const Ke: Key;
|
||||
|
||||
|
||||
|
||||
# Scenario to recreate an attack in SPORE
|
||||
|
||||
|
||||
@@ -1,48 +0,0 @@
|
||||
usertype Key;
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys(pk,sk);
|
||||
|
||||
protocol tmn(A,B,S)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ka: Key;
|
||||
var Kb: Key;
|
||||
|
||||
send_1(A,S, B,{Ka}pk(S) );
|
||||
recv_4(S,A, B,{Kb}Ka );
|
||||
|
||||
claim_5(A,Secret,Ka);
|
||||
claim_8(A,Secret,Kb);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
fresh Kb: Key;
|
||||
|
||||
recv_2(S,B, A );
|
||||
send_3(B,S, A, { Kb }pk(S) );
|
||||
|
||||
claim_6(B,Secret,Kb);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var Ka,Kb: Key;
|
||||
|
||||
recv_1(A,S, B,{Ka}pk(S) );
|
||||
send_2(S,B, A );
|
||||
recv_3(B,S, A, { Kb }pk(S) );
|
||||
send_4(S,A, B,{Kb}Ka );
|
||||
|
||||
claim_7(S,Secret,Ka);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve,Simon: Agent;
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,55 +0,0 @@
|
||||
usertype SessionKey;
|
||||
secret k: Function;
|
||||
|
||||
protocol unknown2(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: SessionKey;
|
||||
var T;
|
||||
|
||||
send_1(I,R, ni );
|
||||
recv_3(S,I, { I,R,kir,ni,nr }k(I,S), T );
|
||||
send_4(I,R, T, {nr}kir );
|
||||
|
||||
claim_i1(I,Nisynch);
|
||||
claim_i2(I,Niagree);
|
||||
claim_i3(I,Secret, kir);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
fresh nr: Nonce;
|
||||
var ni: Nonce;
|
||||
var kir: SessionKey;
|
||||
|
||||
recv_1(I,R, ni );
|
||||
send_2(R,S, { I,R,ni,nr }k(R,S) );
|
||||
recv_4(I,R, { I,R,kir,ni,nr }k(R,S), {nr}kir );
|
||||
|
||||
claim_r1(R,Nisynch);
|
||||
claim_r2(R,Niagree);
|
||||
claim_r3(R,Secret, kir);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh kir: SessionKey;
|
||||
var ni,nr: Nonce;
|
||||
|
||||
recv_2(R,S, { I,R,ni,nr }k(R,S) );
|
||||
send_3(S,I, { I,R,kir,ni,nr }k(I,S), { I,R,kir,ni,nr }k(R,S) );
|
||||
|
||||
/*
|
||||
claim_s1(S,Nisynch);
|
||||
claim_s2(S,Niagree);
|
||||
claim_s3(S,Secret, kir);
|
||||
*/
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
const kee: SessionKey;
|
||||
|
||||
@@ -1,39 +0,0 @@
|
||||
usertype SesKey, Server;
|
||||
secret fresh k : Function;
|
||||
|
||||
/* Version from the Brutus reports
|
||||
*/
|
||||
|
||||
protocol wmfbrutus(A,B,S)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh kab : SesKey;
|
||||
|
||||
send_1(A,S, A, { B,kab }k(A,S) );
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var kab : SesKey;
|
||||
|
||||
recv_2(S,B, { A, kab }k(B,S) );
|
||||
|
||||
claim_3(B, Secret,kab);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var kab : SesKey;
|
||||
|
||||
recv_1(A,S, A, { B,kab }k(A,S) );
|
||||
send_2(S,B, { A, kab }k(B,S) );
|
||||
}
|
||||
}
|
||||
|
||||
const Alice, Bob, Eve: Agent;
|
||||
const Simon: Server;
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,69 +0,0 @@
|
||||
/*
|
||||
* Woo-lam version from Spore, as it is in Sjouke's list
|
||||
*/
|
||||
|
||||
usertype Server, SessionKey, Token, Ticket;
|
||||
secret k: Function;
|
||||
|
||||
const Simon: Server;
|
||||
|
||||
/* give the intruder something to work with */
|
||||
// Scyther finds an attack using basic type flaws
|
||||
|
||||
const ke: SessionKey;
|
||||
|
||||
const authToken: Token;
|
||||
|
||||
protocol woolamcmv(A,B,S)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Na: Nonce;
|
||||
var Nb: Nonce;
|
||||
var Kab: SessionKey;
|
||||
var t1,t2;
|
||||
|
||||
send_1(A,B, A,Na);
|
||||
recv_2(B,A, B,Nb);
|
||||
send_3(A,B, { A,B, Na,Nb }k(A,S) );
|
||||
recv_6(B,A, { B,Na,Nb,Kab }k(A,S), { Na,Nb }Kab );
|
||||
send_7(A,B, { Nb }Kab );
|
||||
|
||||
claim_8(A,Secret, Kab);
|
||||
claim_9(A,Niagree);
|
||||
claim_10(A,Nisynch);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
var Na: Nonce;
|
||||
fresh Nb: Nonce;
|
||||
var Kab: SessionKey;
|
||||
var t1,t2;
|
||||
|
||||
recv_1(A,B, A,Na);
|
||||
send_2(B,A, B,Nb);
|
||||
recv_3(A,B, t1 );
|
||||
send_4(B,S, t1, { A,B,Na,Nb }k(B,S) );
|
||||
recv_5(S,B, t2, { A,Na,Nb,Kab }k(B,S) );
|
||||
send_6(B,A, t2, { Na,Nb }Kab );
|
||||
recv_7(A,B, { Nb }Kab );
|
||||
|
||||
claim_11(B,Secret, Kab);
|
||||
claim_12(B,Niagree);
|
||||
claim_13(B,Nisynch);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var Na, Nb: Nonce;
|
||||
fresh Kab: SessionKey;
|
||||
|
||||
recv_4(B,S, { A,B, Na,Nb }k(A,S), { A,B,Na,Nb }k(B,S) );
|
||||
send_5(S,B, { B,Na,Nb,Kab }k(A,S), { A,Na,Nb,Kab }k(B,S) );
|
||||
|
||||
claim_14(S,Secret, Kab);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,49 +0,0 @@
|
||||
/*
|
||||
* Woo-lam version from Spore, Pi f
|
||||
*
|
||||
* Only one-way verification version
|
||||
*/
|
||||
|
||||
usertype Server, SessionKey, Ticket;
|
||||
secret k: Function;
|
||||
|
||||
const Simon: Server;
|
||||
|
||||
const ke: SessionKey;
|
||||
|
||||
protocol woolampif(A,B,S)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var Nb: Nonce;
|
||||
|
||||
send_1(A,B, A);
|
||||
recv_2(B,A, Nb);
|
||||
send_3(A,B, { A,B,Nb }k(A,S) );
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
fresh Nb: Nonce;
|
||||
var T: Ticket;
|
||||
|
||||
recv_1(A,B, A);
|
||||
send_2(B,A, Nb);
|
||||
recv_3(A,B, T);
|
||||
send_4(B,S, { A,B,Nb, T }k(B,S) );
|
||||
recv_5(S,B, { A,B,Nb }k(B,S) );
|
||||
|
||||
claim_6(B,Niagree);
|
||||
claim_7(B,Nisynch);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
var Nb: Nonce;
|
||||
|
||||
recv_4(B,S, { A,B,Nb, { A,B,Nb }k(A,S) }k(B,S) );
|
||||
send_5(S,B, { A,B,Nb }k(B,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,51 +0,0 @@
|
||||
// BAN modified version of the yahalom protocol
|
||||
// Type flaw
|
||||
// This version actually works!
|
||||
|
||||
usertype Server;
|
||||
|
||||
const a,b,c : Agent;
|
||||
const s : Server;
|
||||
secret k : Function;
|
||||
|
||||
|
||||
|
||||
|
||||
protocol yahalomBan(A,B,S)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh na;
|
||||
var nb;
|
||||
var ticket;
|
||||
var kab;
|
||||
|
||||
send_1(A,B, A,na);
|
||||
recv_3(S,A, nb, {B,kab,na}k(A,S), ticket );
|
||||
send_4(A,B, ticket, {nb}kab );
|
||||
claim_5(A, Secret,kab);
|
||||
}
|
||||
|
||||
role B
|
||||
{
|
||||
fresh nb;
|
||||
var na;
|
||||
var ticket;
|
||||
var kab;
|
||||
|
||||
recv_1(A,B, A,na);
|
||||
send_2(B,S, B,nb, {A,na}k(B,S) );
|
||||
recv_4(A,B, {A,kab,nb}k(B,S) , {nb}kab );
|
||||
claim_6(B, Secret,kab);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh kab;
|
||||
var na,nb;
|
||||
|
||||
recv_2(B,S, B,nb, {A,na}k(B,S) );
|
||||
send_3(S,A, nb, {B,kab,na}k(A,S), {A,kab,nb}k(B,S) );
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,56 +0,0 @@
|
||||
/*
|
||||
* Yahalom Lowe
|
||||
* As in Sjouke's list
|
||||
*/
|
||||
|
||||
usertype Sessionkey;
|
||||
|
||||
secret k : Function;
|
||||
|
||||
const kee: Sessionkey;
|
||||
|
||||
protocol yahalomlowe(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Sessionkey;
|
||||
|
||||
send_1(I,R, I,ni);
|
||||
recv_3(S,I, {R,kir,ni,nr}k(I,S) );
|
||||
send_5(I,R, {I,R,S,nr}kir );
|
||||
|
||||
claim_8(I, Secret,kir);
|
||||
claim_9(I, Niagree);
|
||||
claim_10(I, Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
fresh nr: Nonce;
|
||||
var ni: Nonce;
|
||||
var kir: Sessionkey;
|
||||
|
||||
recv_1(I,R, I,ni);
|
||||
send_2(R,S, {I,ni,nr}k(R,S) );
|
||||
recv_4(S,R, {I,kir}k(R,S) );
|
||||
recv_5(I,R, {I,R,S,nr}kir );
|
||||
claim_11(R, Secret,kir);
|
||||
claim_12(R, Nisynch);
|
||||
claim_13(R, Niagree);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh kir: Sessionkey;
|
||||
var ni,nr: Nonce;
|
||||
|
||||
recv_2(R,S, {I,ni,nr}k(R,S) );
|
||||
send_3(S,I, {R,kir,ni,nr}k(I,S) );
|
||||
send_4(S,R, {I,kir}k(R,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,56 +0,0 @@
|
||||
/*
|
||||
* Yahalom Paulson-strengthened
|
||||
* As in Sjouke's list
|
||||
*/
|
||||
|
||||
usertype Sessionkey, Ticket;
|
||||
|
||||
secret k : Function;
|
||||
|
||||
const kee: Sessionkey;
|
||||
|
||||
protocol yahalompaulson(I,R,S)
|
||||
{
|
||||
role I
|
||||
{
|
||||
fresh ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Sessionkey;
|
||||
var T: Ticket;
|
||||
|
||||
send_1(I,R, I,ni);
|
||||
recv_3(S,I, nr, {R,kir,ni}k(I,S), T );
|
||||
send_4(I,R, T, {nr}kir );
|
||||
|
||||
claim_8(I, Secret,kir);
|
||||
claim_9(I, Nisynch);
|
||||
claim_10(I, Niagree);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
fresh nr: Nonce;
|
||||
var ni: Nonce;
|
||||
var kir: Sessionkey;
|
||||
|
||||
recv_1(I,R, I,ni);
|
||||
send_2(R,S, R,nr,{I,ni}k(R,S) );
|
||||
recv_4(I,R, {I,R,kir,nr}k(R,S), {nr}kir );
|
||||
|
||||
claim_11(R, Secret,kir);
|
||||
claim_12(R, Nisynch);
|
||||
claim_13(R, Niagree);
|
||||
}
|
||||
|
||||
role S
|
||||
{
|
||||
fresh kir: Sessionkey;
|
||||
var ni,nr: Nonce;
|
||||
|
||||
recv_2(R,S, R,nr, {I,ni}k(R,S) );
|
||||
send_3(S,I, nr, { R,kir,ni }k(I,S), {I,R,kir,nr}k(R,S) );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@@ -1,776 +0,0 @@
|
||||
Slave1:multiparty% ./test-heuristics.py
|
||||
Starting with [11, 15]
|
||||
Testing using P 3 and 5 runs.
|
||||
Testing protocol 11.
|
||||
Heuristic 0:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=0 --timer=20
|
||||
states 7488
|
||||
attack NoClaim
|
||||
time 2.007e+01
|
||||
st/sec 3.731e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 1:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=1 --timer=20
|
||||
states 3869
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 1.931e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 2:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=2 --timer=20
|
||||
states 6543
|
||||
attack NoClaim
|
||||
time 2.006e+01
|
||||
st/sec 3.262e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 3:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=3 --timer=20
|
||||
states 9003
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 4.490e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 1 correct: bounded_proof
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 4:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=4 --timer=20
|
||||
states 6375
|
||||
attack NoClaim
|
||||
time 2.008e+01
|
||||
st/sec 3.175e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 5:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=5 --timer=20
|
||||
states 4282
|
||||
attack NoClaim
|
||||
time 2.007e+01
|
||||
st/sec 2.134e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 4 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 6:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=6 --timer=20
|
||||
states 6791
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 3.392e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 7:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=7 --timer=20
|
||||
states 8115
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 4.049e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 14 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 8:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=8 --timer=20
|
||||
states 9649
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 4.817e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 9:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=9 --timer=20
|
||||
states 3873
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 1.932e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 10:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=10 --timer=20
|
||||
states 11954
|
||||
attack NoClaim
|
||||
time 2.007e+01
|
||||
st/sec 5.956e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 11:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=11 --timer=20
|
||||
states 7367
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 3.678e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 12:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=12 --timer=20
|
||||
states 6271
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 3.128e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 13:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=13 --timer=20
|
||||
states 4729
|
||||
attack NoClaim
|
||||
time 2.006e+01
|
||||
st/sec 2.357e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 14:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=14 --timer=20
|
||||
states 7566
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 3.779e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 15:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=15 --timer=20
|
||||
states 8496
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 4.237e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 16:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=16 --timer=20
|
||||
states 7453
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 3.721e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 17:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=17 --timer=20
|
||||
states 3888
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 1.940e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 18:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=18 --timer=20
|
||||
states 6582
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 3.286e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 19:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=19 --timer=20
|
||||
states 9022
|
||||
attack NoClaim
|
||||
time 2.001e+01
|
||||
st/sec 4.509e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 1 correct: bounded_proof
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 20:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=20 --timer=20
|
||||
states 6393
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 3.192e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 21:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=21 --timer=20
|
||||
states 4284
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 2.140e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 4 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 22:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=22 --timer=20
|
||||
states 6769
|
||||
attack NoClaim
|
||||
time 2.001e+01
|
||||
st/sec 3.383e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 23:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=23 --timer=20
|
||||
states 8175
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 4.083e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 14 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 24:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=24 --timer=20
|
||||
states 9625
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 4.805e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 25:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=25 --timer=20
|
||||
states 3883
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 1.940e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 26:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=26 --timer=20
|
||||
states 11992
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 5.984e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 27:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=27 --timer=20
|
||||
states 7361
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 3.673e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 28:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=28 --timer=20
|
||||
states 6277
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 3.132e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 29:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=29 --timer=20
|
||||
states 4728
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 2.358e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 30:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=30 --timer=20
|
||||
states 7610
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 3.797e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 31:
|
||||
./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=31 --timer=20
|
||||
states 8506
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 4.247e+02
|
||||
claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Testing protocol 15.
|
||||
Heuristic 0:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=0 --timer=20
|
||||
states 7499
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 3.744e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 1:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=1 --timer=20
|
||||
states 3866
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 1.929e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 2:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=2 --timer=20
|
||||
states 6558
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 3.274e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 3:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=3 --timer=20
|
||||
states 8933
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 4.462e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 1 correct: bounded_proof
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 4:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=4 --timer=20
|
||||
states 6354
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 3.174e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 5:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=5 --timer=20
|
||||
states 4278
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 2.135e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 4 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 6:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=6 --timer=20
|
||||
states 6749
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 3.371e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 7:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=7 --timer=20
|
||||
states 8166
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 4.077e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 14 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 8:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=8 --timer=20
|
||||
states 9805
|
||||
attack NoClaim
|
||||
time 2.006e+01
|
||||
st/sec 4.888e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 9:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=9 --timer=20
|
||||
states 3873
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 1.933e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 10:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=10 --timer=20
|
||||
states 10729
|
||||
attack NoClaim
|
||||
time 2.006e+01
|
||||
st/sec 5.348e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 11:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=11 --timer=20
|
||||
states 6679
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 3.331e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 12:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=12 --timer=20
|
||||
states 6119
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 3.052e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 13:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=13 --timer=20
|
||||
states 3513
|
||||
attack NoClaim
|
||||
time 2.009e+01
|
||||
st/sec 1.749e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 14:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=14 --timer=20
|
||||
states 7548
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 3.766e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 15:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=15 --timer=20
|
||||
states 8461
|
||||
attack NoClaim
|
||||
time 2.002e+01
|
||||
st/sec 4.226e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 16:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=16 --timer=20
|
||||
states 7503
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 3.746e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 17:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=17 --timer=20
|
||||
states 3837
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 1.916e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 18:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=18 --timer=20
|
||||
states 6537
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 3.260e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 19:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=19 --timer=20
|
||||
states 8893
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 4.438e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 1 correct: bounded_proof
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 20:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=20 --timer=20
|
||||
states 6325
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 3.158e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 21:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=21 --timer=20
|
||||
states 4253
|
||||
attack NoClaim
|
||||
time 2.005e+01
|
||||
st/sec 2.121e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 4 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 22:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=22 --timer=20
|
||||
states 6756
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 3.371e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 23:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=23 --timer=20
|
||||
states 8149
|
||||
attack NoClaim
|
||||
time 2.003e+01
|
||||
st/sec 4.068e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 14 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 24:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=24 --timer=20
|
||||
states 9785
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 4.883e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 25:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=25 --timer=20
|
||||
states 3832
|
||||
attack NoClaim
|
||||
time 2.006e+01
|
||||
st/sec 1.910e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 26:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=26 --timer=20
|
||||
states 10699
|
||||
attack NoClaim
|
||||
time 2.009e+01
|
||||
st/sec 5.326e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 27:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=27 --timer=20
|
||||
states 6672
|
||||
attack NoClaim
|
||||
time 2.006e+01
|
||||
st/sec 3.326e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 28:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=28 --timer=20
|
||||
states 6136
|
||||
attack NoClaim
|
||||
time 2.010e+01
|
||||
st/sec 3.053e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 29:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=29 --timer=20
|
||||
states 3521
|
||||
attack NoClaim
|
||||
time 2.009e+01
|
||||
st/sec 1.753e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 30:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=30 --timer=20
|
||||
states 7584
|
||||
attack NoClaim
|
||||
time 2.006e+01
|
||||
st/sec 3.781e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
Heuristic 31:
|
||||
./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=31 --timer=20
|
||||
states 8369
|
||||
attack NoClaim
|
||||
time 2.004e+01
|
||||
st/sec 4.176e+02
|
||||
claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20
|
||||
claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur
|
||||
claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20
|
||||
|
||||
|
||||
13,25 work well.
|
||||
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user