Specification, proof, and model checking of the Mondex electronic purse using RAISE

    Research output: Contribution to journalJournal articleResearchpeer-review

    Abstract

    This paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, RSL, and the proofs are made by translation to PVS and SAL. The work is part of a year-long project contributing to the international grand challenge in verified software engineering.
    Original languageEnglish
    JournalFormal Aspects of Computing
    Volume20
    Issue number1
    Pages (from-to)101-116
    ISSN0934-5043
    DOIs
    Publication statusPublished - 2008

    Keywords

    • PVS
    • Formal methods
    • Verification
    • RAISE
    • Mondex
    • SAL

    Cite this