Analyzing CAS protocol using weakest precondition semantics for the applied -calculus
Decai Jiao, David A. Sinclair · China-Ireland International Conference on Information and Communications Technologies (CIICT 2007) · 2007
In this paper, we formalize CAS protocol using the applied π-calculus with the weakest precondition semantics. Safety property can be specified as that the weakest precondition with respect to a given "bad" postcondition is false and the liveness property can be specified as that the weakest preconditions are satisfiable by the system with respect to the expected postcondition. We specify a safety and a liveness property of CAS and verify them in the proof system WP4PI, which is an automatic proof tool based on the weakest precondition semantics of the applied π-calculus.