Formal analysis of PIN block attacks (bibtex)
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},
}
Powered by bibtexbrowser