scyther/gui/ns3.spdl

48 lines
728 B
Plaintext
Raw Permalink Normal View History

2006-08-02 13:59:57 +01:00
/*
* Needham-Schroeder protocol
*/
// The protocol description
protocol ns3(I,R)
{
role I
{
fresh ni: Nonce;
2006-08-02 13:59:57 +01:00
var nr: Nonce;
2007-05-19 17:02:36 +01:00
send_1(I,R, {ni,I}pk(R) );
recv_2(R,I, {ni,nr}pk(I) );
claim(I,Running,R,ni,nr);
2006-08-02 13:59:57 +01:00
send_3(I,R, {nr}pk(R) );
claim(I,Secret,ni);
claim(I,Secret,nr);
claim(I,Alive);
2012-05-01 15:37:04 +01:00
claim(I,Weakagree);
claim(I,Commit,R,ni,nr);
claim(I,Niagree);
claim(I,Nisynch);
2006-08-02 13:59:57 +01:00
}
role R
{
var ni: Nonce;
fresh nr: Nonce;
2006-08-02 13:59:57 +01:00
recv_1(I,R, {ni,I}pk(R) );
claim(R,Running,I,ni,nr);
2006-08-02 13:59:57 +01:00
send_2(R,I, {ni,nr}pk(I) );
recv_3(I,R, {nr}pk(R) );
2006-08-02 13:59:57 +01:00
claim(R,Secret,ni);
claim(R,Secret,nr);
claim(R,Alive);
2012-05-01 15:37:04 +01:00
claim(R,Weakagree);
claim(R,Commit,I,ni,nr);
claim(R,Niagree);
claim(R,Nisynch);
2006-08-02 13:59:57 +01:00
}
}