Paper Info
Title
Runtime Security Verification for Itinerary-Driven Mobile Agents
Abstract
We present a new approach to ensure the secure execution of itinerary-driven mobile agents, in which the specification of the navigational behavior of an agent is separated from the specification of its computational behavior. We empower each host with an access control policy so that the host will deny the access from an agent whose itinerary does not conform to the host's access control policy. A host uses model checking algorithms to check if the itinerary of the agent conforms to its access control policy written in mu-calculus, and if so, grant access permission. In order to address the state explosion problem for model checking itineraries, we propose an approach called model generation code. In this approach, instead of verifying the itinerary itself, a host actually checks the conservative models of a mobile agent. If a conservative model does not satisfy the host's access control policy, the mobile agent will provide refined models for further verification. Our preliminary results show that this is a practical and promising approach to ensure the secure execution of mobile agents
Year
DOI
Venue
2006
10.1109/DASC.2006.42
DASC
Keywords
Field
DocType
space probe,itinerary-driven mobile agents,model checking algorithms,runtime security verification,ubiquitous computing,state explosion problem,agent navigational behavior specification,pronounced use,mu-calculus,mobile agents,process algebra,formal specification,formal verification,model generation code,security of data,access control,mobile agent
Permission,Model checking,Computer security,Computer science,Mobile agent,Formal specification,Access control,Ubiquitous computing,Process calculus,Formal verification,Distributed computing
Conference
ISBN
Citations 
PageRank 
0-7695-2539-3
2
0.37
References 
Authors
9
3
Name
Order
Citations
PageRank
Zijiang Yang11308.83
Lu, Shiyong22022126.17
Ping Yang35210.62