Computational Soundness Results for Stateful Applied pi Calculus

TL;DR

This paper establishes the computational soundness of the stateful applied pi-calculus used in SAPIC and StatVerif tools, enabling more secure automated analysis of stateful cryptographic protocols.

Contribution

It provides the first computational soundness proofs for the stateful applied pi-calculus in SAPIC and StatVerif, based on the CoSP framework, including embeddings and modular proofs.

Findings

Proves computational soundness for SAPIC and StatVerif

Embeds protocol states into CoSP protocols efficiently

Extends proofs to cryptographic primitives like encryption and signatures

Abstract

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).