***
*** C --- C, K_{c1} ---> S
*** where K_{c1} = g^{r_c}
*** C <--- K_{s1}    --- S
*** where t_1 = H1(K_{c1})
***       K_{s1} = (g^pw * K_{c1}^{t_1})^{r_s}
*** C --- VK_c      ---> S
*** where t_2 = H2(K_{c1},K_{s1})
***       z = K_{s1}^{(r_c + t_2)/(r_c * t_1 + pw)}
***       VK_c = H4(K_{c1},K_{s1},z)
***       z' = (K_{c1} * g^{t_2})^{r_s}
***       VK_c' = H4(K_{c1},K_{s1},z')
***       assert(VK_c = VK_c')
*** C <--- VK_s      --- S
*** where VK_s = H3(K_{c1},K_{s1},z')
***       VK_s' = H3(K_{c1},K_{s1},z)
***       assert(VK_s = VK_s')
***

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 PWD is
  pr PRIN .
  sort Pwd .
  op dpwd : -> Pwd [ctor] .
  op pwd : Client Server -> Pwd [ctor] .
  op h : Pwd -> Pwd .
endfm

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

fmod VALUE is
  pr RAND .
  pr PWD .
  pr BASE .
  pr PWD .
  sorts Value H3Value H4Value .
  subsorts Rand Pwd Base < Value .
  op _^_ : Value Value -> Value [prec 10] .
  op _*_ : Value Value -> Value [assoc comm prec 20] .
  op _/_ : Value Value -> Value [prec 20] .
  op _+_ : Value Value -> Value [assoc comm prec 30] .
  op h1 : Value -> Value .
  op h2 : Value Value -> Value .
  op h3 : Value Value Value -> H3Value .
  op h4 : Value Value Value -> H4Value .
  vars X Y Z : Value .
  eq (X ^ Y) * (X ^ Z) = X ^ (Y + Z) .
  eq (X ^ Y) ^ Z = X ^ (Y * Z) .
  eq X * (Y / Z) = (X * Y) / Z .
  eq (X * Y) / Y = X .
endfm

fmod MSG is
  pr VALUE .
  sorts Msg Msg1 Msg2 Msg3 Msg4 .
  subsorts Msg1 Msg2 Msg3 Msg4 < Msg .
  op m1 : Client Client Server Nat Client Value -> Msg1 [ctor] .
  op m2 : Server Server Client Nat Value -> Msg2 [ctor] .
  op m3 : Client Client Server Nat H4Value -> Msg3 [ctor] .
  op m4 : Server Server Client Nat H3Value -> Msg4 [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 H3Value from TRIV to VALUE is
  sort Elt to H3Value .
endv

view H4Value from TRIV to VALUE is
  sort Elt to H4Value .
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

view Pwd from TRIV to PWD is
  sort Elt to Pwd .
endv

fmod PWD-SEQ is
  pr SEQ{Pwd} .
  op nth : Seq{Pwd} Nat -> Pwd .
  var X : Nat .
  var PW : Pwd .
  var PWs : Seq{Pwd} .
  eq nth(nil,X) = dpwd .
  eq nth(PW | PWs,0) = PW .
  eq nth(PW | PWs,s(X)) = nth(PWs,X) .
endfm

mod MAP4HTTP is
  pr SOUP{Prin} .
  *** pr SOUP{Rand} .
  pr SOUP{Value} .
  pr SOUP{H3Value} .
  pr SOUP{H4Value} .
  pr SEQ{Rand} .
  pr PWD-SEQ .
  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 kcs:_ : Soup{Value} -> OCom [ctor] .
  op kss:_ : Soup{Value} -> OCom [ctor] .
  op vkcs:_ : Soup{H4Value} -> OCom [ctor] .
  op vkss:_ : Soup{H3Value} -> OCom [ctor] .
  op rm1[_,_,_]:_ : Prin Prin Nat Bool -> OCom [ctor] .
  op rm2[_,_,_]:_ : Prin Prin Nat Bool -> OCom [ctor] .
  op rm3[_,_,_]:_ : Prin Prin Nat Bool -> OCom [ctor] .
  op rm4[_,_,_]:_ : Prin Prin Nat Bool -> OCom [ctor] .
  op done[_,_,_]:_ : Prin Prin Nat Bool -> OCom [ctor] .
  op sr[_,_]:_ : Prin Nat Rand -> OCom [ctor] .
  op crs:_ : Soup{Value} -> OCom [ctor] .
  op srs:_ : Soup{Value} -> OCom [ctor] .
  op ks:_ : Soup{Value} -> OCom [ctor] .
  op pws:_ : Soup{Value} -> OCom [ctor] .
  op exks:_ : Soup{Exckey} -> OCom [ctor] .
  op pwl[_,_]:_ : Prin Prin Seq{Pwd} -> OCom [ctor] .
  op nw:_ : Soup{Msg} -> OCom [ctor] .
  *** Maude variables
  vars SID SID1 : Nat .
  vars C C1 C2 C3 : Client .
  var Cs : Soup{Prin} .
  vars S S1 S2 : Server .
  var Ss : Soup{Prin} .
  vars R1 R2 R : Rand .
  vars T1 T2 KC1 KS1 Z KC KS K K1 K2 : Value .
  vars KCs KSs UKCs UKSs Ks Rs PWs : Soup{Value} .
  var PW : Pwd .
  var VKC : H4Value .
  var VKCs : Soup{H4Value} .
  var VKS : H3Value .
  var VKSs : Soup{H3Value} .
  var RS : Seq{Rand} .
  var EXK : Exckey .
  var EXKs : Soup{Exckey} .
  var NW : Soup{Msg} .
  var SYS : Sys .
  var SIDs : Soup{Nat} .
  var PWL : Seq{Pwd} .
  *** 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))
            (pwl[c,s]: (h(h(pwd(c,s))) | h(pwd(c,s)) | nil))
            (pwl[ic,s]: (h(h(pwd(ic,s))) | h(pwd(ic,s)) | nil))
            (pwl[c,is]: (h(h(pwd(c,is))) | h(pwd(c,is)) | nil))
            (pwl[ic,is]: (h(h(pwd(ic,is))) | h(pwd(ic,is)) | nil))
            (kcs: empty) (kss: empty) (vkcs: empty) (vkss: empty)
            (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) 
            (rm3[s,c,0]: false) (rm3[s,ic,0]: false) 
            (rm3[is,c,0]: false) (rm3[is,ic,0]: false) 
            (rm3[s,c,1]: false) (rm3[s,ic,1]: false) 
            (rm3[is,c,1]: false) (rm3[is,ic,1]: false) 
            (rm4[c,s,0]: false) (rm4[c,is,0]: false) 
            (rm4[ic,s,0]: false) (rm4[ic,is,0]: false) 
            (rm4[c,s,1]: false) (rm4[c,is,1]: false) 
            (rm4[ic,s,1]: false) (rm4[ic,is,1]: false) 
            (done[c,s,0]: false) (done[c,is,0]: false) 
            (done[ic,s,0]: false) (done[ic,is,0]: false) 
            (done[c,s,1]: false) (done[c,is,1]: false) 
            (done[ic,s,1]: false) (done[ic,is,1]: false) 
            (sr[s,0]: dr) (sr[s,1]: dr) (sr[s,2]: dr) (sr[s,3]: dr) 
            (sr[is,0]: dr) (sr[is,1]: dr) (sr[is,2]: dr) (sr[is,3]: dr) 
            (crs: empty) (srs: empty) (pws: empty) (ks: empty)
            (exks: empty) (nw: empty) .
  *** transitions
  crl [send1] :
  (sid: SID) (cs: (C Cs)) (ss: (S Ss)) (crl: (R1 | RS)) (kcs: KCs) (nw: NW)
  (crs: Rs)
  =>
  (sid: (SID + 1)) (cs: (C Cs)) (ss: (S Ss)) (crl: RS) (kcs: (g ^ R1 KCs))
  (nw: (m1(C,C,S,SID,C,g ^ R1) NW))
  (crs: (if not (C == ic or S == is) then (R1 Rs) else Rs fi))
  if not (C == ic and S == is) .
  ***
  crl [send2] :
  (srl: (R2 | RS)) (sr[S,SID]: R) (kss: KSs) (rm1[S,C,SID]: false)
  (nw: (m1(C1,C,S,SID,C,KC1) NW))
  (srs: Rs) (pwl[C,S]: PWL)
  =>
  (srl: RS) (sr[S,SID]: R2)
  (kss: ((g ^ nth(PWL,SID) * KC1 ^ h1(KC1)) ^ R2 KSs))
  (rm1[S,C,SID]: true)
  (nw: (m2(S,S,C,SID,(g ^ nth(PWL,SID) * KC1 ^ h1(KC1)) ^ R2)
        m1(C1,C,S,SID,C,KC1) NW))
  (srs: (if not (C == ic or S == is) then (R2 Rs) else Rs fi))
  (srs: Rs) (pwl[C,S]: PWL)
  if not nth(PWL,SID) == dpwd .
  ***
  crl [send3] :
  (vkcs: VKCs) (rm2[C,S,SID]: false)
  (nw: (m2(S1,S,C,SID,KS1) m1(C,C,S,SID,C,g ^ R1) NW))
  (pwl[C,S]: PWL)
  =>
  (vkcs: (h4(g ^ R1,KS1,
             (KS1 ^ ((R1 + h2(g ^ R1,KS1)) / (R1 * h1(g ^ R1) + nth(PWL,SID)))) ^ nth(PWL,SID))
          VKCs))
  (rm2[C,S,SID]: true)
  (nw: (m3(C,C,S,SID,
          h4(g ^ R1,KS1,
             (KS1 ^ ((R1 + h2(g ^ R1,KS1)) / (R1 * h1(g ^ R1) + nth(PWL,SID)))) ^ nth(PWL,SID)) )
        m2(S1,S,C,SID,KS1) m1(C,C,S,SID,C,g ^ R1) NW))
  (pwl[C,S]: PWL)
  if not nth(PWL,SID) == dpwd .
  ***
  crl [send4] :
  (sr[S,SID]: R) (vkss: VKSs) (rm3[S,C,SID]: false) (exks: EXKs)
  (nw: (m3(C2,C,S,SID,VKC) m2(S,S,C,SID,KS1) m1(C1,C,S,SID,C,KC1) NW))
  (pwl[C,S]: PWL)
  =>
  (sr[S,SID]: R) (vkss: (h3(KC1,KS1,(KC1 * g ^ h2(KC1,KS1)) ^ R) VKSs))
  (rm3[S,C,SID]: true)
  (exks: (exk(S,C,SID,((KC1 * g ^ h2(KC1,KS1)) ^ R) ^ nth(PWL,SID)) EXKs))
  (nw: (m4(S,S,C,SID,h3(KC1,KS1,((KC1 * g ^ h2(KC1,KS1)) ^ R) ^ nth(PWL,SID)))
        m3(C2,C,S,SID,VKC) m2(S,S,C,SID,KS1) m1(C1,C,S,SID,C,KC1) NW))
  (pwl[C,S]: PWL)
  if VKC = h4(KC1,KS1,((KC1 * g ^ h2(KC1,KS1)) ^ R) ^ nth(PWL,SID)) /\
     not nth(PWL,SID) == dpwd .
  ***
  crl [rec4] :
  (rm4[C,S,SID]: false) (exks: EXKs)
  (nw: (m4(S2,S,C,SID,VKS) m3(C,C,S,SID,VKC)
        m2(S1,S,C,SID,KS1) m1(C,C,S,SID,C,g ^ R1) NW))
  (pwl[C,S]: PWL)
  =>
  (rm4[C,S,SID]: true)
  (exks: (exk(C,S,SID,(KS1 ^ ((R1 + h2(g ^ R1,KS1)) / (R1 * h1(g ^ R1) + nth(PWL,SID)))) ^ nth(PWL,SID))
          EXKs))
  (nw: (m4(S2,S,C,SID,VKS) m3(C,C,S,SID,VKC)
        m2(S1,S,C,SID,KS1) m1(C,C,S,SID,C,g ^ R1) NW))
  (pwl[C,S]: PWL)
  if VKS = h3(g ^ R1,KS1,
              (KS1 ^ ((R1 + h2(g ^ R1,KS1)) / (R1 * h1(g ^ R1) + nth(PWL,SID)))) ^ nth(PWL,SID)) /\
     not nth(PWL,SID) == dpwd .
  ***
  crl [done] :
  (rm4[C,S,SID]: true) (done[C,S,SID]: false)
  (pwl[C,S]: PWL) (pws: PWs)
  =>
  (rm4[C,S,SID]: true) (done[C,S,SID]: true)
  (pwl[C,S]: PWL) (pws: (nth(PWL,SID) PWs))
  if not nth(PWL,SID) == dpwd .
  ***
  crl [fake1] :
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m1(C1,C2,S1,SID,C3,KC1) NW))
  =>
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m1(ic,C,S,SID1,C,KC1) m1(C1,C2,S1,SID,C3,KC1) NW))
  if not (C1 == ic) /\ not (C == ic or S == is) .
  ***
  crl [fake1-2] :
  (sid: SID) (cs: (C Cs)) (ss: (S Ss)) (crl: (R1 | RS)) 
  (sids: (SID1 SIDs)) (nw: NW)
  =>
  (sid: SID) (cs: (C Cs)) (ss: (S Ss)) (crl: RS) 
  (sids: (SID1 SIDs)) (nw: (m1(ic,C,S,SID1,C,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,KS1) NW))
  =>
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m2(is,S,C,SID1,KS1) m2(S1,S2,C1,SID,KS1) NW))
  if not (S1 == is) /\ not (C == ic or S == is) .
  ***
  crl [fake2-1] :
  (srl: (R2 | RS)) (pws: (PW PWs)) (ks: Ks)
  (nw: (m1(C1,C,S,SID,C,KC1) NW))
  =>
  (srl: RS) (pws: (PW PWs))
  (ks: ((((KC1 * g ^ h2(KC1,(g ^ PW * KC1 ^ h1(KC1)) ^ R2)) ^ R2) ^ PW) Ks))
  (nw: (m2(is,S,C,SID,((g ^ PW * KC1 ^ h1(KC1)) ^ R2) ^ PW)
        m1(C1,C,S,SID,C,KC1) NW))
  if not (C == ic or S == is) .
  ***
  crl [fake3] :
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m3(C1,C2,S1,SID,VKC) NW))
  =>
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m3(ic,C,S,SID1,VKC) m3(C1,C2,S1,SID,VKC) NW))
  if not (C1 == ic) /\ not (C == ic or S == is) .
  ***
  crl [fake3-2] :
  (ks: (K Ks))
  (nw: (m2(S1,S,C,SID,KS1) m1(C1,C,S,SID,C,KC1) NW))
  =>
  (ks: (K Ks))
  (nw: (m3(ic,C,S,SID,h4(KC1,KS1,K))
        m2(S1,S,C,SID,KS1) m1(C1,C,S,SID,C,KC1) NW))
  if not (S == is or C == ic) .
  ***
  crl [fake4] :
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m4(S1,S2,C1,SID,VKS) NW))
  =>
  (cs: (C Cs)) (ss: (S Ss)) (sids: (SID1 SIDs))
  (nw: (m4(is,S,C,SID1,VKS) m4(S1,S2,C1,SID,VKS) NW))
  if not (S1 == is) /\ not (C == ic or S == is) .
  ***
  crl [fake4-2] :
  (ks: (K Ks))
  (nw: (m3(C2,C,S,SID,VKC) m2(S1,S,C,SID,KS1)
        m1(C1,C,S,SID,C,KC1) NW))
  =>
  (ks: (K Ks))
  (nw: (m4(is,S,C,SID,h3(KC1,KS1,K)) m3(C2,C,S,SID,VKC) 
        m2(S1,S,C,SID,KS1) m1(C1,C,S,SID,C,KC1) NW))
  if not (S == is or C == ic) /\ VKC = h4(KC1,KS1,K) .
  ***
  rl [forge-key1] :
  (kcs: (KC KCs)) (kss: (KS KSs)) (crs: (R Rs)) (pws: (PW PWs))
  (ks: Ks)
  =>
  (kcs: (KC KCs)) (kss: (KS KSs)) (crs: (R Rs)) (pws: (PW PWs))
  (ks: (((KS ^ ((R + h2(KC,KS)) / (R * h1(KC) + PW))) ^ PW) Ks)) .
  ***
  rl [forge-key2] :
  (kcs: (KC KCs)) (kss: (KS KSs)) (srs: (R Rs)) (pws: (PW PWs)) (ks: Ks)
  =>
  (kcs: (KC KCs)) (kss: (KS KSs)) (srs: (R Rs)) (pws: (PW PWs))
  (ks: ((((KC * g ^ h2(KC,KS)) ^ R) ^ PW) Ks)) .
endm

eof

search [,10] in MAP4HTTP : init =>* SYS .
search [,9] in MAP4HTTP : init =>* SYS such that false .
quit
eof

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

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

search [1] in MAP4HTTP : init
=>* (nw: (m1(C,C,S,SID,C,KC1) m2(S1,S,C,SID,KS1)
          m3(C,C,S,SID,h4(KC1,KS1,K)) m4(S2,S,C,SID,h3(KC1,KS1,K)) NW))
     SYS
such that
not (m2(S,S,C,SID,KS1) \in (m2(S1,S,C,SID,KS1) NW) and
     m4(S,S,C,SID,h3(KC1,KS1,K)) \in (m4(S2,S,C,SID,h3(KC1,KS1,K)) NW)) .

search [1] in MAP4HTTP : init
=>* (nw: (m1(C1,C,S,SID,C,KC1) m2(S,S,C,SID,KS1)
          m3(C2,C,S,SID,h4(KC1,KS1,K)) m4(S,S,C,SID,h3(KC1,KS1,K)) NW))
     SYS
such that
not (m1(C,C,S,SID,C,KC1) \in (m1(C1,C,S,SID,C,KC1) NW) and
     m3(C,C,S,SID,h4(KC1,KS1,K)) \in (m3(C2,C,S,SID,h4(KC1,KS1,K)) NW)) .