Security Modelling for Electronic Commerce: The Common Electronic Purse Specifications

: Designing security-critical systems correctly is very difficult. 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.

• Type: Conference
• Year: 2001
• Where: I3E
• Authors: Jan Jürjens, Guido Wimmel
• Keywords: Case Tool Autofocus, I3E 2001, I3E 2007, Model Checking, Security Critical Systems