Design of a CIL Connector to Maude
The CAPSL Integrated Protocol Environment effort aims at providing
an intuitive and expressive language
for specifying cryptographic authentication and key distribution protocols
and supporting interfaces to various analysis tools. The
CAPSL Intermediate Language CIL has been designed with the emphasis
on simplifying translators from CIL to other analysis tools.
In this paper we describe the design
of a CIL-to-Maude connector. Maude is a rewriting logic based,
efficiently executable specification language that has been
extended by a model checking tool. We describe how CIL concepts are
translated in Maude and propose several optimization techniques in order
to achieve protocol specifications that are efficiently executable
and analyzable with the Maude model checker. A prototype connector
has been implemented in Java.