The certification of the Mondex electronic purse to ITSEC level E6

TY - JOUR

T1 - The certification of the Mondex electronic purse to ITSEC level E6

AU - Woodcock, J

AU - Stepney, S

AU - Cooper, David

AU - Clark, John Andrew

AU - Jacob, Jeremy Lawrence

N1 - Query date: 14/01/2011

PY - 2008/1

Y1 - 2008/1

N2 - Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assurance for secure systems. This involved building formal models in the Z notation, linking them with refinement, and proving that they correctly implement the required security properties. The work has been revived recently as a pilot project for the international Grand Challenge in Verified Software. This paper records the history of the original project and gives an overview of the formal models and proofs used.

AB - Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assurance for secure systems. This involved building formal models in the Z notation, linking them with refinement, and proving that they correctly implement the required security properties. The work has been revived recently as a pilot project for the international Grand Challenge in Verified Software. This paper records the history of the original project and gives an overview of the formal models and proofs used.

KW - certification

KW - correctness

KW - electronic finance

KW - grand challenges

KW - Grand Challenge in Verified Software

KW - ITSEC Level E6

KW - Mondex

KW - refinement

KW - security

KW - smart cards

KW - theorem proving

KW - verification

KW - Verified Software Repository

KW - Z notation

KW - REFINEMENT

UR - http://www.scopus.com/inward/record.url?scp=37549043961&partnerID=8YFLogxK

U2 - 10.1007/s00165-007-0060-5

DO - 10.1007/s00165-007-0060-5

M3 - Article

SN - 0934-5043

VL - 20

SP - 5

EP - 19

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 1

ER -