Automated deduction with XOR constraints

This paper describes £rst-order theorem proving with XOR constraints. The purpose of these constraints is to facilitate ef£cient reasoning with models of APIs of hardware security modules (HSMs), which frequently employ XOR as a cryptographic operation. The self-inverse and associative-commutative properties of XOR cause a large combinatorial blow-up in the number of possible actions an attacker ca