fmod PRIN is
  sort Prin .
  ops intr p1 p2 : -> Prin .
endfm

fmod RAND is
  sort Rand .
  op seed : -> Rand .
  op next : Rand -> Rand .
endfm

fmod NONCE is
  pr PRIN .
  pr RAND .
  sort Nonce .
  op n : Prin Prin Rand -> Nonce .
  op p1 : Nonce -> Prin .
  op p2 : Nonce -> Prin .
  op r  : Nonce -> Rand .
  vars P1 P2 : Prin .
  var R : Rand .
  eq p1(n(P1,P2,R)) = P1 .
  eq p2(n(P1,P2,R)) = P2 .
  eq r(n(P1,P2,R))  = R .
endfm

fmod CIPHER is
  pr NONCE .
  sorts Cipher1 Cipher2 Cipher3 Cipher .
  subsorts 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 .
  var K : Prin .
  vars N1 N2 : Nonce .
  var P : Prin .
  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 .
endfm

fmod MSG is
  pr CIPHER .
  sort Msg .
  op m : Prin Prin Prin Cipher -> Msg .
  op c : Msg -> Prin .
  op s : Msg -> Prin .
  op r : Msg -> Prin .
  op b : Msg -> Cipher .
  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 .
endfm

fmod NONCESET is
  pr NONCE .
  sort NonceSet .
  subsort Nonce < NonceSet .
  op empty : -> NonceSet .
  op __ : NonceSet NonceSet -> NonceSet [assoc comm id: empty] .
  op _\in_ : Nonce NonceSet -> Bool .
  var N : Nonce .
  var B : NonceSet .
  eq N N = N . *** idempotency
  eq N \in (N B) = true .
  eq N \in B = false [owise] .
endfm

fmod NETWORK is
  pr MSG .
  sort Network .
  subsort Msg < Network .
  op empty : -> Network .
  op __ : Network Network -> Network [assoc comm id: empty] .
  op _\in_ : Msg Network -> Bool .
  var M : Msg .
  var NW : Network .
  eq M M = M . *** idempotency
  eq M \in (M NW) = true .
  eq M \in NW = false [owise] .
endfm

fmod PRINSET is
  pr PRIN .
  sort PrinSet .
  subsort Prin < PrinSet .
  op empty : -> PrinSet .
  op __ : PrinSet PrinSet -> PrinSet [assoc comm id: empty] .
  op _\in_ : Prin PrinSet -> Bool .
  var P : Prin .
  var B : PrinSet .
  eq P P = P . *** idempotency
  eq P \in (P B) = true .
  eq P \in B = false [owise] .
endfm

mod NSPK is
  pr NONCESET .
  pr NETWORK .
  pr PRINSET .
  sorts Trans Obs Sys .
  subsorts Trans Obs < Sys .
  *** Configuration
  op none : -> Sys .
  op __ : Sys Sys -> Sys [assoc comm id: none] .
  *** Observation
  op prins:_  : PrinSet  -> Obs . *** Principals involved
  op rand:_   : Rand     -> Obs . *** Random number
  op nw:_     : Network  -> Obs . *** Network
  op nonces:_ : NonceSet -> Obs . *** Nonces gleaned by the intruder
  *** Transitions
  *** Maude variables
  var R : Rand .
  vars N N1 N2 : Nonce .
  vars P1 P2 P3 : Prin .
  var M : Msg .
  var NW : Network .
  var Ns : NonceSet .
  var Ps : PrinSet .
  *** Transition rules
  *** send1
  rl [send1] : 
    (prins: (P1 P2 Ps)) (rand: R) (nw: NW) (nonces: Ns)
    => (prins: (P1 P2 Ps)) (rand: next(R)) (nw: (m(P1,P1,P2,enc1(P2,n(P1,P2,R),P1)) NW))
       (nonces: (if P2 == intr then n(P1,P2,R) Ns else Ns fi)) .
  *** send2
  rl [send2] :
    (rand: R) (nw: (m(P3,P2,P1,enc1(P1,N,P2)) NW)) (nonces: Ns)
    => (rand: next(R))
       (nw: (m(P1,P1,P2,enc2(P2,N,n(P1,P2,R))) m(P3,P2,P1,enc1(P1,N,P2)) NW))
       (nonces: (if P2 == intr then N n(P1,P2,R) Ns else Ns fi)) .
  *** send3
  rl [send3] :
    (nw: (m(P3,P2,P1,enc2(P1,N1,N2)) m(P1,P1,P2,enc1(P2,N1,P1)) NW))
    (nonces: Ns)
    => (nw: (m(P1,P1,P2,enc3(P2,N2)) m(P3,P2,P1,enc2(P1,N1,N2)) m(P1,P1,P2,enc1(P2,N1,P1)) NW))
       (nonces: (if P2 == intr then N2 Ns else Ns fi)) .
  *** fake1
  rl [fake1] :
    (prins: (P1 P2 Ps)) (nw: NW) (nonces: (N Ns)) 
    => (prins: (P1 P2 Ps)) (nw: (m(intr,P1,P2,enc1(P2,N,P1)) NW)) (nonces: (N Ns)) . 
  *** fake2
  rl [fake2] :
    (prins: (P1 P2 Ps)) (nw: NW) (nonces: (N1 N2 Ns))
    => (prins: (P1 P2 Ps)) (nw: (m(intr,P1,P2,enc2(P2,N1,N2)) NW)) (nonces: (N1 N2 Ns)) .
  *** fake3
  rl [fake3] :
    (prins: (P1 P2 Ps)) (nw: NW) (nonces: (N Ns))
    => (prins: (P1 P2 Ps)) (nw: (m(intr,P1,P2,enc3(P2,N)) NW)) (nonces: (N Ns)) .
  *** fake4
  rl [fake4] :
    (prins: (P1 P2 Ps)) (nw: (M NW))
    => (prins: (P1 P2 Ps))  (nw: (m(intr,P1,P2,b(M)) M NW)) .
endm

mod NSPK-INIT is
  pr NSPK .
  op init : -> Sys .
  vars N N1 N2 : Nonce .
  vars P1 P2 P3 P4 P5 : Prin .
  var Ns : NonceSet .
  var NW : Network .
  var R : Rand .
  var S : Sys .
  eq init = (prins: (p1 p2 intr)) (rand: seed) (nw: empty) (nonces: empty) .
endm  

eof

***
*** The reachable state space seems too big, actually unbounded.
***
search [1] in NSPK-INIT : init
=>* (nw: (m(P1,P1,P2,enc1(P2,N1,P1)) m(P3,P2,P1,enc2(P1,N1,N2)) NW)) S
such that not((P1 =/= intr) implies
              m(P2,P2,P1,enc2(P1,N1,N2)) \in (m(P3,P2,P1,enc2(P1,N1,N2)) NW)) .

***
*** Even the bounded reachable state space whose depth is 6 seems too big.
***
search [1,6] in NSPK-INIT : init
=>* (nw: (m(P1,P1,P2,enc1(P2,N1,P1)) m(P3,P2,P1,enc2(P1,N1,N2)) NW)) S
such that not((P1 =/= intr) implies
              m(P2,P2,P1,enc2(P1,N1,N2)) \in (m(P3,P2,P1,enc2(P1,N1,N2)) NW)) .
              
***
*** No counterexample is found in the bounded reachable state space whose depth is 5.
***
search [1,5] in NSPK-INIT : init
=>* (nw: (m(P1,P1,P2,enc1(P2,N1,P1)) m(P3,P2,P1,enc2(P1,N1,N2)) NW)) S
such that not((P1 =/= intr) implies
              m(P2,P2,P1,enc2(P1,N1,N2)) \in (m(P3,P2,P1,enc2(P1,N1,N2)) NW)) .

***
*** No counterexample is found in the bounded reachable state space whose depth is 5.
***
search [1,5] in NSPK-INIT : init
=>* (nw: (m(P2,P2,P1,enc2(P1,N1,N2)) m(P3,P1,P2,enc3(P2,N2)) NW)) S
such that not((P2 =/= intr) implies
              m(P1,P1,P2,enc3(P2,N2)) \in (m(P3,P1,P2,enc3(P2,N2)) NW)) .

***
*** A counterexample is found.
***
search [1,5] in NSPK-INIT : init
=>* (nonces: (N Ns)) S such that not(p1(N) == intr or p2(N) == intr) .
show path 417126 .