基于SPIN的协议分析技术研究

摘要

随着网络规模不断扩大,协议已广泛应用在各种分布式的网络环境中.使用形式化的分析方法有助于发现协议设计中的缺陷,保障分布式应用的质量。而模型检测技术作为一种形式化的分析方法,支持自动化的推理技术,能根据逻辑公式自动的验证协议的属性,发现缺陷.本文给出了基于模型检测技术的协议分析框架，然后用模型检测工具SPIN[1]在该框架下分析了SAS［2］协议，验证了协议的安全属性和数据流的功能属性，发展了数据流的一个缺陷；分析了NS[3]协议的机密性和论证性，给出了该协议的路径。