Formal Modelling and Analysis of a Secure Mobile Agent System

ASIA unversity > 資訊學院 > 生物資訊與醫學工程學系 > 期刊論文 > Item 310904400/4763

Please use this identifier to cite or link to this item: http://asiair.asia.edu.tw/ir/handle/310904400/4763

Title:	Formal Modelling and Analysis of a Secure Mobile Agent System
Authors:	Jeffrey J. P. Tsai;L. Ma
Date:	2008-01
Issue Date:	2009-12-02 01:04:05 (UTC+0)
Publisher:	Asia University
Abstract:	As a recently emerging distributed computing paradigm, mobile-agent technology attracts great interests because of its salient merits. However, it also brings significant security concerns, among which the security problems between a mobile agent and its platforms are of primary importance. While protecting a platform (platform or host security) can benefit from the security measures in a traditional client-server system, protecting a mobile agent (mobile-agent or code security) has not been met in traditional client-server systems and is a new area emerging with mobile-agent technology. Mobile-agent security is also believed to be the most difficult in the security areas of a mobile-agent system. Several methods are proposed to provide protection or detection mechanisms for mobile-agent security. However, many of them either lack an intuitive formal approach to formally model and analyze the system or lack security consideration for mobility - the most distinct characteristic of a mobile agent. In this paper, we extended the original elementary object system (EOS), which applies object-oriented technology to Petri nets, in several aspects because the original EOS cannot fully support the features of mobile-agent system and security modeling. Based on the extended EOS (EEOS), we developed a formal model for a generic secure mobile-agent system. This model supports not only strong mobility but also secure mobility of a mobile agent. Mutual authentication between a mobile agent and its hosting platform is accomplished in this model. Meanwhile, a security mechanism is presented for the detection of malicious platform attacks to mobile-agent code or execution flow during the mobile-agent execution. Using an intuitively graphical formal method to model, simulate, and analyze a secure mobile-agent system distinguishes this paper from other works on mobile-agent security. This paper also introduces how to translate our EEOS model to a colored Petri net (CPN) model and pres- - ents the simulation of a sample mobile-agent system model in Design/CPN. Different from the mathematical or theorem-proving analysis methods used by other mobile-agent system and mobility models, we used simulation-based analysis to verify several characteristics including boundedness, liveness, concurrence, and security of the system. Compared with other analysis methods, simulation-based analysis is generally more intuitive and more widely used in industry to solve real problems.
Relation:	IEEE Transactions on Systems, Man, Cybernetics, Part A 38(1):180-196
Appears in Collections:	[生物資訊與醫學工程學系 ] 期刊論文

Files in This Item:

File	Description	Size	Format
		0Kb	Unknown	587	View/Open
310904400-4763.doc		34Kb	Microsoft Word	242	View/Open

Loading...