Deduction with XOR Constraints in Security API Modelling

Graham Steel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationAutomated Deduction - CADE-20
Subtitle of host publication20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005. Proceedings
EditorsRobert Nieuwenhuis
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-540-31864-4
ISBN (Print)978-3-540-28005-7
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Deduction with XOR Constraints in Security API Modelling'. Together they form a unique fingerprint.

Cite this