- Updated many protocols according to the tests.
This commit is contained in:
parent
70d076644d
commit
3ee392ca08
@ -40,13 +40,14 @@ protocol bkepk(A,B,testnonce)
|
||||
{
|
||||
var n: Nonce;
|
||||
|
||||
read_4 (A,A, n);
|
||||
read_4 (testnonce,testnonce, n);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve;
|
||||
|
||||
compromised sk(Eve);
|
||||
untrusted Eve;
|
||||
|
||||
|
||||
run bkepk.A(Alice,Bob,Alice);
|
||||
|
@ -1,5 +1,5 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (BKEPK)
|
||||
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.
|
||||
@ -12,7 +12,7 @@ secret sk: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol bkepk(A,B,testnonce)
|
||||
protocol bkepkCE2(A,B,testnonce)
|
||||
{
|
||||
role B
|
||||
{
|
||||
@ -40,22 +40,23 @@ protocol bkepk(A,B,testnonce)
|
||||
{
|
||||
var n: Nonce;
|
||||
|
||||
read_4 (A,A, n);
|
||||
read_4 (testnonce,testnonce, n);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve;
|
||||
|
||||
compromised sk(Eve);
|
||||
untrusted Eve;
|
||||
|
||||
|
||||
run bkepk.A(Alice,Bob,Alice);
|
||||
run bkepk.A(Alice,Bob,Alice);
|
||||
run bkepk.A(Alice,Bob,Alice);
|
||||
run bkepk.B(Alice,Bob,Alice);
|
||||
run bkepk.B(Alice,Bob,Alice);
|
||||
run bkepk.B(Alice,Bob,Alice);
|
||||
run bkepkCE2.A(Alice,Bob,Alice);
|
||||
run bkepkCE2.A(Alice,Bob,Alice);
|
||||
run bkepkCE2.A(Alice,Bob,Alice);
|
||||
run bkepkCE2.B(Alice,Bob,Alice);
|
||||
run bkepkCE2.B(Alice,Bob,Alice);
|
||||
run bkepkCE2.B(Alice,Bob,Alice);
|
||||
|
||||
run bkepk.testnonce(Alice,Bob,Alice);
|
||||
run bkepk.testnonce(Alice,Bob,Alice);
|
||||
run bkepk.testnonce(Alice,Bob,Alice);
|
||||
run bkepkCE2.testnonce(Alice,Bob,Alice);
|
||||
run bkepkCE2.testnonce(Alice,Bob,Alice);
|
||||
run bkepkCE2.testnonce(Alice,Bob,Alice);
|
||||
|
@ -22,7 +22,7 @@ protocol broken1(I,R,S)
|
||||
{
|
||||
read_3(S, R, {HelloWorld, S, I, R}k );
|
||||
read_1(I, R, PlainSight, {HelloWorld, I, R}k );
|
||||
claim(R, Secret, PlainSight);
|
||||
claim_4(R, Secret, PlainSight);
|
||||
}
|
||||
role S
|
||||
{
|
||||
|
@ -9,7 +9,6 @@ protocol carkeybroken(I,R)
|
||||
const ni: Nonce;
|
||||
|
||||
send_1(I,R, I,R );
|
||||
claim_3(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
|
@ -9,7 +9,6 @@ protocol carkeybroken(I,R)
|
||||
const ni: Nonce;
|
||||
|
||||
send_1(I,R, {ni}sk(I) );
|
||||
claim_3(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
|
@ -9,7 +9,6 @@ protocol carkeyni(I,R)
|
||||
const ni: Nonce;
|
||||
|
||||
send_1(I,R, {R,ni}sk(I) );
|
||||
claim_3(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
|
@ -10,7 +10,6 @@ protocol carkeyni(I,R)
|
||||
|
||||
send_1(I,R, {R,ni}sk(I) );
|
||||
send_2(I,R, {R,ni}sk(I) );
|
||||
claim_5(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
|
@ -4,20 +4,6 @@ inversekeys (pk,sk);
|
||||
|
||||
protocol r5bound(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
const k1: Nonce;
|
||||
const ni: Nonce;
|
||||
var k2: Nonce;
|
||||
|
||||
send_1 (I,R, ni );
|
||||
read_2 (R,I, { ni }sk(R) );
|
||||
send_3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) );
|
||||
read_4 (R,I, {k2}k1 );
|
||||
|
||||
claim_5 (I, Secret, k2);
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var k1: Nonce;
|
||||
@ -34,18 +20,13 @@ protocol r5bound(I,R)
|
||||
}
|
||||
|
||||
const Alice, Bob: Agent;
|
||||
const ne: Nonce;
|
||||
|
||||
run r5bound.I(Agent,Agent);
|
||||
run r5bound.R(Agent,Agent);
|
||||
run r5bound.I(Agent,Agent);
|
||||
run r5bound.R(Agent,Agent);
|
||||
run r5bound.R(Agent);
|
||||
run r5bound.R(Agent);
|
||||
|
||||
run r5bound.I(Agent,Agent);
|
||||
run r5bound.R(Agent,Agent);
|
||||
run r5bound.I(Agent,Agent);
|
||||
run r5bound.R(Agent,Agent);
|
||||
run r5bound.R(Agent);
|
||||
run r5bound.R(Agent);
|
||||
|
||||
run r5bound.I(Agent,Agent);
|
||||
run r5bound.R(Agent,Agent);
|
||||
run r5bound.I(Agent,Agent);
|
||||
run r5bound.R(Agent,Agent);
|
||||
run r5bound.R(Agent);
|
||||
run r5bound.R(Agent);
|
||||
|
@ -6,7 +6,7 @@ protocol hw(initiator,world)
|
||||
role initiator
|
||||
{
|
||||
send_1(initiator, world, HelloWorld);
|
||||
claim_2(initiator, Secret, HelloWorld);
|
||||
/* claim_2(initiator, Secret, HelloWorld); */
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -2,7 +2,7 @@ const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol ns3(I,R)
|
||||
protocol ns3brutus(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
@ -12,7 +12,7 @@ protocol ns3(I,R)
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
read_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim(I,Secret,nr);
|
||||
claim_4(I,Secret,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
@ -23,7 +23,7 @@ protocol ns3(I,R)
|
||||
read_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
claim(I,Secret,ni);
|
||||
claim_5(I,Secret,ni);
|
||||
}
|
||||
}
|
||||
|
||||
@ -38,13 +38,13 @@ compromised sk(Eve);
|
||||
/* pre-defined 10 runs, limit using --max-runs parameters */
|
||||
/* to be nice to brutus, stupid scenario :( */
|
||||
|
||||
run ns3.R(Agent,Bob);
|
||||
run ns3.I(Alice,Agent);
|
||||
run ns3.R(Agent,Bob);
|
||||
run ns3.I(Alice,Agent);
|
||||
run ns3.R(Agent,Bob);
|
||||
run ns3.I(Alice,Agent);
|
||||
run ns3.R(Agent,Bob);
|
||||
run ns3.I(Alice,Agent);
|
||||
run ns3.R(Agent,Bob);
|
||||
run ns3.I(Alice,Agent);
|
||||
run ns3brutus.R(Agent,Bob);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
run ns3brutus.R(Agent,Bob);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
run ns3brutus.R(Agent,Bob);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
run ns3brutus.R(Agent,Bob);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
run ns3brutus.R(Agent,Bob);
|
||||
run ns3brutus.I(Alice,Agent);
|
||||
|
@ -13,6 +13,7 @@ protocol ns3(I,R)
|
||||
read_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim_4(I,Nisynch);
|
||||
claim_5(I,Secret, ni,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
@ -23,14 +24,15 @@ protocol ns3(I,R)
|
||||
read_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
claim_5(R,Nisynch);
|
||||
claim_6(R,Nisynch);
|
||||
claim_7(R,Secret, ni,nr);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve: Agent;
|
||||
|
||||
untrusted Eve;
|
||||
const nc: Nonce;
|
||||
const ne: Nonce;
|
||||
compromised sk(Eve);
|
||||
|
||||
run ns3.I(Agent,Agent);
|
||||
|
@ -2,7 +2,7 @@ const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol ns3(I,R)
|
||||
protocol ns3var(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
@ -12,7 +12,7 @@ protocol ns3(I,R)
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
read_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim(I,Secret,ni,nr);
|
||||
claim_4(I,Secret,ni,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
@ -23,7 +23,7 @@ protocol ns3(I,R)
|
||||
read_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
claim(R,Secret,ni,nr);
|
||||
claim_5(R,Secret,ni,nr);
|
||||
}
|
||||
}
|
||||
|
||||
@ -33,5 +33,5 @@ untrusted Eve;
|
||||
const nc: Nonce;
|
||||
compromised sk(Eve);
|
||||
|
||||
run ns3.I(Agent,Agent);
|
||||
run ns3.R(Agent,Agent);
|
||||
run ns3var.I(Agent,Agent);
|
||||
run ns3var.R(Agent,Agent);
|
||||
|
@ -13,6 +13,7 @@ protocol nsl3(I,R)
|
||||
read_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim_4(I,Nisynch);
|
||||
claim_5(I,Secret,ni,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
@ -23,14 +24,15 @@ protocol nsl3(I,R)
|
||||
read_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
claim_5(R,Nisynch);
|
||||
claim_6(R,Nisynch);
|
||||
claim_7(R,Secret,ni,nr);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve: Agent;
|
||||
|
||||
untrusted Eve;
|
||||
const nc: Nonce;
|
||||
const ne: Nonce;
|
||||
compromised sk(Eve);
|
||||
|
||||
run nsl3.I(Agent,Agent);
|
||||
|
@ -12,7 +12,7 @@ protocol nsl3(I,R)
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
read_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim(I,Secret,ni,nr);
|
||||
claim_4(I,Secret,ni,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
@ -23,7 +23,7 @@ protocol nsl3(I,R)
|
||||
read_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
claim(I,Secret,ni,nr);
|
||||
claim_5(I,Secret,ni,nr);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -12,11 +12,11 @@ protocol nsl7(I,R)
|
||||
read_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
claim(I,Secret,nr,ni);
|
||||
claim_4(I,Secret,nr,ni);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob;
|
||||
|
||||
run nsl3.R(Alice,Bob);
|
||||
run nsl3.R(Alice,Bob);
|
||||
run nsl7.R(Alice,Bob);
|
||||
run nsl7.R(Alice,Bob);
|
||||
|
@ -12,6 +12,7 @@ protocol onetrace(I)
|
||||
read_1(I,I, input);
|
||||
send_2(I,I, Hallo);
|
||||
read_3(I,I, input);
|
||||
claim_4(I, Secret, input);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -10,8 +10,9 @@ protocol simplest(I)
|
||||
var x: Nonce;
|
||||
const n: Nonce;
|
||||
|
||||
read(I,I, x);
|
||||
send(I,I, n, {n, x}k );
|
||||
read_1(I,I, x);
|
||||
send_2(I,I, n, {n, x}k );
|
||||
claim_3(I, Secret, n);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -10,7 +10,7 @@ protocol soph(I,R)
|
||||
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
read_2(R,I, ni );
|
||||
claim_4(I,Niagree);
|
||||
claim_3(I,Niagree);
|
||||
}
|
||||
|
||||
role R
|
||||
|
@ -2,7 +2,7 @@ const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
protocol ns3(I,R)
|
||||
protocol ns3speedtest(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
@ -12,7 +12,7 @@ protocol ns3(I,R)
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
read_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim(I,Secret,nr);
|
||||
claim_4(I,Secret,nr);
|
||||
}
|
||||
|
||||
role R
|
||||
@ -23,7 +23,7 @@ protocol ns3(I,R)
|
||||
read_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
claim(I,Secret,ni);
|
||||
claim_5(I,Secret,ni);
|
||||
}
|
||||
}
|
||||
|
||||
@ -37,13 +37,13 @@ compromised sk(Eve);
|
||||
|
||||
/* pre-defined 10 runs, limit using --max-runs parameters */
|
||||
|
||||
run ns3.I(Alice,Bob);
|
||||
run ns3.R(Alice,Bob);
|
||||
run ns3.I(Alice,Eve);
|
||||
run ns3.R(Eve,Bob);
|
||||
run ns3.I(Bob,Alice);
|
||||
run ns3.R(Bob,Alice);
|
||||
run ns3.I(Bob,Eve);
|
||||
run ns3.R(Eve,Alice);
|
||||
run ns3.I(Alice,Alice);
|
||||
run ns3.R(Bob,Bob);
|
||||
run ns3speedtest.I(Alice,Bob);
|
||||
run ns3speedtest.R(Alice,Bob);
|
||||
run ns3speedtest.I(Alice,Eve);
|
||||
run ns3speedtest.R(Eve,Bob);
|
||||
run ns3speedtest.I(Bob,Alice);
|
||||
run ns3speedtest.R(Bob,Alice);
|
||||
run ns3speedtest.I(Bob,Eve);
|
||||
run ns3speedtest.R(Eve,Alice);
|
||||
run ns3speedtest.I(Alice,Alice);
|
||||
run ns3speedtest.R(Bob,Bob);
|
||||
|
@ -29,7 +29,7 @@ protocol woolamce(A,B,S)
|
||||
send_6(B,A, { B,(Na,(Nb,Kab)) }Kas, { Na,Nb }Kab );
|
||||
read_7(A,B, { Nb }Kab );
|
||||
|
||||
claim(B,Secret,authToken);
|
||||
claim_8(B,Secret,authToken);
|
||||
}
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user