论文研究一种新的安全通信协议安全性验证框架.pdf

将CRA应用于安全通信协议的层次结构分析领域，采用LTS对协议的层次结构进行行为建模，并利用映像LTS描述协议行为的安全属性。采用接口技术对行为模型和属性模型进行组合约简，通过观察组合模型中错误状态是否可达来判定协议是否安全，为安全通信协议的安全性验证提供了一种新的框架。最后基于该框架给出FSFB/2(fail safe field bus/2)协议的安全性验证，表明该框架的可用性。