On the Decidability of a Class of XOR-based Key-management APIs

Véronique Cortier, Graham Steel

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


We define a new class of security protocols using XOR, and show that secrecy after an unbounded number of sessions is decidable for this class. The new class is important as it contains examples of key-management APIs, such as the IBM 4758 CCA API, which lie outside the classes for which secrecy has previously been shown to be decidable. Earlier versions of the CCA API were shown to have serious flaws, and the fixes introduced by IBM in version 2.41 have not been formally verified in a model with unbounded sessions. In showing the decidability of this class, we also suggest a simple decision procedure, which we plan to implement in future work to finally verify the revised API.
Original languageEnglish
Title of host publicationFCS-ARSPA 2006 Proceedings
Number of pages15
Publication statusPublished - 2006


Dive into the research topics of 'On the Decidability of a Class of XOR-based Key-management APIs'. Together they form a unique fingerprint.

Cite this