A Compositional and Complete approach to Verifying Privacy Properties using the Applied Pi-calculus

The pi-calculus was introduced for verifying cryptographic protocols by Abadi and Fournet in 2001. They proposed an equivalence technique, called bisimilarity, useful for verify privacy properties. It is widely acknowledged (cf. Paige and Tarjan 1987), that bisimilarity is more efficient to check than trace equivalence; however, surprisingly, tools based on the applied pi-calculus typically still implement trace equivalence. I suggest this may be attributed to two problems:1. Abadi and Fournet did not publish proofs following conference paper from 2001, until a journal version in 2018 with Blanchet. This perhaps reduced the confidence of the community in bisimilarity. Further to providing proofs, the journal version adjusts definitions to avoid some well known limitations in the original presentation.2. To efficiently implement bisimulation for extensions of the pi-calculus, we typically require a bisimilarity congruence, and no bisimilarity congruence has been proposed for the applied pi-calculus.To address the second point above I propose a bisimilarity congruence for the applied pi-calculus. I argue that the definition I provide is optimal; and show that it is sufficiently strong to verify privacy properties. The definition makes use of recent advances in concurrency theory that were not available prior to LICS 2018. Furthermore, these results lead us to the first sound and complete modal logic for the applied pi-calculus, that can specify attacks if and only if an attack exists.