Encoding Cryptographic Primitives in a Calculus with Polyadic Synchronisation

We thoroughly study the behavioural theory of epi, a ??-calculus extended with polyadic synchronisation. We show that the natural contextual equivalence, barbed congruence, coincides with early bisimilarity, which is thus its co-inductive characterisation. Moreover, we relate early bisimilarity with the other usual notions, ground, late and open, obtaining a lattice of equivalence relations that clarifies the relationship among the ??standard?? bisimilarities. Furthermore, we apply the theory developed to obtain an expressiveness result: epi extended with key encryption primitives may be fully abstractly encoded in the original epi calculus. The proposed encoding is sound and complete with respect to barbed congruence; hence, cryptographic epi (crypto-epi) gets behavioural theory for free, which contrasts with other process languages with cryptographic constructs that usually require a big effort to develop such theory. Therefore, it is possible to use crypto-epi to analyse and to verify properties of security protocols using equational reasoning. To illustrate this claim, we prove compliance with symmetric and asymmetric cryptographic system laws, and the correctness of a protocol of secure message exchange.