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

Publication: Research - peer-reviewJournal article – Annual report year: 2008

View graph of relations

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
Publication date2008
Volume20
Journal number1
Pages101-116
ISSN0934-5043
DOIs
StatePublished
CitationsWeb of Science® Times Cited: 7

Keywords

  • PVS, formal methods, verification, RAISE, Mondex, SAL
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

ID: 3608838