Proof methodologies for behavioural equivalence in DPI

Abstract

We focus on techniques for proving behavioural equivalence between systems in Dpi, a distributed version of the picalculus in which processes may migrate between dynamically created locations, and where resource access policies are implemented by means of capability types. We devise a tractable collection of auxiliary proof methods, relying mainly on the use of bisimulations up-to -reductions, which considerably relieve the burden of exhibiting witness bisimulations. Using such methods we model simple distributed protocols, such as crossing a firewall, the interaction between a server and its clients, metaservers installing memory services, and address their correctness in a relatively simple manner.