@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},
}