中文会议： 广西计算机学会2008年年会论文集

会议日期： 2008-09-01

会议地点： 广西北海

主办单位： 中国计算机学会

作　　者： ; ; ;

机构地区： 桂林电子科技大学计算机科学与工程学院

出　　处： 《广西计算机学会2008年年会》

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

关 键 词： 模型检测 网络规模 网络协议 协议分析

分 类 号： [TN]

领　　域： [电子电信]