中文摘要：

提出一种多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.