Trust in the pi-calculus
Mark Hepburn, David A. Wright · 2001
We introduce a new system of trust analysis for concurrent and distributed systems using the π-calculus[13, 14, 15] as a modelling tool. A Type system using boolean annotations guarantees that no run-time errors due to un trusted data being used in a trusted context are possible. We improve on other similar systems[18] by introducing a safe environment in which trust-coercion can be performed based on the results of run-time checks. An algorithm for reducing the most general types for the type system is presented.