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
SN - 0167-6423
VL - 74
SP - 52
EP - 63
JO - Science of Computer Programming
JF - Science of Computer Programming
IS - 1-2
ER -