fmod PRIN is
  pr NAT .
  sorts Client Server Prin .
  subsorts Client Server < Prin .
  ops c ic : -> Client [ctor] .
  ops s is : -> Server [ctor] .
endfm

fmod RAND is
  pr NAT .
  sort Rand .
  op r : Nat -> Rand [ctor] .
  op dr : -> Rand [ctor] . --- dummy
endfm

fmod BASE is
  sort Base .
  op g : -> Base [ctor] .
endfm

fmod VALUE is
  pr PRIN .
  pr RAND .
  pr BASE .
  sort Value .
  subsorts Rand Base < Value .
  op _^_ : Value Value -> Value [prec 10] .
  op _*_ : Value Value -> Value [assoc comm prec 20] .
  vars X Y Z : Value .
  eq (X ^ Y) ^ Z = X ^ (Y * Z) .
endfm

fmod MSG is
  pr VALUE .
  sorts Msg Msg1 Msg2 .
  subsorts Msg1 Msg2 < Msg .
  op m1 : Client Client Server Nat Value -> Msg1 [ctor] .
  op m2 : Server Server Client Nat Value -> Msg2 [ctor] .
endfm

fmod EXCKEY is
  pr VALUE .
  sort Exckey . 
  op exk : Prin Prin Nat Value -> Exckey [ctor] .
endfm

fmod SOUP {D :: TRIV} is
  sort Soup{D} .
  subsort D$Elt < Soup{D} .
  op empty : -> Soup{D} [ctor] .
  op _ _ : Soup{D} Soup{D} -> Soup{D} [ctor assoc comm id: empty] .
  op _\in_ : D$Elt Soup{D} -> Bool .
  var S : Soup{D} .
  var E : D$Elt .
  eq E E = E . *** idempotent
  eq E \in (E S) = true .
  eq E \in S = false [owise] .
endfm

fmod SEQ {D :: TRIV} is
  sort Seq{D} .
  op nil : -> Seq{D} [ctor] .
  op _|_ : D$Elt Seq{D} -> Seq{D} [ctor] .
endfm

view Rand from TRIV to RAND is
  sort Elt to Rand .
endv

view Prin from TRIV to PRIN is
  sort Elt to Prin .
endv

view Value from TRIV to VALUE is
  sort Elt to Value .
endv

view Msg from TRIV to MSG is
  sort Elt to Msg .
endv

view Exckey from TRIV to EXCKEY is
  sort Elt to Exckey .
endv

mod DH is
  pr SOUP{Prin} .
  pr SOUP{Value} .
  pr SEQ{Rand} .
  pr SOUP{Msg} .
  pr SOUP{Exckey} .
  pr SOUP{Nat} .
  ***
  sorts OCom Sys .
  subsorts OCom < Sys .
  ***
  op none : -> Sys [ctor] .
  op __ : Sys Sys -> Sys [ctor assoc comm id: none] .
  *** Observable Components
  op sids:_ : Soup{Nat} -> OCom [ctor] .
  op sid:_ : Nat -> OCom [ctor] .
  op cs:_ : Soup{Prin} -> OCom [ctor] .
  op ss:_ : Soup{Prin} -> OCom [ctor] .
  op crl:_ : Seq{Rand} -> OCom [ctor] .
  op srl:_ : Seq{Rand} -> OCom [ctor] .
  op rm1[_,_,_]:_ : Prin Prin Nat Bool -> OCom [ctor] .
  op rm2[_,_,_]:_ : Prin Prin Nat Bool -> OCom [ctor] .
  op crs:_ : Soup{Value} -> OCom [ctor] .
  op ks:_ : Soup{Value} -> OCom [ctor] .
  op exks:_ : Soup{Exckey} -> OCom [ctor] .
  op nw:_ : Soup{Msg} -> OCom [ctor] .
  *** Maude variables
  vars SID SID1 : Nat .
  var SIDs : Soup{Nat} .
  vars C C1 C2 : Client .
  vars S S1 S2 : Server .
  var Cs : Soup{Prin} .
  var Ss : Soup{Prin} .
  vars R1 R2 R : Rand .
  var RS : Seq{Rand} .
  var CRS : Soup{Value} .
  var NW : Soup{Msg} .
  vars KC KS K1 K2 : Value .
  vars UKCs UKSs Ks : Soup{Value} .
  var EXKs : Soup{Exckey} .
  var SYS : Sys .
  *** initial state
  op init : -> Sys .
  eq init = (sid: 0) (cs: (c ic)) (ss: (s is)) (sids: (0 1))
            (crl: (r(0) | r(1) | nil)) (srl: (r(2) | r(3) | nil))
            (rm1[s,c,0]: false) (rm1[s,ic,0]: false) 
            (rm1[is,c,0]: false) (rm1[is,ic,0]: false) 
            (rm1[s,c,1]: false) (rm1[s,ic,1]: false) 
            (rm1[is,c,1]: false) (rm1[is,ic,1]: false) 
            (rm2[c,s,0]: false) (rm2[c,is,0]: false) 
            (rm2[ic,s,0]: false) (rm2[ic,is,0]: false) 
            (rm2[c,s,1]: false) (rm2[c,is,1]: false) 
            (rm2[ic,s,1]: false) (rm2[ic,is,1]: false) 
            (crs: empty) (ks: empty) (exks: empty) (nw: empty) .
  *** transitions
  crl [send1] :
  (sid: SID) (cs: (C Cs)) (ss: (S Ss)) (crl: (R1 | RS)) (nw: NW)
  =>
  (sid: (SID + 1)) (cs: (C Cs)) (ss: (S Ss)) (crl: RS) 
  (nw: (m1(C,C,S,SID,g ^ R1) NW))
  if not (C == ic and S == is) .
  ***
  rl [send2] :
  (srl: (R2 | RS)) (rm1[S,C,SID]: false) (exks: EXKs) (ks: Ks)
  (nw: (m1(C1,C,S,SID,KC) NW))
  =>
  (srl: RS) (rm1[S,C,SID]: true) (exks: (exk(S,C,SID,KC ^ R2) EXKs))
  (ks: (if S == is then (KC ^ R2 Ks) else Ks fi))
  (nw: (m2(S,S,C,SID,g ^ R2) m1(C1,C,S,SID,KC) NW)) .
  ***
  rl [rec2] :
  (rm2[C,S,SID]: false) (exks: EXKs) (ks: Ks)
  (nw: (m2(S1,S,C,SID,KS) m1(C,C,S,SID,g ^ R) NW))
  =>
  (rm2[C,S,SID]: true) (exks: (exk(C,S,SID,KS ^ R) EXKs))
  (ks: (if C == ic then (KS ^ R Ks) else Ks fi))
  (nw: (m2(S1,S,C,SID,KS) m1(C,C,S,SID,g ^ R) NW)) .
  ***
  crl [fake1] :
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m1(C1,C2,S1,SID,KC) NW))
  =>
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m1(ic,C,S,SID1,KC) m1(C1,C2,S1,SID,KC) NW))
  if not (C1 == ic) /\ not (S == is or C == ic) .
  *** transitions
  crl [fake1-2] :
  (sids: (SID1 SIDs)) (cs: (C Cs)) (ss: (S Ss))
  (crl: (R1 | RS)) (crs: CRS) (nw: NW)
  =>
  (sids: (SID1 SIDs)) (cs: (C Cs)) (ss: (S Ss))
  (crl: RS) (crs: (R1 CRS))
  (nw: (m1(ic,C,S,SID1,g ^ R1) NW))
  if not (C == ic or S == is) .
  ***
  crl [fake2] :
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m2(S1,S2,C1,SID,KS) NW))
  =>
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m2(is,S,C,SID1,KS) m2(S1,S2,C1,SID,KS) NW))
  if  not (S1 == is) /\ not (S == is or C == ic) .
  ***
  crl [fake2-2] :
  (srl: (R2 | RS)) (ks: Ks)
  (nw: (m1(C1,C,S,SID,KC) NW))
  =>
  (srl: RS) (ks: (KC ^ R2 Ks))
  (nw: (m2(is,S,C,SID,g ^ R2) m1(C1,C,S,SID,KC) NW))
  if not (C1 == ic) /\ not (C == ic or S == is) .
  ***
  crl [forge-key] :
  (ks: Ks) (crs: (R CRS))
  (nw: (m2(S1,S,C,SID,KS) NW))
  =>
  (ks: (KS ^ R Ks)) (crs: (R CRS))
  (nw: (m2(S1,S,C,SID,KS) NW))
  if  not (S1 == is) /\ not (C == ic or S == is) .
endm

eof

search [1] in DH : init =>*
(exks: (exk(C,S,SID,K1) exk(S,C,SID,K1) EXKs)) (ks: (K1 Ks)) SYS
such that (not C == ic) /\ (not S == is) .

***(
No solution.
states: 40765  rewrites: 16345066 in 11469ms cpu (11475ms real) (1425117 rewrites/second)
)

search [1] in DH : init =>*
(exks: (exk(C,S,SID,K1) exk(S,C,SID,K2) EXKs)) (ks: (K1 K2 Ks)) SYS
such that (not K1 == K2) /\ (not C == ic) /\ (not S == is) .

***(
Solution 1 (state 3714)
states: 3715  rewrites: 338557 in 190ms cpu (190ms real) (1775263 rewrites/second)
SYS --> sids: (0 1) sid: 1 cs: (c ic) ss: (s is) crl: nil srl: nil crs: r(1) nw: (m1(c, c, s, 0, g ^ r(0)) m1(ic, c, s, 0, g ^ r(1)) m2(s, s, c, 0, g ^ r(2))
    m2(is, s, c, 0, g ^ r(3))) (rm1[s,c,0]: true) (rm1[s,c,1]: false) (rm1[s,ic,0]: false) (rm1[s,ic,1]: false) (rm1[is,c,0]: false) (rm1[is,c,1]: false) (rm1[
    is,ic,0]: false) (rm1[is,ic,1]: false) (rm2[c,s,0]: true) (rm2[c,s,1]: false) (rm2[c,is,0]: false) (rm2[c,is,1]: false) (rm2[ic,s,0]: false) (rm2[ic,s,1]:
    false) (rm2[ic,is,0]: false) rm2[ic,is,1]: false
Ks --> (empty).Soup{Value}
K1 --> g ^ (r(0) * r(3))
K2 --> g ^ (r(1) * r(2))
EXKs --> (empty).Soup{Exckey}
C --> c
S --> s
SID --> 0
Maude> 
> show path 3714 .
show path 3714 .
state 0, Sys: sids: (0 1) sid: 0 cs: (c ic) ss: (s is) crl: (r(0) | r(1) | nil) srl: (r(2) | r(3) | nil) crs: empty ks: empty exks: empty nw: empty (rm1[s,c,
    0]: false) (rm1[s,c,1]: false) (rm1[s,ic,0]: false) (rm1[s,ic,1]: false) (rm1[is,c,0]: false) (rm1[is,c,1]: false) (rm1[is,ic,0]: false) (rm1[is,ic,1]:
    false) (rm2[c,s,0]: false) (rm2[c,s,1]: false) (rm2[c,is,0]: false) (rm2[c,is,1]: false) (rm2[ic,s,0]: false) (rm2[ic,s,1]: false) (rm2[ic,is,0]: false)
    rm2[ic,is,1]: false
===[ crl sid: SID cs: (C Cs) ss: (S Ss) crl: (R1 | RS) nw: NW => sid: (SID + 1) cs: (C Cs) ss: (S Ss) crl: RS nw: (NW m1(C, C, S, SID, g ^ R1)) if not (C == ic
    and S == is) = true [label send1] . ]===>
state 1, Sys: sids: (0 1) sid: 1 cs: (c ic) ss: (s is) crl: (r(1) | nil) srl: (r(2) | r(3) | nil) crs: empty ks: empty exks: empty nw: m1(c, c, s, 0, g ^ r(0))
    (rm1[s,c,0]: false) (rm1[s,c,1]: false) (rm1[s,ic,0]: false) (rm1[s,ic,1]: false) (rm1[is,c,0]: false) (rm1[is,c,1]: false) (rm1[is,ic,0]: false) (rm1[is,
    ic,1]: false) (rm2[c,s,0]: false) (rm2[c,s,1]: false) (rm2[c,is,0]: false) (rm2[c,is,1]: false) (rm2[ic,s,0]: false) (rm2[ic,s,1]: false) (rm2[ic,is,0]:
    false) rm2[ic,is,1]: false
===[ crl sids: (SID1 SIDs) cs: (C Cs) ss: (S Ss) crl: (R1 | RS) crs: CRS nw: NW => sids: (SID1 SIDs) cs: (C Cs) ss: (S Ss) crl: RS crs: (R1 CRS) nw: (NW m1(ic,
    C, S, SID1, g ^ R1)) if not (C == ic or S == is) = true [label fake1-2] . ]===>
state 12, Sys: sids: (0 1) sid: 1 cs: (c ic) ss: (s is) crl: nil srl: (r(2) | r(3) | nil) crs: r(1) ks: empty exks: empty nw: (m1(c, c, s, 0, g ^ r(0)) m1(ic,
    c, s, 0, g ^ r(1))) (rm1[s,c,0]: false) (rm1[s,c,1]: false) (rm1[s,ic,0]: false) (rm1[s,ic,1]: false) (rm1[is,c,0]: false) (rm1[is,c,1]: false) (rm1[is,ic,
    0]: false) (rm1[is,ic,1]: false) (rm2[c,s,0]: false) (rm2[c,s,1]: false) (rm2[c,is,0]: false) (rm2[c,is,1]: false) (rm2[ic,s,0]: false) (rm2[ic,s,1]:
    false) (rm2[ic,is,0]: false) rm2[ic,is,1]: false
===[ rl srl: (R2 | RS) ks: Ks exks: EXKs nw: (NW m1(C1, C, S, SID, KC)) rm1[S,C,SID]: false => srl: RS (exks: (EXKs exk(S, C, SID, KC ^ R2)) ks: if S == is
    then Ks KC ^ R2 else Ks fi nw: ((NW m1(C1, C, S, SID, KC)) m2(S, S, C, SID, g ^ R2))) rm1[S,C,SID]: true [label send2] . ]===>
state 77, Sys: sids: (0 1) sid: 1 cs: (c ic) ss: (s is) crl: nil srl: (r(3) | nil) crs: r(1) ks: empty exks: exk(s, c, 0, g ^ (r(1) * r(2))) nw: (m1(c, c, s,
    0, g ^ r(0)) m1(ic, c, s, 0, g ^ r(1)) m2(s, s, c, 0, g ^ r(2))) (rm1[s,c,0]: true) (rm1[s,c,1]: false) (rm1[s,ic,0]: false) (rm1[s,ic,1]: false) (rm1[is,
    c,0]: false) (rm1[is,c,1]: false) (rm1[is,ic,0]: false) (rm1[is,ic,1]: false) (rm2[c,s,0]: false) (rm2[c,s,1]: false) (rm2[c,is,0]: false) (rm2[c,is,1]:
    false) (rm2[ic,s,0]: false) (rm2[ic,s,1]: false) (rm2[ic,is,0]: false) rm2[ic,is,1]: false
===[ crl srl: (R2 | RS) ks: Ks nw: (NW m1(C1, C, S, SID, KC)) => srl: RS ks: (Ks KC ^ R2) nw: ((NW m1(C1, C, S, SID, KC)) m2(is, S, C, SID, g ^ R2)) if not C1
    == ic = true /\ not (C == ic or S == is) = true [label fake2-2] . ]===>
state 330, Sys: sids: (0 1) sid: 1 cs: (c ic) ss: (s is) crl: nil srl: nil crs: r(1) ks: g ^ (r(0) * r(3)) exks: exk(s, c, 0, g ^ (r(1) * r(2))) nw: (m1(c, c,
    s, 0, g ^ r(0)) m1(ic, c, s, 0, g ^ r(1)) m2(s, s, c, 0, g ^ r(2)) m2(is, s, c, 0, g ^ r(3))) (rm1[s,c,0]: true) (rm1[s,c,1]: false) (rm1[s,ic,0]: false) (
    rm1[s,ic,1]: false) (rm1[is,c,0]: false) (rm1[is,c,1]: false) (rm1[is,ic,0]: false) (rm1[is,ic,1]: false) (rm2[c,s,0]: false) (rm2[c,s,1]: false) (rm2[c,
    is,0]: false) (rm2[c,is,1]: false) (rm2[ic,s,0]: false) (rm2[ic,s,1]: false) (rm2[ic,is,0]: false) rm2[ic,is,1]: false
===[ rl ks: Ks exks: EXKs nw: (NW m1(C, C, S, SID, g ^ R) m2(S1, S, C, SID, KS)) rm2[C,S,SID]: false => (exks: (EXKs exk(C, S, SID, KS ^ R)) ks: if C == ic
    then Ks KS ^ R else Ks fi nw: ((NW m1(C, C, S, SID, g ^ R)) m2(S1, S, C, SID, KS))) rm2[C,S,SID]: true [label rec2] . ]===>
state 1236, Sys: sids: (0 1) sid: 1 cs: (c ic) ss: (s is) crl: nil srl: nil crs: r(1) ks: g ^ (r(0) * r(3)) exks: (exk(c, s, 0, g ^ (r(0) * r(3))) exk(s, c, 0,
    g ^ (r(1) * r(2)))) nw: (m1(c, c, s, 0, g ^ r(0)) m1(ic, c, s, 0, g ^ r(1)) m2(s, s, c, 0, g ^ r(2)) m2(is, s, c, 0, g ^ r(3))) (rm1[s,c,0]: true) (rm1[s,
    c,1]: false) (rm1[s,ic,0]: false) (rm1[s,ic,1]: false) (rm1[is,c,0]: false) (rm1[is,c,1]: false) (rm1[is,ic,0]: false) (rm1[is,ic,1]: false) (rm2[c,s,0]:
    true) (rm2[c,s,1]: false) (rm2[c,is,0]: false) (rm2[c,is,1]: false) (rm2[ic,s,0]: false) (rm2[ic,s,1]: false) (rm2[ic,is,0]: false) rm2[ic,is,1]: false
===[ crl crs: (R CRS) ks: Ks nw: (NW m2(S1, S, C, SID, KS)) => ks: (Ks KS ^ R) crs: (R CRS) nw: (NW m2(S1, S, C, SID, KS)) if not S1 == is = true /\ not (C ==
    ic or S == is) = true [label forge-key] . ]===>
state 3714, Sys: sids: (0 1) sid: 1 cs: (c ic) ss: (s is) crl: nil srl: nil crs: r(1) ks: (g ^ (r(0) * r(3)) g ^ (r(1) * r(2))) exks: (exk(c, s, 0, g ^ (r(0) *
    r(3))) exk(s, c, 0, g ^ (r(1) * r(2)))) nw: (m1(c, c, s, 0, g ^ r(0)) m1(ic, c, s, 0, g ^ r(1)) m2(s, s, c, 0, g ^ r(2)) m2(is, s, c, 0, g ^ r(3))) (rm1[s,
    c,0]: true) (rm1[s,c,1]: false) (rm1[s,ic,0]: false) (rm1[s,ic,1]: false) (rm1[is,c,0]: false) (rm1[is,c,1]: false) (rm1[is,ic,0]: false) (rm1[is,ic,1]:
    false) (rm2[c,s,0]: true) (rm2[c,s,1]: false) (rm2[c,is,0]: false) (rm2[c,is,1]: false) (rm2[ic,s,0]: false) (rm2[ic,s,1]: false) (rm2[ic,is,0]: false)
    rm2[ic,is,1]: false
)