Computational Soundness Results for Stateful Applied pi Calculus
This work addresses a foundational gap in automated verification of stateful cryptographic protocols for security researchers and tool developers, though it is incremental as it builds on existing frameworks like CoSP.
The paper tackles the problem of ensuring computational soundness for stateful applied pi calculus used in automated verification tools like SAPIC and StatVerif, which previously relied on symbolic abstractions that might overlook attacks based on algebraic properties of cryptography. It establishes computational soundness results by embedding these languages into the CoSP framework, providing proofs for SAPIC and StatVerif, and extending to specific cryptographic primitives like public-key encryption and signatures.
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 π-calculus, is extended from the applied π-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 π-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).