Deduction with XOR Constraints in Security API Modelling

Graham Steel

doi:10.1007/11532231_24

Deduction with XOR Constraints in Security API Modelling

Graham Steel

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Automated Deduction - CADE-20
Subtitle of host publication	20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005. Proceedings
Editors	Robert Nieuwenhuis
Publisher	Springer
Pages	322-336
Number of pages	15
ISBN (Electronic)	978-3-540-31864-4
ISBN (Print)	978-3-540-28005-7
DOIs	https://doi.org/10.1007/11532231_24
Publication status	Published - 2005

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	3632
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/11532231_24

6 steel cade05Submitted manuscript, 370 KB

Cite this

@inproceedings{3d51eedda5fb4bcaacc69037c70ed31e,

title = "Deduction with XOR Constraints in Security API Modelling",

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.",

author = "Graham Steel",

year = "2005",

doi = "10.1007/11532231_24",

language = "English",

isbn = "978-3-540-28005-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "322--336",

editor = "Robert Nieuwenhuis",

booktitle = "Automated Deduction - CADE-20",

address = "United Kingdom",

}

Deduction with XOR Constraints in Security API Modelling. / Steel, Graham.
Automated Deduction - CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005. Proceedings. ed. / Robert Nieuwenhuis. Springer, 2005. p. 322-336 (Lecture Notes in Computer Science; Vol. 3632).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Deduction with XOR Constraints in Security API Modelling

AU - Steel, Graham

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

U2 - 10.1007/11532231_24

DO - 10.1007/11532231_24

M3 - Conference contribution

SN - 978-3-540-28005-7

T3 - Lecture Notes in Computer Science

SP - 322

EP - 336

BT - Automated Deduction - CADE-20

A2 - Nieuwenhuis, Robert

PB - Springer

ER -

Deduction with XOR Constraints in Security API Modelling

Abstract

Publication series

Access to Document

Fingerprint

Cite this