Title of article :
Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic Hoare style logic
Author/Authors :
Jerry den Hartog، نويسنده ,
Issue Information :
دوهفته نامه با شماره پیاپی سال 2008
Pages :
12
From page :
52
To page :
63
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.
Keywords :
Axiomatization , Provable correctness , Probability , cryptography , Hoare logic
Journal title :
Science of Computer Programming
Serial Year :
2008
Journal title :
Science of Computer Programming
Record number :
1080048
Link To Document :
بازگشت