{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T13:57:17Z","timestamp":1649080637209},"reference-count":6,"publisher":"World Scientific Pub Co Pte Lt","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2008,2]]},"abstract":"<jats:p> 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. <\/jats:p>","DOI":"10.1142\/s0218194008003568","type":"journal-article","created":{"date-parts":[[2008,4,21]],"date-time":"2008-04-21T09:18:43Z","timestamp":1208769523000},"page":"65-91","source":"Crossref","is-referenced-by-count":0,"title":["DESIGN OF A CIL CONNECTOR TO SPIN"],"prefix":"10.1142","volume":"18","author":[{"given":"YONGJIAN","family":"LI","sequence":"first","affiliation":[{"name":"Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China"},{"name":"The State Key Laboratory of Information Security, Beijing 100080, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"RUI","family":"XUE","sequence":"additional","affiliation":[{"name":"The State Key Laboratory of Information Security, Beijing 100080, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf5","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00095-X"},{"key":"rf8","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"Song D.","journal-title":"J. Computer Security"},{"key":"rf9","volume-title":"The GENTLE Compiler Construction System","author":"Schroder F. W.","year":"1997"},{"key":"rf10","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46017-9_14"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194008003568","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T01:44:53Z","timestamp":1565142293000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194008003568"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,2]]},"references-count":6,"journal-issue":{"issue":"01","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2008,2]]}},"alternative-id":["10.1142\/S0218194008003568"],"URL":"https:\/\/doi.org\/10.1142\/s0218194008003568","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,2]]}}}