Towards mechanized correctness proofs for cryptographic algorithms : Axiomatization of a probabilistic Hoare style logic

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
1 Downloads (Pure)

Abstract

In [R.J. Corin, J.I. den Hartog, A probabilistic hoare-style logic for game-based cryptographic proofs, in: M. Bugliesi, B. Preneel, V. Sassone (Eds.), ICALP 2006 Track C, Venice, Italy, in: Lecture Notes in Computer Science, vol. 4052, Springer-Verlag, Berlin, 2006, pp. 252–263] we build a formal verification technique for game-based correctness proofs of cryptographic algorithms based on a probabilistic Hoare style logic [J.I. den Hartog, E.P. de Vink, Verifying probabilistic programs using a Hoare like logic, International Journal of Foundations of Computer Science 13 (3) (2002) 315–340]. An important step towards enabling mechanized verification within this technique is an axiomatization of implication between predicates which is purely semantically defined in the latter reference cited above. In this paper we provide an axiomatization and illustrate its place in the formal verification technique given in the former.
Original languageEnglish
Pages (from-to)52-63
JournalScience of Computer Programming
Volume74
Issue number1-2
DOIs
Publication statusPublished - 2008

Fingerprint

Dive into the research topics of 'Towards mechanized correctness proofs for cryptographic algorithms : Axiomatization of a probabilistic Hoare style logic'. Together they form a unique fingerprint.

Cite this