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.

• maudeconpaper.ps