TY - JOUR

T1 - Encoding cryptographic primitives in a calculus with polyadic synchronization

AU - Ravara, António Maria Lobo César Alarcão

N1 - URL={http://ctp.di.fct.unl.pt/~aravara/pubs/journals/10-MR-crypto-epi-final.pdf}

PY - 2011/1/1

Y1 - 2011/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/s10817-010-9189-7

DO - 10.1007/s10817-010-9189-7

M3 - Article

VL - 46

SP - 293

EP - 323

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 3-4

ER -