Formally testing fail-safety of electronic purse protocols

Designing and implementing security-critical systems correctly is difficult. In practice, most vulnerabilities arise from bugs in implementations. We present work towards systematic specification-based testing of security-critical systems using the CASE tool AutoFocus. Cryptographic systems are formally specified with state transition diagrams, a notation for state machines in the AutoFocus system., We show how to systematically generate test sequences for security properties based on the model that can be used to test the implementation for vulnerabilities. In particular we focus on the principle of fail-safety. We explain our method at the example of a part of the Common Electronic Purse Specifications (CEPS). Most commonly, attacks address vulnerabilities in the way security mechanisms are used, rather than the mechanisms themselves. Being able to treat security aspects with a general CASE tool within the context of system development enables detection of such vulnerabilities.