Types for Access Control in a Calculus of Mobile Resources

This paper presents a type system for the calculus of Mobile Resources (MR) proposed by Godskesen et al. The type system is able to prevent undesirable border-crossing behaviour such as Trojan horses. This is achieved by combining the notion of group with a notion of security policy. Well-typed processes satisfy a safety property which is preserved under reduction. An algorithm is presented which computes the minimal security policy making a process well typed.