基于协同侦测技术的移动主体模型验证策略研究

Model Checking Strategy of Mobile Agent Based on Technology of Collaborative Detection

移动主体模型可以实现协同侦测网络攻击和区域预警的功能;它利用元组空间(TUPLE SPACE)构建移动主体服务集群(RMAS CMAS)网络结构及侦测ARP攻击的主体.为了证明该模型逻辑的有效性,验证策略设计了可以分析ARP攻击数据包从初始组态到终结组态的动态空间树;利用空间树嵌套演算推理协同侦测系统的组态迁移过程,分析模块的动态移动重组以及消息的并行传递机制.对模型验证策略的研究可以消除在模型设计阶段出现的冗余组态,提高移动系统的设计水平.

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 re-compose 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.