The goal of this project is to produce a new flexible specification for a security API that manages cryptographic keys. Unlike existing designs such as RSA PKCS#11 which were designed principally to promote interoperable access to cryptiohrapgic functionality and then were retrofitted with security features, our proposal considers security from the start, imposing a hierarchy on keys and admitting proofs of strong security properties even under corruption.
Below are links to source code for the experiments described in the paper A Generic Security API for Symmetric Key Management on Cryptographic Devices.
The algorithm has been implemented in Prolog. It has been tested in SICStus Prolog but contains little in the way of non-standard features and should work with any ANSI compliant Prolog (you may have to change the declarations for dynamic predicates).
The links below are to input files for various protocols. After 'consult'ing the code above, try these with the query go(filename).