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

C. George; Anne Elisabeth Haxthausen

doi:10.1007/s00165-007-0054-3

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

Research output: Contribution to journal › Journal article › Research › peer-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 language	English
Journal	Formal Aspects of Computing
Volume	20
Issue number	1
Pages (from-to)	101-116
ISSN	0934-5043
DOIs	https://doi.org/10.1007/s00165-007-0054-3
Publication status	Published - 2008

Keywords

PVS
Formal methods
Verification
RAISE
Mondex
SAL

Access to Document

10.1007/s00165-007-0054-3

OpenUrl availability

Full text

Cite this

@article{1f8836673fd741d69a4f1c7cd08eb279,

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

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.",

keywords = "PVS, Formal methods, Verification, RAISE, Mondex, SAL",

author = "C. George and Haxthausen, \{Anne Elisabeth\}",

year = "2008",

doi = "10.1007/s00165-007-0054-3",

language = "English",

volume = "20",

pages = "101--116",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery",

number = "1",

}

TY - JOUR

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

AU - George, C.

AU - Haxthausen, Anne Elisabeth

PY - 2008

Y1 - 2008

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

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

KW - PVS

KW - Formal methods

KW - Verification

KW - RAISE

KW - Mondex

KW - SAL

U2 - 10.1007/s00165-007-0054-3

DO - 10.1007/s00165-007-0054-3

M3 - Journal article

SN - 0934-5043

VL - 20

SP - 101

EP - 116

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 1

ER -

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

Abstract

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this