Title :
Design of a CIL connector to SPIN
Author :
Yongjian, Li ; Rui, Xue
Author_Institution :
Lab. of Comput. Sci., Chinese Acad. of Sci., Beijing
Abstract :
The CAPSL Integrated Protocol Environment effort aims at providing an intuitive and expressive language for specifying 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 can automatically translate CIL specification to promela code and LTL formula, thus greatly simplifying the modelling and analysis process
Keywords :
cryptography; formal specification; program interpreters; protocols; specification languages; CAPSL Integrated Protocol Environment; CAPSL Intermediate Language; CIL-to-Spin connector; Gentle; LTL formula; authentication protocols; interfaces; intruder; key distribution protocols; promela code; translators; Authentication; Computer science; Connectors; Contracts; Cryptographic protocols; Cryptography; Electronic mail; Information security; Laboratories; Natural languages;
Conference_Titel :
Computer Software and Applications Conference, 2004. COMPSAC 2004. Proceedings of the 28th Annual International
Conference_Location :
Hong Kong
Print_ISBN :
0-7695-2209-2
DOI :
10.1109/CMPSAC.2004.1342857
