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.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Boiten08,
author = {Eerke A. Boiten},
editor = {Egon B{\"{o}}rger and
Michael J. Butler and
Jonathan P. Bowen and
Paul Boca},
title = {From {ABZ} to Cryptography},
booktitle = {Abstract State Machines, {B} and Z, First International Conference,
{ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5238},
pages = {353},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87603-8\_40},
doi = {10.1007/978-3-540-87603-8\_40},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/Boiten08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}