27/01/2012, 16:15 — 17:15 — Room P3.10, Mathematics Building
Marco Giunti, Laboratoire informatique (LIX), École Polytechnique
Programming Secrecy in Untrusted Networks
The idea that the restriction operator of the pi-calculus (new) and
its scope extrusion mechanism can model the possession and
communication of a secret goes back to the spi-calculus. In this
approach, one can devise specifications of protocols that rely on
channel-based communication protected by new, and establish the
desired security properties by using equivalences representing
indistinguishability in the presence of a Dolev-Yao attacker.
However, while some protocol can assume dedicated channels to be
available, it is not obvious how to enforce secret communications
over the Transport/Internet layer. In practice, the secrecy of the
open communications is recovered by relying on cryptographic
mechanisms which can be very complex in the presence of scope
extrusion. Based on these considerations, in this talk we enrich
the pi-calculus with an operator for confidentiality (hide), whose
main effect is to restrict the access to the communication channel,
thus representing confidentiality in a natural way. The hide
operator is meant for local communication, and it differs from new
in that it forbids the extrusion of the channel and hence has a
static scope. Consequently, a communication channel in the scope of
a hide can be implemented as a dedicated channel, and it is more
secure than one in the scope of a new. To emphasize the difference,
we introduce a spy process that represents a side-channel attack
and breaks some of the standard security equations for new. To
formally reason on the security guarantees provided by the hide
construct, we introduce an observational theory and establish
stronger equivalences by relying on a proof technique based on
bisimulation semantics. Joint work with Catuscia Palamidessi and
Frank D. Valencia.
