基于通信顺序进程方法的RSSP-II通信协议安全性分析

摘要

近年来，工业控制系统网络安全问题逐渐显现。铁路信号系统作为工业控制系统的一种特殊应用，除了保证系统设备可靠、功能完整之外，承载信息传输的网络安全问题也是迫切需要关注和解决的问题。文章分析了关乎铁路信号系统安全的RSSP-II通信协议，引入了形式化建模中的通信顺序进程方法，对通信协议的密钥服务流程和对等实体认证过程这两个关键内容进行了相应的建模研究工作。文章采用模型检测工具Casper-FDR对协议安全属性中的保密性、认证性进行了验证，分析了对应的验证结果。实验结果表明，访问状态数、转换状态数、状态转换时间参数均正常，反例个数为0，验证了 RSSP-II 在密钥服务和对等实体认证过程的安全性。