- Abstract:
-
We present results from the application of a model checker to the analysis of the API used by a number of security modules in Automated Teller Machine networks --- IBM's Common Cryptographic Architecture API. We show that it is capable of rediscovering all known attacks on the API, using models containing a greater set of API commands.
We also analyse the set of recommendations released, in response to one of the discovered attacks, by IBM and show that, under certain assumptions, they do not prevent the attack. We use a revised set of assumptions, under which they do prevent the attack, to determine a number of our own recommendations aimed at the design and implementation of the API.
Finally, we discuss various issues concerning the analysis of security APIs, based on our experiences of carrying out the work presented.
- Links To Paper
- 1st Link
- Bibtex format
- @Misc{EDI-INF-RR-0862,
- author = {
Gavin Keighren
},
- title = {Model Checking IBM's Common Cryptographic Architecture API},
- year = 2006,
- month = {Oct},
- url = {http://dream.inf.ed.ac.uk/publications/Keighren-Techreport.pdf},
- }
|