基于模型检测技术的网络安全协议形式化分析研究
形式化方法是提高软件系统，特别是safety-critical系统的安全性与可靠性的重要手段。模型检测是一种针对并发系统的自动分析与验证技术，以其简洁明了和自动化程度高而引人注目。密码协议目前已广泛应用于计算机网络与并发分布式系统中，但当密码协议并发执行时，其安全可靠性的论证仍是当前软件安全可靠性研究领域的一个世界难题。90年代以来，密码协议的形式化分析验证成为国际上的研究热点。本文提出了一种通用的安全协议模型及网络协议验证方法，出发点是将密码协议形式化，模型通用化，运用静态分析及惰性计算二种策略以解决状态爆炸问题。以TMN协议为例，通过SPIN/Promela具体在同一个模型下找出了针对其的五种攻击序列，并直观地通过信息序列图(Message Sequence Charts)具体地描述出其攻击轨迹。实验证明了此方法的有效性及通用性，可方便地用于其它网络安全协议验证。
网络安全协议 形式化方法 网络安全 协议验证 密码协议
肖美华 薛锦云
中科院软件所 江西师范大学计算机与信息工程学院
国内会议
南昌
中文
67-72
2004-10-28（万方平台首次上网日期，不代表论文的发表时间）