Formal Modelling and Analysis of a Secure Mobile Agent System

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

jsp.display-item.identifier=請使用永久網址來引用或連結此文件: http://asiair.asia.edu.tw/ir/handle/310904400/4763

题名:	Formal Modelling and Analysis of a Secure Mobile Agent System
作者:	Jeffrey J. P. Tsai;L. Ma
日期:	2008-01
上传时间:	2009-12-02 01:04:05 (UTC+0)
出版者:	Asia University
摘要:	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.
關聯:	IEEE Transactions on Systems, Man, Cybernetics, Part A 38(1):180-196
显示于类别:	[生物資訊與醫學工程學系 ] 期刊論文

文件中的档案:

档案	描述	大小	格式	浏览次数
		0Kb	Unknown	587	检视/开启
310904400-4763.doc		34Kb	Microsoft Word	242	检视/开启

在ASIAIR中所有的数据项都受到原著作权保护.

数据加载中.....