scyther/gui/ns3.spdl
2012-05-01 16:37:04 +02:00

48 lines
728 B
Plaintext

/*
* Needham-Schroeder protocol
*/
// The protocol description
protocol ns3(I,R)
{
role I
{
fresh ni: Nonce;
var nr: Nonce;
send_1(I,R, {ni,I}pk(R) );
recv_2(R,I, {ni,nr}pk(I) );
claim(I,Running,R,ni,nr);
send_3(I,R, {nr}pk(R) );
claim(I,Secret,ni);
claim(I,Secret,nr);
claim(I,Alive);
claim(I,Weakagree);
claim(I,Commit,R,ni,nr);
claim(I,Niagree);
claim(I,Nisynch);
}
role R
{
var ni: Nonce;
fresh nr: Nonce;
recv_1(I,R, {ni,I}pk(R) );
claim(R,Running,I,ni,nr);
send_2(R,I, {ni,nr}pk(I) );
recv_3(I,R, {nr}pk(R) );
claim(R,Secret,ni);
claim(R,Secret,nr);
claim(R,Alive);
claim(R,Weakagree);
claim(R,Commit,I,ni,nr);
claim(R,Niagree);
claim(R,Nisynch);
}
}