Design of a CIL connector to SPIN

Author

Yongjian, Li ; Rui, Xue

Author_Institution

Lab. of Comput. Sci., Chinese Acad. of Sci., Beijing

fYear

2004

Firstpage

349

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 2004. COMPSAC 2004. Proceedings of the 28th Annual International

Conference_Location

Hong Kong

ISSN

0730-3157

Print_ISBN

0-7695-2209-2

Type

conf

DOI

10.1109/CMPSAC.2004.1342857

Filename

1342857