Behavioral Equivalence of Security-Oriented Interactive Systems

Guanjun LIU  Changjun JIANG  

IEICE TRANSACTIONS on Information and Systems   Vol.E99-D   No.8   pp.2061-2068
Publication Date: 2016/08/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2015INP0017
Type of Manuscript: Special Section PAPER (Special Section on Security, Privacy and Anonymity of Internet of Things)
interactive systems,  labelled petri nets,  labelled transition systems,  bisimulation,  security,  

Full Text: PDF(563.6KB)>>
Buy this Article

In the classical computation theory, the language of a system features the computational behavior of the system but it does not distinguish the determinism and nondeterminism of actions. However, Milner found that the determinism and nondeterminism affect the interactional behavior of interactive systems and thus the notion of language does not features the interactional behavior. Therefore, Milner proposed the notion of (weak) bisimulation to solve this problem. With the development of internet, more and more interactive systems occur in the world, such as electronic trading system. Security is one of the most important topics for these systems. We find that different security policies can also affect the interactional behavior of a system, which exactly is the reason why a good policy can strengthen the security. In other words, two interactive systems with different security policies are not of an equivalent behavior although their functions (or business processes) are identical. However, the classic (weak) bisimulation theory draws an opposite conclusion that their behaviors are equivalent. The notion of (weak) bisimulation is not suitable for these security-oriented interactive systems since it does not consider a security policy. This paper proposes the concept of secure bisimulation in order to solve the above problem.