  In recent years, many researches have been done to establish symbolic models
of stateful protocols. Two works among them, the SAPIC tool and StatVerif tool,
provide a high-level specification language and an automated analysis. Their
language, the stateful applied \pi-calculus, is extended from the applied
\pi-calculus by defining explicit state constructs. Symbolic abstractions of
cryptography used in it make the analysis amenable to automation. However, this
might overlook the attacks based on the algebraic properties of the
cryptographic algorithms. In our paper, we establish the computational
soundness results for stateful applied \pi-calculus used in SAPIC tool and
StatVerif tool.
  In our approach, we build our results on the CoSP framework. For SAPIC, we
embed the non-monotonic protocol states into the CoSP protocols, and prove that
the resulting CoSP protocols are efficient. Through the embedding, we provide
the computational soundness result for SAPIC (by Theorem 1). For StatVerif, we
encode the StatVerif process into a subset of SAPIC process, and obtain the
computational soundness result for StatVerif (by Theorem 2). Our encoding shows
the differences between the semantics of the two languages. Our work inherits
the modularity of CoSP, which allows for easily extending the proofs to
specific cryptographic primitives. Thus we establish a computationally sound
automated verification result for the input languages of SAPIC and StatVerif
that use public-key encryption and signatures (by Theorem 3).
