Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Model Checking IBM's Common Cryptographic Architecture API
Authors: Gavin Keighren
Date:Oct 2006
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
author = { Gavin Keighren },
title = {Model Checking IBM's Common Cryptographic Architecture API},
year = 2006,
month = {Oct},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh