| ¡¡ | Chinese Journal of Computers Full Text |
| Title | Model Checking Strategy of Mobile Agent Based on Technology of Collaborative Detection |
| Authors | LI Hai-Ying CHENG Hao YE Wei-Quan ZHUANG Zhen-Quan |
| Address | (Department of Electronic Science and Technology, University of Science and Technology of China, Hefei 230026) |
| Year | 2005 |
| Issue | No.5(921¡ª927) |
| Abstract & Background | The mobile agent model achieves the goal of collaborative detection of network intrusion when attacks occur in a vast region.The architecture of service cluster(RMAS-CMAS) is described as well as mobile agent for detecting ARP attack via the concept of Tuple-Space. To check the effectiveness of the system detection logic, model checking strategy enables us to build dynamic spaces tree from initial configuration to terminative configuration which is used to analyze packets of ARP attack.Transference of collaborative detection system configurations, dynamic recompose of modules and message parallel transfer mechanism are ratiocinated by calculation of nested spaces tree. Study of model checking strategy can eliminate the redundance configurations which exist in the model design and help to improve quality of the design of mobile system. keywords mobile agent£» tuple-space£» model checking£» transference of configurations background The research on collaborative detection of network intrusion is supported by the National Natural Science Foundation of China under grant Noª±90104030. Its purpose is to improve validity of mobile detection agent. The research group has developed a practice system to analyze packets of ARP attack, and it can alert administrator about significant security events happening on workstations and servers .This paper is about how to apply logic model design to establish the architecture of detection system. |