Variant of Safe Ambient Calculus and its Contextual Bisimulation
Qian Ma · Mini-micro Systems · 2005
Computation with mobility becomes a novel distributed computation paradigm with the development of network technology. The calculus of Mobile Ambient is a widely studied formal mechanism for describing both mobile computing and mobile computation. This paper deals with one of its variants, the Safe Ambient calculus (SA) . In details, this paper modify the syntactic definition of SA, as a result, the security checking action is unified to be executed when an ambient is to be entered, which makes it fit into the intuition more accurately. At the same time, an improved contextual bisimulation is given by the means of Honda-Yoshida′s technique, which leads to a finer algebraic property. An example of firewall is provided to show the soundness of the improved calculus and its behavior equivalence.