Security modelling for electronic commerce: The common electronic purse specifications

Abstract

Designing security-critical systems correctly is very difflcult. We present work on software engineering of security critical systems, supported by the CASE tool AUTOFOCUS. Security critical systems are specified with extended structure diagrams, message sequence charts for the protocols and statecharts for the attacker, translated into an AUTOFOCUS system model and examined for security weaknesses using model checking. Additionally, the specifications could be simulated or tested - which is a first step towards integration of cryptographic primitives, intuitive graphical modelling, simulation and model checking. We explain our method at the example of a part of the Common Electronic Purse Specifications (CEPS), and comment on potential of vulnerability and consequences for the design. © 2002 Kluwer Academic Publishers.