摘要
形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段。本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约。运用此技术和模型检测器SPIN找到了两种针对TMN协议的攻击,证明了此方法的实用性,可方便地用于其它网络安全协议验证。
Formal method has been advocated as an important means of improving the safety and reliability of software systems, especial those which are safety-critical. This paper proposes a new simple trace semantics that can be used to specify security properties, this technique supports a protocol designer to provide formal analysis of the security properties. It illustrates the utility of this technique by exposing two attacks on the well studied protocol TMN.
出处
《计算机与现代化》
2007年第2期107-109,共3页
Computer and Modernization
