A Generic API for Key Management

Experiments: Implementing Protocols with the API

This page links to experiments with an algorithm for instantiating a generic security API to implement protocols from the Clark-Jacob corpus. The experiments are described in a paper entitled A Generic Security API for Symmetric Key Management on Cryptographic Devices, by Véronique Cortier and Graham Steel (to appear at ESORICS 2009)

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

  1. Carlsen's Secret Key Initiator
  2. Neuman Stubblebine
  3. Needham Schroeder Shared key (original)
  4. Needham Schroeder Shared key (revised)
  5. Otway Rees (original)
  6. Woo Lam Mutual Authentication
  7. Yahalom
Note (for the benefit of search engines) The original submitted version of this paper was called Synthesising Secure APIs, and it appeared in the ESORICS 2009 list of accepted papers under this title. However, following the advice of an anonymous reviewer, we changed the title for the camera ready version

About LSV