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

Jeremy den Hartog

    Research output: Book/ReportReportProfessional

    19 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).
    den Hartog, Jeremy. / Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic Hoare style logic. Enschede : Distributed and Embedded Security (DIES), 2007. 20 p. (CTIT Technical Report Series; LNCS4549/TR-CTIT-07-53).
    @book{481ec5168f844d0bae18fcb6b21f3408,
    title = "Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic Hoare style logic",
    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].",
    keywords = "METIS-241835, IR-64280, EWI-10860",
    author = "{den Hartog}, Jeremy",
    year = "2007",
    month = "8",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Distributed and Embedded Security (DIES)",
    number = "LNCS4549/TR-CTIT-07-53",

    }

    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, Distributed and Embedded Security (DIES), Enschede.

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

    Enschede : Distributed and Embedded Security (DIES), 2007. 20 p. (CTIT Technical Report Series; No. LNCS4549/TR-CTIT-07-53).

    Research output: Book/ReportReportProfessional

    TY - BOOK

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

    AU - den Hartog, Jeremy

    PY - 2007/8

    Y1 - 2007/8

    N2 - 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].

    AB - 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].

    KW - METIS-241835

    KW - IR-64280

    KW - EWI-10860

    M3 - Report

    T3 - CTIT Technical Report Series

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

    PB - Distributed and Embedded Security (DIES)

    CY - Enschede

    ER -

    den Hartog J. Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic Hoare style logic. Enschede: Distributed and Embedded Security (DIES), 2007. 20 p. (CTIT Technical Report Series; LNCS4549/TR-CTIT-07-53).