CAPSL is a formal language for expressing authentication and key-exchange protocols. Its purpose is to express enough of the abstract features of these protocols to support an analysis for protocol failures. Publications produced under the project or in related projects are listed below.

CAPSL was extended to MuCAPSL to express group multicast protcols. MuCAPSL includes significant new features such as a higher-level organization of protocols into suites, group addressing, and variable-length messages. An introduction to some of its new features is available.

Another important development arising from the CAPSL activity is the constraint-solving approach for protocol analysis.

The first version of CAPSL was developed in early 1996 with the idea in mind that it could be used by any of several protocol analysis tools and techniques. With the help of a common understanding of CAPSL syntax and semantics, the developers of each tool could translate it into the internal form required by their tools. The definition of the language has been influenced, and is still being influenced, by the suggestions and needs of the researchers in this area.

This web site is intended to support refinement and standardization of the language definition, and to act as a repository of CAPSL-related software tools, as available. Please send suggestions for the language design and expository material to J. Millen.

CAPSL-related resources at this site also include a tutorial, some examples, the standard CAPSL prelude, an incomplete but perhaps helpful Bibtex bibliography, a CAPSL-to-CIL translator, and a CAPSL version of the Clark-Jacob protocol library.

Documents and Papers

MuCAPSL (postscript) by Millen and Denker, for DISCEX III, April, 2003. Abstract

On the Freedom of Decryption (postscript) by Millen. Information Processing Letters, 86(6), June 2003, pp. 329-333. Abstract

Modeling Group Communication Protocols Using Multiset Term Rewriting by Denker and Millen, to appear in Proceedings of WRLA '02, Electronic Notes in Theoretical Computer Science, ENTCS, Elsevier Science Publishers, 2002. Abstract

CAPSL and MuCAPSL by Millen and Denker, J. Telecommunications and Information Technology, 4/2002, pp. 16-27. Abstract (See JTIT.)

Cryptographic Protocol Generation from CAPSL (postscript) by Millen and Muller, SRI-CSL-01-07, December 2001, for NSF. Abstract

Bounded-Process Cryptographic Protocol Analysis (postscript) by Millen and Shmatikov, for 2001 ACM Conference on Computer and Communication Security. The associated Prolog program and NSL example are available. Abstract

Applications of Term Rewriting to Cryptographic Protocol Analysis, by Millen, in Electronic Notes in Theoretical Computer Science, ENTCS Vol. 36 (ed. Kokichi Futatsugi), Elsevier Science Publishers, 2001. Abstract

Proving Secrecy is Easy Enough (postscript) by Cortier, Millen, and Ruess, for 2001 Computer Security Foundations Workshop. (Supported in part by NSF) Abstract

The CAPSL Integrated Protocol Environment (postscript) by Denker, Millen, and Ruess; TIPE project final report and language reference document. Abstract

Local Secrecy for State-Based Models (postscript) by Ruess and Millen, for Formal Methods in Computer Security, CAV workshop, Chicago, 2000

Design of a CIL Connector to Maude (postscript) by G. Denker, for Formal Methods in Computer Security, CAV workshop, Chicago, 2000

A CAPSL Connector to Athena (postscript file) for Formal Methods in Computer Security, CAV workshop, Chicago, 2000 (abstract).

Optimizing Protocol Rewrite Rules of CIL Specifications (postscript file) by Denker, Millen, Grau, and Kuester Filipe, for 2000 Computer Security Foundations Workshop.

Protocol-Independent Secrecy (postscript file) by Millen and Ruess, for IEEE 2000 Security and Privacy Symposium. (abstract).

CAPSL Integrated Protocol Environment (postscript file) by Denker and Millen, for DARPA Information Survivability Conference, January 2000. 15-page overview. There is a Powerpoint presentation also.

CAPSL Intermediate Language (postscript file) by Denker and Millen, presented at FMSP '99 (abstract). A ten-page summary of CIL concepts and issues.

A Necessarily Parallel Attack (Postscript), shows PVS verification technique, FMSP '99, also SRI Technical Report CSL-98-00, August 1998. Abstract

CAPSL and CIL Language Design (postscript file) by Denker and Millen, SRI-CSL-99-02, February 1999; (outdated)

The Agent Model is discussed in this draft document, suggesting an object-oriented approach for representing the relationship between agents and session processes, affecting environment specifications. (4/11/00)

S. Brackin, C. Meadows, and J. Millen, CAPSL Interface for the NRL Protocol Analyzer, (postscript) IEEE Symposium on Application-Specific Systems and Software Engineering Technology (ASSET '99, Dallas, March 1999); abstract.