Back to Search
Start Over
Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic Hoare style logic
- Source :
-
Science of Computer Programming . Dec2008, Vol. 74 Issue 1/2, p52-63. 12p. - Publication Year :
- 2008
-
Abstract
- 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. [Copyright &y& Elsevier]
- Subjects :
- *VIDEO games
*ALGORITHMS
*CRYPTOGRAPHY
*COMPUTER science
Subjects
Details
- Language :
- English
- ISSN :
- 01676423
- Volume :
- 74
- Issue :
- 1/2
- Database :
- Academic Search Index
- Journal :
- Science of Computer Programming
- Publication Type :
- Academic Journal
- Accession number :
- 35501971
- Full Text :
- https://doi.org/10.1016/j.scico.2008.09.006