Cryptographically Sound and Machine-Assisted Verification of Security Protocols

We consider machine-aided verification of suitably constructed abstractions of security protocols, such that the verified properties are valid for the concrete implementation of the protocol with respect to cryptographic definitions. In order to link formal methods and cryptography, we show that integrity properties are preserved under step-wise refinement in asynchronous networks with respect to cryptographic definitions, so formal verifications of our abstractions carry over to the concrete counterparts. As an example, we use the theorem prover PVS to formally verify a system for ordered secure message transmission, which yields the first example ever of a formally verified but nevertheless cryptographically sound proof of a security protocol. We believe that a general methodology for verifying cryptographic protocols cryptographically sound can be derived by following the ideas of this example.