Security Abstractions and Intruder Models

Process algebraic specifications of distributed systems are increasingly being targeted at identifying security primitives well-suited as high-level programming abstractions, and at the same time adequate for security analysis and verification. Drawing on our earlier work along these lines in [Bugliesi and Focardi 2008], we investigate the expressive power of a core set of security and network abstractions that provide high-level primitives for the specifications of the honest principals in a network as well as the lower-level adversarial primitives that must be assumed available to an attacker. 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 comparing the relative strength of the bimimulation equivalences we obtain a a direct measure of the discriminating power of the intruders, hence of the expressiveness of the corresponding models.