Deduction with XOR Constraints in Security API Modelling (bibtex)
by Graham Steel
Abstract:
We introduce XOR constraints, and show how they enable a theorem prover to reason effectively about security critical subsystems which employ bitwise XOR. Our primary case study is the API of the IBM 4758 hardware security module. We also show how our technique can be applied to standard security protocols.
Reference:
Deduction with XOR Constraints in Security API Modelling (Graham Steel), In Proceedings of the 20th International Conference on Automated Deduction (CADE'05) (Robert Nieuwenhuis, ed.), Springer, volume 3632, 2005.
Bibtex Entry:
@inproceedings{steel-cade05,
  abstract =      {We introduce XOR constraints, and show how they
                   enable a theorem prover to reason effectively about
                   security critical subsystems which employ bitwise
                   XOR. Our primary case study is the API of the IBM
                   4758 hardware security module. We also show how our
                   technique can be applied to standard security
                   protocols.},
  address =       {Tallinn, Estonia},
  author =        {Steel, Graham},
  booktitle =     {{P}roceedings of the 20th {I}nternational
                   {C}onference on {A}utomated {D}eduction ({CADE}'05)},
  DOI =           {10.1007/11532231_24},
  editor =        {Nieuwenhuis, Robert},
  month =         jul,
  pages =         {322-336},
  publisher =     {Springer},
  series =        {Lecture Notes in Artificial Intelligence},
  title =         {Deduction with {XOR} Constraints in Security {API}
                   Modelling},
  volume =        {3632},
  year =          {2005},
  acronym =       {{CADE}'05},
  nmonth =        {7},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-cade05.pdf},
  PDF =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-cade05.pdf},
  lsv-category =  {intc},
  lsv-time =      {ant},
  wwwpublic =     {perso},
}
Powered by bibtexbrowser