Kaman协议是移动Ad Hoc网络安全认证机制,然而,协议设计者未对该协议的安全性作严格的形式化分析.协议复合逻辑PCL是验证协议安全属性的形式化方法,PCL逻辑能够简化协议安全分析过程.本文在协议复合逻辑PCL中描述Kaman协议并分析Kaman协议的安全属性,证明Kaman协议能够实现其安全目标.%Kaman is security authentication scheme of mobile Ad Hoc networks. However, the author of Kaman didn't verify security of the protocol by using formal method. Protocol Composition Logic (PCL) is formal verification logic of security protocol. This logic can simplify the process of protocol verification. This paper describes Kaman and analyzes its security properties in PCL. It is proved that Kaman can implement its security aim.
展开▼
