In [Corin, den Hartog in ICALP 2006] we build a formal verification technique for game based correctness proofs of cryptograhic algorithms based on a probabilistic Hoare style logic [den Hartog, de Vink in IJFCS 13(3), 2002]. An important step towards enabling mechanized verification within this technique is an axiomatization of implication between predicates which is purely semantically defined in [den Hartog, de Vink in IJFCS 13(3), 2002]. In this paper we provide an axiomatization and illustrate its place in the formal verification technique of [Corin, den Hartog in ICALP 2006].
|Place of Publication||Enschede|
|Publisher||Distributed and Embedded Security (DIES)|
|Number of pages||20|
|Publication status||Published - Aug 2007|
|Name||CTIT Technical Report Series|
|Publisher||University of Twente, Centre for Telematics and Information Technology|
den Hartog, J. (2007). Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic Hoare style logic. (CTIT Technical Report Series; No. LNCS4549/TR-CTIT-07-53). Enschede: Distributed and Embedded Security (DIES).