(mod! PRIN {
	[Prin]
	*** adf
	op intr : -> Prin . *** adf
	ops p q : -> Prin .
	op _eqs_ : Prin Prin -> Bool {comm} .
	var P : Prin .
	eq (P eqs P) = true .
})


(mod! RAND {
  [Rand]
  op seed : -> Rand  .
  op next : Rand -> Rand .
  op _eqs_ : Rand Rand -> Bool {comm} .
  vars R R1 R2 : Rand .
  eq (R eqs R) = true .
  eq (seed eqs next(R)) = false .
  eq (R eqs next(R)) = false .
  eq (next(R1) eqs next(R2)) = (R1 eqs R2) .
})

(
mod! NONCE {
  pr(PRIN)
  pr(RAND)
  [Nonce]
  op n : Prin Prin Rand -> Nonce .
  op p1 : Nonce -> Prin .
  op p2 : Nonce -> Prin .
  op r  : Nonce -> Rand .
  op _eqs_ : Nonce Nonce -> Bool {comm} .
  vars P1 P2 P12 P22 : Prin .
  vars R R1 R2 : Rand .
  var N : Nonce .
  eq p1(n(P1,P2,R)) = P1 .
  eq p2(n(P1,P2,R)) = P2 .
  eq r(n(P1,P2,R))  = R .
  eq (N eqs N) = true .
  eq (n(P1,P2,R1) eqs n(P12,P22,R2)) = (P1 eqs P12 and P2 eqs P22 and R1 eqs R2) .
})


(mod! CIPHER {
  pr(NONCE)
  [Cipher1 Cipher2 Cipher3 < Cipher]
  
  op enc1 : Prin Nonce Prin -> Cipher1 .
  op enc2 : Prin Nonce Nonce -> Cipher2 .
  op enc3 : Prin Nonce -> Cipher3 .
  op k    : Cipher -> Prin .
  op n1   : Cipher -> Nonce .
  op n2   : Cipher2 -> Nonce .
  op p    : Cipher1 -> Prin .
  op _eqs_  : Cipher Cipher -> Bool {comm} .
  vars K K1 K2 : Prin .
  vars N1 N2 N11 N21 N12 N22 : Nonce .
  vars P P1 P2 : Prin .
  var C : Cipher .
  eq k(enc1(K,N1,P)) = K .
  eq k(enc2(K,N1,N2)) = K .
  eq k(enc3(K,N1)) = K .
  eq n1(enc1(K,N1,P)) = N1 .
  eq n1(enc2(K,N1,N2)) = N1 .
  eq n1(enc3(K,N1)) = N1 .
  eq n2(enc2(K,N1,N2)) = N2 .
  eq p(enc1(K,N1,P)) = P .
  eq (C eqs C) = true .
  eq (enc1(K1,N11,P1) eqs enc1(K2,N12,P2)) = (K1 eqs K2 and N11 eqs N12 and P1 eqs P2) .
  eq (enc1(K1,N11,P1) eqs enc2(K2,N12,N22)) = false .
  eq (enc1(K1,N11,P1) eqs enc3(K2,N12)) = false .
  eq (enc2(K1,N11,N21) eqs enc2(K2,N12,N22)) = (K1 eqs K2 and N11 eqs N12 and N21 eqs N22) .
  eq (enc2(K1,N11,N21) eqs enc3(K2,N12)) = false .
  eq (enc3(K1,N11) eqs enc3(K2,N12)) = (K1 eqs K2 and N11 eqs N12) .
})

(
mod! NONCESET {
  pr(NONCE)
  [Nonce < NonceSet]
  op empty : -> NonceSet .
  op __ : NonceSet NonceSet -> NonceSet {assoc comm } .
  op _\in_ : Nonce NonceSet -> Bool .
  op del : NonceSet Nonce -> NonceSet .
  op _eqs_ : NonceSet NonceSet -> Bool {comm} .
  vars N N1 N2 N' N1' N2' : Nonce .
  vars S S' : NonceSet .
  eq N N = N . 
  eq N \in empty = false .
  eq N \in (N1 S) = (N eqs N1 or N \in S) .
  eq del(empty,N) = empty .
  eq del(N1 S,N) = if N1 eqs N then S else N1 del(S,N) fi .
  eq (S eqs S) = true .
  eq (N S eqs empty) = false .
  eq (N1 N2 S eqs N') = false .
  eq (N1 N2 S eqs N1' N2' S')
     = if N1 \in (N1' N2' S') and N2 \in (N1' N2' S')
       then S eqs del(del(N1' N2' S',N1),N2) else false fi .
})

(mod! MSG {
  pr(CIPHER)
  [Msg]
  op m : Prin Prin Prin Cipher -> Msg .
  op c : Msg -> Prin .
  op s : Msg -> Prin .
  op r : Msg -> Prin .
  op b : Msg -> Cipher .
  op _eqs_ : Msg Msg -> Bool {comm} .
  vars M M' : Msg .
  vars C C1 : Prin .
  vars S S1 : Prin .
  vars R R1 : Prin .
  vars B B1 : Cipher .
  eq c(m(C,S,R,B)) = C .
  eq s(m(C,S,R,B)) = S .
  eq r(m(C,S,R,B)) = R .
  eq b(m(C,S,R,B)) = B .
  eq (M eqs M) = true .
  eq (m(C,S,R,B) eqs m(C1,S1,R1,B1)) 
     = (C eqs C1 and S eqs S1 and R eqs R1 and B eqs B1) .
})

(
mod! NETWORK {
  pr(MSG)
  [Msg < MsgSet]
  op empty : -> MsgSet .
  op __ : MsgSet MsgSet -> MsgSet {assoc comm  id: empty} .
  op _\in_ : Msg MsgSet -> Bool .
  op del : MsgSet Msg -> MsgSet .
  op _eqs_ : MsgSet MsgSet -> Bool {comm} .
  vars M M1 M2 M' M1' M2' : Msg .
  vars NW NW' : MsgSet .
  eq M M = M . *** idempotency
  eq M \in empty = false .
  eq M \in (M1 NW) = (M eqs M1 or M \in NW) .
  eq del(empty,M) = empty .
  eq del(M1 NW,M) = if M1 eqs M then NW else M1 del(NW,M) fi .
  eq (NW eqs NW) = true .
  eq (M NW eqs empty) = false .
  eq (M1 M2 NW eqs M') = false .
  eq (M1 M2 NW eqs M1' M2' NW')
     = if M1 \in (M1' M2' NW') and M2 \in (M1' M2' NW')
       then NW eqs del(del(M1' M2' NW',M1),M2) else false fi .
})

(

mod! PRINSET {
  pr(PRIN)
  [Prin < PrinSet]
  op empty : -> PrinSet .
  op __ : PrinSet PrinSet -> PrinSet {assoc comm id: empty} .
  op _\in_ : Prin PrinSet -> Bool .
  op del : PrinSet Prin -> PrinSet .
  op _eqs_ : PrinSet PrinSet -> Bool {comm} .
  vars P P1 P2 P' P1' P2' : Prin .
  vars S S' : PrinSet .
  eq P P = P . 
  eq P \in empty = false .
  eq P \in (P1 S) = (P eqs P1 or P \in S) .
  eq del(empty,P) = empty .
  eq del(P1 S,P) = if P1 eqs P then S else P1 del(S,P) fi .
  eq (S eqs S) = true .
  eq (P S eqs empty) = false .
  eq (P1 P2 S eqs P') = false .
  eq (P1 P2 S eqs P1' P2' S')
     = if P1 \in (P1' P2' S') and P2 \in (P1' P2' S')
       then S eqs del(del(P1' P2' S',P1),P2) else false fi .
})

( mod* OTS-NSPK {
  pr(NONCESET)
  pr(NETWORK)
  pr(PRINSET)
  *[Sys]*
  --- an arbitrary initial state
  op init : -> Sys .
  --- observers
  bop rand   : Sys -> Rand .
  bop nw     : Sys -> MsgSet .
  bop nonces : Sys -> NonceSet .
  --- actions
  bop send1 : Sys Prin Prin -> Sys .
  bop send2 : Sys Prin Prin Prin Nonce -> Sys .
  bop send3 : Sys Prin Prin Prin Nonce Nonce -> Sys .
  bop fake1 : Sys Prin Prin Nonce -> Sys .
  bop fake2 : Sys Prin Prin Nonce Nonce -> Sys .
  bop fake3 : Sys Prin Prin Nonce -> Sys .
  bop fake4 : Sys Prin Prin Msg -> Sys .
  --- CafeOBJ variables
  var S : Sys .
  vars P1 P2 P3 : Prin .
  vars N N1 N2 : Nonce .
  var M : Msg .
  var NW : MsgSet .
  --- init
  eq rand(init)   = seed .
  eq nw(init)     = empty .
  eq nonces(init) = empty .
  
  eq rand(send1(S,P1,P2))   = next(rand(S))  .
  eq nw(send1(S,P1,P2))     = m(P1,P1,P2,enc1(P2,n(P1,P2,rand(S)),P1)) nw(S) .
  eq nonces(send1(S,P1,P2)) = 
      if P2 eqs intr then n(P1,P2,rand(S)) nonces(S) else nonces(S) fi .
  


  op c-send2 : Sys Prin Prin Prin Nonce -> Bool .
  eq c-send2(S,P1,P2,P3,N) = m(P3,P2,P1,enc1(P1,N,P2)) \in nw(S) .
  ---
  ceq rand(send2(S,P1,P2,P3,N))   = next(rand(S)) if c-send2(S,P1,P2,P3,N) .
  ceq nw(send2(S,P1,P2,P3,N))
      = m(P1,P1,P2,enc2(P2,N,n(P1,P2,rand(S)))) nw(S) if c-send2(S,P1,P2,P3,N) .
  ceq nonces(send2(S,P1,P2,P3,N))  = if P2 eqs intr then (N n(P1,P2,rand(S)) nonces(S)) else nonces(S) fi
      if c-send2(S,P1,P2,P3,N) .

  ceq send2(S,P1,P2,P3,N)         = S if not c-send2(S,P1,P2,P3,N) .



  
  --- send3
  op c-send3 : Sys Prin Prin Prin Nonce Nonce -> Bool .
  eq c-send3(S,P1,P2,P3,N1,N2)
     = m(P3,P2,P1,enc2(P1,N1,N2)) \in nw(S) and m(P1,P1,P2,enc1(P2,N1,P1)) \in nw(S) .
  ---
  ceq  rand(send3(S,P1,P2,P3,N1,N2))   = rand(S) if c-send3(S,P1,P2,P3,N1,N2) .
  ceq nw(send3(S,P1,P2,P3,N1,N2)) = (m(P1,P1,P2,enc3(P2,N2)) nw(S)) if c-send3(S,P1,P2,P3,N1,N2) .
  ceq nonces(send3(S,P1,P2,P3,N1,N2)) = if P2 eqs intr then (N2 nonces(S)) else nonces(S) fi 
      if c-send3(S,P1,P2,P3,N1,N2) .
  ceq send3(S,P1,P2,P3,N1,N2)         = S if not c-send3(S,P1,P2,P3,N1,N2) .

  
  
 --- fake1
  op c-fake1 : Sys Prin Prin Nonce -> Bool .
  eq c-fake1(S,P1,P2,N) = N \in nonces(S) .
  ---
  ceq  rand(fake1(S,P1,P2,N))   = rand(S)  if c-fake1(S,P1,P2,N) .
  ceq nw(fake1(S,P1,P2,N))     = m(intr,P1,P2,enc1(P2,N,P1)) nw(S) if c-fake1(S,P1,P2,N) .
  ceq  nonces(fake1(S,P1,P2,N)) = nonces(S) if c-fake1(S,P1,P2,N) .
  ceq fake1(S,P1,P2,N)         = S if not c-fake1(S,P1,P2,N) .
  
  --- fake2
  op c-fake2 : Sys Prin Prin Nonce Nonce -> Bool .
  eq c-fake2(S,P1,P2,N1,N2) = N1 \in nonces(S) and N2 \in nonces(S) .
  ---
  ceq  rand(fake2(S,P1,P2,N1,N2))   = rand(S) if c-fake2(S,P1,P2,N1,N2) .
  ceq nw(fake2(S,P1,P2,N1,N2))
      = m(intr,P1,P2,enc2(P2,N1,N2)) nw(S) if c-fake2(S,P1,P2,N1,N2) .
  ceq  nonces(fake2(S,P1,P2,N1,N2)) = nonces(S) if c-fake2(S,P1,P2,N1,N2) .
  ceq fake2(S,P1,P2,N1,N2)         = S if not c-fake2(S,P1,P2,N1,N2) .
  
  --- fake3
  op c-fake3 : Sys Prin Prin Nonce -> Bool .
  eq c-fake3(S,P1,P2,N) = N \in nonces(S) .
  ---
  ceq  rand(fake3(S,P1,P2,N))   = rand(S) if c-fake3(S,P1,P2,N) .
  ceq nw(fake3(S,P1,P2,N))     = m(intr,P1,P2,enc3(P2,N)) nw(S) if c-fake3(S,P1,P2,N) .
  ceq  nonces(fake3(S,P1,P2,N)) = nonces(S) if c-fake3(S,P1,P2,N) .
  ceq fake3(S,P1,P2,N)         = S if not c-fake3(S,P1,P2,N) .
  
  
  --- fake4
  op c-fake4 : Sys Prin Prin Msg -> Bool .
  eq c-fake4(S,P1,P2,M) = M \in nw(S) .
  ---
  ceq  rand(fake4(S,P1,P2,M))   = rand(S) if c-fake4(S,P1,P2,M) .
  ceq nw(fake4(S,P1,P2,M))     = m(intr,P1,P2,b(M)) nw(S) if c-fake4(S,P1,P2,M) .
  ceq  nonces(fake4(S,P1,P2,M)) = nonces(S) if c-fake4(S,P1,P2,M) .
  
  ceq fake4(S,P1,P2,M)         = S if not c-fake4(S,P1,P2,M) .
  

  }
)