Relating Process Algebras and Multiset Rewriting for Security Protocol Analysis

Abstract. When formalizing security protocols, different specification languages support very different reasoning methodologies, whose results are not directly or easily comparable. Therefore, establishing clear map-pings among different frameworks is highly desirable, as it permits vari-ous methodologies to cooperate by interpreting theoretical and practical results of one system in another. In this paper, we examine the non-trivial relationship between two general verification frameworks: multi-set rewriting (MSR) and a process algebra (PA) inspired to CCS and the pi-calculus. Although defining a simple and general bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify a large class of cryptographic protocols (immediate decryption protocols) admits an effective translation that is not only bijective and trace-preserving, but also induces a weak form of bisimulation across the two languages. In particular, the correspondence sketched in this ab-stract permits transferring several important trace-based properties suc