***(
The informal journal-level description of this protocol is as follows:

A --> B: A
A --> B: B
A --> B: exp(g,N_A)
B --> A: B
B --> A: A
B --> A: exp(g,N_B)

where N_A and N_B are nonces, and exp(x,y) means raising message y to 
exponent x. Moreover, concatenation and encription/decription
have the following property:

  exp(exp(X,Y),Z) = exp(X, Y * Z)

However, note that this property is restricted below by using appopriate sorts
in such a way that variable X can be only the generator g. This is necessary
to have a finitary unification procedure based on narrowing.
)***

fmod PROTOCOL-EXAMPLE-SYMBOLS is
  --- Importing sorts Msg, Fresh, Public
  protecting DEFINITION-PROTOCOL-RULES .
  
  ----------------------------------------------------------
  --- Overwrite this module with the syntax of your protocol
  --- Notes:
  --- * Sort Msg and Fresh are special and imported
  --- * Every sort must be a subsort of Msg
  --- * No sort can be a supersort of Msg
  ----------------------------------------------------------

  --- Sort Information 
  sorts Name Nonce NeNonceSet Gen Exp GenvExp .
  subsort Gen Exp < GenvExp .
  subsort Name NeNonceSet GenvExp < Msg .
  subsort Name < Public . --- This is quite relevant and necessary
  subsort Gen < Public . --- This is quite relevant and necessary

  --- Nonce operator
  op n : Name Fresh -> Nonce [frozen] .

  --- Intruder
  ops a b i : -> Name .

  --- Exp
  op exp : GenvExp NeNonceSet -> Exp [frozen] .

  --- Gen
  op g : -> Gen .

  --- NeNonceSet
  subsort Nonce < NeNonceSet .
  op _*_ : NeNonceSet NeNonceSet -> NeNonceSet [frozen assoc comm] .

endfm

fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  
  ----------------------------------------------------------
  --- Overwrite this module with the algebraic properties 
  --- of your protocol
  ----------------------------------------------------------
  
  eq exp(exp(W:Gen,Y:NeNonceSet),Z:NeNonceSet) 
   = exp(W:Gen, Y:NeNonceSet * Z:NeNonceSet) [nonexec metadata "variant"] .

endfm

fmod PROTOCOL-SPECIFICATION is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  protecting DEFINITION-PROTOCOL-RULES .
  protecting DEFINITION-CONSTRAINTS-INPUT .

  ----------------------------------------------------------
  --- Overwrite this module with the strands 
  --- of your protocol
  ----------------------------------------------------------
  
  vars NS1 NS2 NS : NeNonceSet .
  var G : GenvExp .
  var A : Name .
  var r : Fresh .
  vars XE YE : Exp .

  eq STRANDS-DOLEVYAO
   = :: nil :: [ nil | -(NS1), -(NS2), +(NS1 * NS2), nil ] &
     :: nil :: [ nil | -(G), -(NS), +(exp(G,NS)), nil ] &
     :: r :: [ nil | +(n(i,r)), nil ] &
     :: nil :: [ nil | +(g), nil ] &
     :: nil :: [ nil | +(A), nil ]
  [nonexec] .

  eq STRANDS-PROTOCOL
   = :: r :: [nil | +(a), +(b), +(exp(g,n(a,r))), -(b), -(a), -(XE), nil] &
     :: r :: [nil | -(a), -(b), -(YE), +(b), +(a), +(exp(g,n(b,r))), nil]
  [nonexec] .

  eq ATTACK-STATE(0)
   = :: r :: 
     [nil, +(a), +(b), +(exp(g,n(a,r))), -(b), -(a), -(exp(g,NS)) | nil]
     || exp(g, NS * n(a,r)) inI
     || nil
     || nil
     || nil
  [nonexec] .

endfm

--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .