Type-Based Analysis of PIN Processing APIs

We examine some known attacks on the PIN verification framework, based on weaknesses of the security API for the tamperresistant Hardware Security Modules used in the network. We specify this API in an imperative language with cryptographic primitives, and show how its flaws are captured by a notion of robustness that extends the one of Myers, Sabelfeld and Zdancewic to our cryptographic setting. We propose an improved API, give an extended type system for assuring integrity and for preserving confidentiality via randomized and nonrandomized encryptions, and show our new API to be type-checkable.

• Type: Conference
• Year: 2009
• Where: ESORICS
• Authors: Matteo Centenaro, Riccardo Focardi, Flaminia L. Luccio, Graham Steel
• Keywords: ESORICS 2009, Improved Api, PIN Verification Framework, Security Api, Security Privacy