  This paper is the first thorough investigation into the coarsest notion of
bisimilarity for the applied pi-calculus that is a congruence relation: open
barbed bisimilarity. An open variant of labelled bisimilarity (quasi-open
bisimilarity), better suited to constructing bisimulations, is proven to
coincide with open barbed bisimilarity. These bisimilary congruences are shown
to be characterised by an intuitionistic modal logic that can be used, for
example, to describe an attack on privacy whenever a privacy property is
violated. Open barbed bisimilarity provides a compositional approach to
verifying cryptographic protocols, since properties proven can be reused in any
context, including under input prefix. Furthermore, open barbed bisimilarity is
sufficiently coarse for reasoning about security and privacy properties of
cryptographic protocols; in constrast to the finer bisimilarity congruence,
open bisimilarity, which cannot verify certain privacy properties.
