DESIGN OF A CIL CONNECTOR TO SPIN
Yongjian Li, Rui Xue · International Journal of Software Engineering and Knowledge Engineering · 2008
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-Spin connector. We describe how CIL concepts are translated into Spin and propose a general method to model the behaviors of honest principals and the intruder. Based on the method, a prototype connector has been implemented in Gentle, which automatically translates CIL specifications to Promela codes and LTL formulae, thus greatly simplifying the modeling and analysis process.