Formal modeling and verification of secure mobile agent systems

Mingyue Jiang, Zuohua Ding, Mengchu Zhou, Yuan Zhou

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publication2015 IEEE Conference on Automation Science and Engineering
Subtitle of host publicationAutomation for a Sustainable Future, CASE 2015
PublisherIEEE Computer Society
Pages545-550
Number of pages6
ISBN (Electronic)9781467381833
DOIs
StatePublished - Oct 7 2015
Event11th IEEE International Conference on Automation Science and Engineering, CASE 2015 - Gothenburg, Sweden
Duration: Aug 24 2015Aug 28 2015

Publication series

NameIEEE International Conference on Automation Science and Engineering
Volume2015-October
ISSN (Print)2161-8070
ISSN (Electronic)2161-8089

Other

Other11th IEEE International Conference on Automation Science and Engineering, CASE 2015
CountrySweden
CityGothenburg
Period8/24/158/28/15

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Formal modeling and verification of secure mobile agent systems'. Together they form a unique fingerprint.

Cite this