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

Jeremy den Hartog

    Research output: Book/ReportReportProfessional

    20 Downloads (Pure)

    Abstract

    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].
    Original languageUndefined
    Place of PublicationEnschede
    PublisherDistributed and Embedded Security (DIES)
    Number of pages20
    Publication statusPublished - Aug 2007

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology
    No.LNCS4549/TR-CTIT-07-53
    ISSN (Print)1381-3625

    Keywords

    • METIS-241835
    • IR-64280
    • EWI-10860

    Cite this

    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).