Specification of the Group Diffie-Hellman Protocol as a Component of the Cliques Toolkit

Mark-Oliver Stehr and Carolyn Talcott

This work is supported by:
the DARPA FTN Project Composable Formal Models for High-Assurance Fault Tolerant Networks and
the ONR MURI Project CONTESSA.

Keywords: Group Communication, Group Diffie-Hellman, Cliques Toolkit, Secure Spread, Formal Specification

The Cliques toolkit is a C library providing an API for secure group communication which has the nice feature that it is to a large extend independent of the actual protocol. One of the protocols that have been implemented is the Group Diffie-Hellman Protocol (GDH) developped by M. Steiner, G. Tsudik and M. Waidner in Key Agreement in Dynamic Peer Groups (see [1] below). Unfortunately, due to outdated documentation there seemed to be some confusion about which version of the protocol has actually been implemented in the toolkit (cf. [3] and [4] below). Our goal in this project was to come up with a formal specification which exactly captures what has been implemented for the case of GHD and also catures the generic nature of the cliques API so that further protocols can be added without major modifications. An analysis of the C source code revealed that the Cliques toolkit does not implement GDH with implicit authentication (called AGDH.2 in [1]) as suggested by the paper The Design of a Group Key Agreement API (see [2] below) and some comments in the source code, but GDH with explicit authentication via digital signatures.

The result of our effort is a rather abstract but realistic specification that we have obtained by reengineering from the C code. Since adding digital signatures is a straightforward task that can be done in a modular we have omitted them in the current version.

Since the Cliques toolkit has been used as part of the Secure Spread group communication system, one possible application of this specification is to serve as a component for a formal specification of Secure Spread.

The current state of our specification is available below, but please note that it is a snapshot of ongoing work and that digital signatures have not been modelled.

Relevant References:

  1. M. Steiner, G. Tsudik and M. Waidner: Key Agreement in Dynamic Peer Groups, IEEE Transactions on Parallel and Distributed Systems, August 2000. Paper available here.
  2. G. Ateniese, O. Chevassut, D. Hasse, Y. Kim and G. Tsudik: The Design of a Group Key Agreement API, DARPA DISCEX 2000, Jan. 2000. Paper available here.
  3. O. Pereira and J. J. Quisquater. A Security Analysis of the Cliques Protocols Suites. In 14-th IEEE Computer Security Foundations Workshop. IEEE Press, June 2001. Paper available here.
  4. C. Meadows, Extending Formal Cryptographic Protocol Analysis Techniques for Group Protocols and Low-Level Cryptographic Primitives, Proceedings of the First Workshop on Issues in the Theory of Security - WITS'00, (P. Degano, editors), pp. 87-92, Geneva, Switzerland, July 8-9 2000. Paper available here.

Presentations:

  1. Composable Formal Models for High-Assurance Fault Tolerance Networks, FTN PI Meeting, July 21-23, 2003, Honolulu, Hawaii. Slides available here: ps pdf.

The Formal Specification in Maude 2.0 (available here) can be found here.
This package contains the following files: