Secrecy in Untrusted Networks

We investigate the protection of migrating agents against the untrusted sites they traverse. The resulting calculus provides a formal framework to reason about protection policies and security protocols over distributed, mobile infrastructures, and aims to stand to ambients as the spi calculus stands to π. We present a type system that separates trusted and untrusted data and code, while allowing safe interactions with untrusted sites. We prove that the type system enforces a privacy property, and show the expressiveness of the calculus via examples and an encoding of the spi calculus.

• Type: Conference
• Year: 2003
• Where: ICALP
• Authors: Michele Bugliesi, Silvia Crafa, Amela Prelic, Vladimiro Sassone
• Keywords: Formal Framework, ICALP 2003, Spi Calculus, Theoretical Computer Science, Untrusted Sites