Encoding cryptographic primitives in a calculus with polyadic synchronization

We thoroughly study the behavioural theory of epi, a π-calculus extendedwith polyadic synchronisation. We show that the natural contextual equivalence,barbed congruence, coincides with early bisimilarity, which is thus its co-inductivecharacterisation. Moreover, we relate early bisimilarity with the other usual notions,ground, late and open, obtaining a lattice of equivalence relations that clarifies therelationship among the “standard” bisimilarities. Furthermore, we apply the theorydeveloped to obtain an expressiveness result: epi extended with key encryptionprimitives may be fully abstractly encoded in the original epi calculus. The proposedencoding is sound and complete with respect to barbed congruence; hence, cryptographicepi (crypto-epi) gets behavioural theory for free, which contrasts with otherprocess languages with cryptographic constructs that usually require a big effort todevelop such theory. Therefore, it is possible to use crypto-epi to analyse and toverify properties of security protocols using equational reasoning. To illustrate thisclaim, we prove compliance with symmetric and asymmetric cryptographic systemlaws, and the correctness of a protocol of secure message exchange.