/*****************************************************************
  Simplified Needham-Schroeder Protocol
  original version by  R. Okabe, 2007-12-27
  last update by K. Ueda, 2010-06-12
 
  A->B : Na
  B->A : Na,Nb
  A->B : Nb
 
  Original description in MSR:
    I. Cervesato, N.A. Durgin, P.D. Lincoln, J.C. Mitchell, A. Scedrov.
    A Meta-notation for Protocol Analysis, CSFW'99, pp.55-69, 1999
  Encoding in LMNtal:
    T. Ayano et al., T. Hori, H. Iwasawa, S. Ogawa and K. Ueda,
    LMNtal Model Checking using an Integrated Development Environment.
    To appear in Computer Software, 2010.   
******************************************************************/
 
/* An atom name is composed of an agent name and its state number.
   Arguments of an atom stand for data held by the atom.  
   Nonces are represented by membranes, and references to nonces
   are represented by links to membranes. */

// alice creates a nonce, sends it and remembers it
a0 :- n1(A0), a1(A1), {+A0,+A1}.

// bob receives it, creates a new nonce,
// sends it and remembers it 
b0, n1(A0), {+A0,$a} :-
      n2(A1,B1), b1(A2,B2), {+A1,+A2,$a}, {+B1,+B2}.
      
// alice receives it and replies      
n2(A0,B0), a1(A1), {+A0,+A1,$a}, {+B0,$b} :-
      n3(B1), a2(A2,B2), {+A2,$a}, {+B1,+B2,$b}.
      
// bob receives alice's final message
n3(B0), b1(A0,B1), {+A0,$a}, {+B0,+B1,$b} :-
      b2(A1,B2), {+A1,$a}, {+B2,$b}.
      
// alice and bob in initial state
a0, b0.

/* intruder; m( ) stands for its memory.
   i1, i3 and i5 steal messages; i2, i4 and i6 insert messages;
   i7 forges a new message.  Atoms s and g are to control the
   number of applications of i2, i4, i6 and i7. */
    
i1@@ n1(X) :- m(X).
i2@@ s, m(X), {+X,$x} :- n1(X1), m(X2), {+X1,+X2,$x}.
i3@@ n2(X,Y) :- m(X), m(Y).
i4@@ s, m(X), m(Y), {+X,$x}, {+Y,$y} :-
	   n2(X1,Y1), m(X2), m(Y2), {+X1,+X2,$x}, {+Y1,+Y2,$y}.
i5@@ n3(X) :- m(X).
i6@@ s, m(X), {+X,$x} :- n3(X1), m(X2), {+X1,+X2,$x}.
i7@@ g :- m(N), {+N,i}.

s, s, g.
