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.

The development of CAPSL and associated protocol verification techniques was supported under the Group Inference project by DARPA through the Navy SPAWAR. There was prior support by DARPA under the TIPE project through Air Force Rome Laboratory.

The first version of CAPSL was developed in early 1996 with the idea 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 was influenced by the suggestions and needs of the researchers in this area.

Staff Members:

• Dr. Grit Denker

• Symbolic Protocol Analysis with Products and Diffie-Hellman Exponentiation  (2003)
• On the Freedom of Decryption  (2003)
• MuCAPSL  (2003)
• Modeling Group Communication Protocols Using Multiset Term Rewriting  (2002)
• CAPSL and MuCAPSL  (2002)
• Proving Secrecy is Easy Enough  (2001)
• Cryptographic Protocol Generation from CAPSL  (2001)
• CAPSL Integrated Protocol Environment  (2000)