Deriving cryptographically sound implementations using composition and formally verified bisimulation

Abstract

We consider abstract specifications of cryptographic protocols which are both suitable for formal verification and maintain a sound cryptographic semantics. In this paper, we present the first abstract specification for ordered secure message transmission in reactive systems based on the recently published model of Pfitzmann and Waidner. We use their composition theorem to derive a possible implementation whose correctness additionally involves a classical bisimulation, which we formally verify using the theorem prover PVS. The example serves as the first important case study which shows that this approach is applicable in practice, and it is the first example that combines tool-supported formal proof techniques with the rigorous proofs of cryptography.