Formally modeling and analyzing a secure mobile agent finder

Mobile agents provide a powerful and flexible paradigm for the development of autonomic computing systems. However, due to the security concern, mobile agents are not popularly used for real-world systems. In this paper, we define a security framework that can effectively protect mobile agents and agent systems from intruder attacking. In the framework, a mobile agent finder, which is extended with a registration protocol, is used to authenticate and authorize agent systems, incoming messages, and agents. We formally model the secure mobile agent finder using predicate transition nets, and analyze the models using model checking tool Spin. The results help us to develop high confidence applications using mobile agents. In addition, the modeling and analysis approach can be easily extended to develop other complex software systems.