多agent逻辑程序及其在协议验证中的应用  

Multi-agent Logic Program and its Application to Protocol Verification

作　　者：周勇[1] 朱梧[1] 

机构地区：[1]南京航空航天大学信息科学与技术学院,江苏南京210016

出　　处：《小型微型计算机系统》2007年第1期54-57,共4页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60573070)资助.

摘　　要：提出一种多agent逻辑程序,每个agent具有一个相信算子,讨论了其不动点语义和操作语义,证明了两种语义之间的等价性.提出了一种基于多agent逻辑程序的协议验证方法,以一种多方非否认安全协议为例,对该协议进行了形式化描述,验证了其具有不可否认性.A multi-agent logic program with several modal operators is presented. Each operator represents an agent＇s belief. The declarative semantics based on the fix-point theory and the procedural semantics for the multi-agent logic program are given. The equivalence of the above two semantics is proved. Within the new logic program framework, a method for verifying the security protocols is proposed. As an example, an multi-party security protocol is represented formally with the multi-agent logic program and is proved having the property of non-repudiation.

关 键 词：逻辑程序 安全协议 不可否认性 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]