TY - GEN
T1 - Formal modeling and verification of secure mobile agent systems
AU - Jiang, Mingyue
AU - Ding, Zuohua
AU - Zhou, Mengchu
AU - Zhou, Yuan
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/10/7
Y1 - 2015/10/7
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84952790733&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84952790733&partnerID=8YFLogxK
U2 - 10.1109/CoASE.2015.7294136
DO - 10.1109/CoASE.2015.7294136
M3 - Conference contribution
AN - SCOPUS:84952790733
T3 - IEEE International Conference on Automation Science and Engineering
SP - 545
EP - 550
BT - 2015 IEEE Conference on Automation Science and Engineering
PB - IEEE Computer Society
T2 - 11th IEEE International Conference on Automation Science and Engineering, CASE 2015
Y2 - 24 August 2015 through 28 August 2015
ER -