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.
(
geocities.com/de/christian_jacobi) (
geocities.com/de)