From ABZ to Cryptography

Abstract

Three Steps from the Ideal

Ideally correctness is by construction; post-hoc verification is second choice; verification of proofs is the next step down. In the application area of modern cryptographic protocol verification, the latter would be viewed as serious progress.

Modern Cryptographic Protocols and Security

A modern cryptographic protocol may have the following properties:

• its functionality is clear, but its security definition incomplete;

• it contains explicit probabilistic elements;

• its notion of security (correctness) is approximate, and relative to computational resources available for an attack against it;

• its security is proved relative to some problem being hard;

• primitives cannot be implemented compositionally.

All this means that the standard techniques and good intentions of formal methods do not work straight out of the box. Many approaches to bridging the gap between formal methods and modern cryptography exist – but none of these are too close in spirit to the ABZ world.