Affiliations: [a] Istituto di Informatica e Telematica – CNR, Via G. Moruzzi 1, I-56100 Pisa, Italy. E-mail: [email protected], [email protected] | [b] Dipartimento di Scienze, Università “D'Annunzio” di Chieti-Pescara, Viale Pindaro 87, 65127 Pescara, Italy. E-mail: [email protected] | [c] Advanced Engineering and Science Division, ITT Industries Inc., Alexandria, VA 22303, USA. E-mail: [email protected] | [d] Istituto di Scienza e Tecnologie dell'Informazione – CNR, Via G. Moruzzi 1, I-56100 Pisa, Italy. E-mail: [email protected] | [e] Department of Computer Science, University of Twente, 7500 AE Enschede, The Netherlands. E-mail: [email protected]
Abstract: When formalizing security protocols, different specification languages support very different reasoning methodologies, whose results are not directly or easily comparable. Therefore, establishing clear mappings among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting theoretical and practical results of one system into another. In this paper, we examine the relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to CCS and the π-calculus. Although defining a simple and general bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify cryptographic protocols admit an effective translation that is not only trace-preserving, but also induces a correspondence relation between the two languages. In particular, the correspondence sketched in this paper permits transferring several important trace-based properties such as secrecy and many forms of authentication.
