Sciweavers

SCP
2008

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

13 years 12 months ago
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].
Jerry den Hartog
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2008
Where SCP
Authors Jerry den Hartog
Comments (0)