The CAPSL Integrated Protocol Environment
CAPSL is a Common Authentication Protocol Specification
Language intended to support analysis of cryptographic protocols using
formal methods. CAPSL is adapted for use by various protocol analysis
tools using an intermediate language, CIL. This report includes a
CAPSL tutorial, the syntax of CAPSL and CIL, and the abstract
rewriting model underlying CIL. Algorithms are given for translating
CAPSL to CIL and for CIL rule optimization. Methods are given for
integration of CAPSL and CIL with analysis tools, specifically PVS,
Maude, and Athena, and for protocol analysis using PVS and Maude.