In this work, we present the first automated analysis of security application programming interfaces (security APIs). In particular, we analyze the API of the IBM 4758 CCA, a hardware security module for banking networks. Adapting techniques from formal analyses of security protocols, we model the API purely according its specification and assuming ideal encryption primitives. We then use the automated theorem-prover Otter to analyze this model, combining its standard reasoning strategies with novel techniques of our own (also presented here). In this way, we derive not only all published API-level attacks against the 4758 CCA, but an extension to these attacks as well. Thus, this work represents the first step toward fully-automated, rigorous analyses of security APIs.
CITATION STYLE
Youn, P., Adida, B., Bond, M., Clulow, J., Herzog, J., Lin, A., … Anderson, R. (2010). Robbing the bank with a theorem prover. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5964 LNCS, p. 171). Springer Verlag. https://doi.org/10.1007/978-3-642-17773-6_21
Mendeley helps you to discover research relevant for your work.