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

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.