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

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)

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.
LanguageEnglish
Pages52-63
JournalScience of Computer Programming
Volume74
Issue number1-2
DOIs
StatePublished - 2008

Fingerprint

Computer science
Formal verification

Cite this

@article{9784ea679e754785b3c930f722d6c995,
title = "Towards mechanized correctness proofs for cryptographic algorithms : Axiomatization of a probabilistic Hoare style logic",
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.",
author = "{Hartog, den}, J.I.",
year = "2008",
doi = "10.1016/j.scico.2008.09.006",
language = "English",
volume = "74",
pages = "52--63",
journal = "Science of Computer Programming",
issn = "0167-6423",
publisher = "Elsevier",
number = "1-2",

}

Towards mechanized correctness proofs for cryptographic algorithms : Axiomatization of a probabilistic Hoare style logic. / Hartog, den, J.I.

In: Science of Computer Programming, Vol. 74, No. 1-2, 2008, p. 52-63.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

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

AU - Hartog, den,J.I.

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

U2 - 10.1016/j.scico.2008.09.006

DO - 10.1016/j.scico.2008.09.006

M3 - Article

VL - 74

SP - 52

EP - 63

JO - Science of Computer Programming

T2 - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

IS - 1-2

ER -