### Abstract

Language | English |
---|---|

Pages | 52-63 |

Journal | Science of Computer Programming |

Volume | 74 |

Issue number | 1-2 |

DOIs | |

State | Published - 2008 |

### Fingerprint

### Cite this

}

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

Research output: Contribution to journal › Article › Academic › peer-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 -