- Added 2r890 exercise 3, year 2004/2005. Check with assignment notes

because I did them off the top of my head.
This commit is contained in:
ccremers 2005-04-18 05:48:28 +00:00
parent de2c9c0127
commit 06a0a6c234
2 changed files with 103 additions and 0 deletions

52
spdl/2r890-ex3-a.spdl Normal file
View File

@ -0,0 +1,52 @@
/*
* 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
{
const nx: Nonce;
const ny: Nonce;
send_1(I,X, nx );
read_2(X,I, { nx,I }sk(X) );
send_3(I,Y, ny );
read_4(Y,I, { I,ny }sk(Y) );
claim_i1(I,Niagree);
claim_i2(I,Nisynch);
}
role X
{
var nx: Nonce;
read_1(I,X, nx );
send_2(X,I, { nx,I }sk(X) );
}
role Y
{
var ny: Nonce;
read_3(I,Y, ny );
send_4(Y,I, { I,ny }sk(Y) );
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);

51
spdl/2r890-ex3-b.spdl Normal file
View File

@ -0,0 +1,51 @@
/*
* 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
{
const ni: Nonce;
send_1(I,X, ni );
read_2(X,I, { ni,I }sk(X) );
send_3(I,Y, ni );
read_4(Y,I, { I,ni }sk(Y) );
claim_i1(I,Niagree);
claim_i2(I,Nisynch);
}
role X
{
var nx: Nonce;
read_1(I,X, nx );
send_2(X,I, { nx,I }sk(X) );
}
role Y
{
var ny: Nonce;
read_3(I,Y, ny );
send_4(Y,I, { I,ny }sk(Y) );
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);