Abstractions for Network Security† MICH E L E B U G L I E S I, R I C C A R D O F O C A R D I Dipartimento di Informatica, Universit`a Ca’ Foscari, Venice. Received 6 October 2010 Process algebraic techniques for distributed systems are increasingly being targeted at ing abstractions adequate both for high-level programming and specification, and for security analysis and verification. Drawing on our earlier work in (Bugliesi and Focardi, 2008), we investigate the expressive power of a core set of security and network ions that provide high-level primitives for the specifications of the honest principals in a network, while at the same time enabling an analysis of the network-level adversarial attacks that may be mounted by an intruder. We analyze various bisimulation equivalences for security, arising from endowing the intruder with (i) different adversarial capabilities and (ii) increasingly powerful control on the interaction among the distributed principals of a network. By ...