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

In [5] we build a formal verification technique for game based correctness proofs of cryptograhic algorithms based on a probabilistic Hoare style logic [10]. An important step towards enabling mechanized verification within this technique is an axiomatization of implication between predicates which is purely semantically defined in [10]. In this paper we provide an axiomatization and illustrate its place in the formal verification technique of [5].

• Type: Journal
• Year: 2008
• Where: SCP
• Authors: Jerry den Hartog
• Keywords: Formal Verification Technique, Game Based Correctness, Probabilistic Hoare Style, SCP 2008