Information Security Seminar 

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.