Formal modeling and verification of secure mobile agent systems

Security of a Mobile Agent System (MAS), which has been a barrier to wider applications of a MAS, remains a compelling problem. Formal methods have been applied to this problem, and various formal models have recently been studied. However, many of them either lack of mechanisms that can protect a MAS or depend on simulation based analysis. In this paper, we concentrate on one specific category of security threats, namely, the agent-platform related security issues, and present a new method for formally modeling and verifying a secure MAS. To model a secure MAS, we equip the MAS with secure mechanisms, and propose an extended logical agent model (ELAM) for formally describing it. By transforming the ELAM to the input model of model checker SPIN, the MAS is further verified by using model checking technique. We apply ELAM to the competing airline carriers system to check its security, and our experimental results show that the proposed method works well in modeling and verifying a secure MAS.