by Graham Steel
Abstract:
Personal identification number (PIN) blocks are 64-bit strings that encode a PIN ready for encryption and secure transmission in banking networks. These networks employ tamper-proof hardware security modules (HSMs) to perform sensitive cryptographic operations, such as checking the correctness of a PIN typed by a customer. The use of these HSMs is controlled by an API designed to enforce security. PIN block attacks are unanticipated sequences of API commands which allow an attacker to determine the value of a PIN in an encrypted PIN block. This paper describes a framework for formal analysis of such attacks. Our analysis is probabilistic, and is automated using constraint logic programming and probabilistic model checking.
Reference:
Formal analysis of PIN block attacks (Graham Steel), In Theoretical Computer Science, Elsevier Science Publishers, volume 367, 2006.
Bibtex Entry:
@article{steel-tcs06,
abstract = {Personal identification number (PIN) blocks are
64-bit strings that encode a PIN ready for encryption
and secure transmission in banking networks. These
networks employ tamper-proof hardware security
modules (HSMs) to perform sensitive cryptographic
operations, such as checking the correctness of a PIN
typed by a customer. The use of these HSMs is
controlled by an API designed to enforce security.
PIN block attacks are unanticipated sequences of API
commands which allow an attacker to determine the
value of a PIN in an encrypted PIN block. This paper
describes a framework for formal analysis of such
attacks. Our analysis is probabilistic, and is
automated using constraint logic programming and
probabilistic model checking.},
author = {Steel, Graham},
DOI = {10.1016/j.tcs.2006.08.042},
journal = {Theoretical Computer Science},
month = nov,
number = {1-2},
pages = {257-270},
publisher = {Elsevier Science Publishers},
title = {Formal analysis of {PIN} block attacks},
volume = {367},
year = {2006},
nmonth = {11},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Steel-tcs06.pdf},
PDF = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Steel-tcs06.pdf},
lsv-category = {jour},
lsv-time = {ant},
wwwpublic = {perso},
}