- 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.
- Links To Paper
- 1st link
- 2nd link
- Bibtex format
- @InProceedings{EDI-INF-RR-0267,
- author = {
Graham Steel
},
- title = {Deduction with XOR Constraints in Security API Modelling},
- book title = {Proceedings of the 20th Conference on Automated Deduction (CADE 20), July 2005},
- publisher = {Springer-Verlag},
- year = 2005,
- month = {Jul},
- pages = {322-336},
- doi = {10.1007/11532231_24},
- url = {http://homepages.inf.ed.ac.uk/gsteel/papers/cade-05.pdf},
- }
|
