Deduction with XOR Constraints in Security API Modelling

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.

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Graham Steel
• Keywords: Automated Reasoning, CADE 2005, Hardware Security Module, Security Critical Subsystems, XOR Constraints