RSSP-Ⅱ协议消息鉴定层的形式化描述及验证

协议流程的形式化描述及验证能够高效地保障协议的开发质量,对安全苛求系统尤为重要。针对铁路信号安全通信协议-Ⅱ(Railway Signal Safety Communication Protocol,RSSP-Ⅱ)中消息鉴定层(Message Authenticate Safety Layer,MASL)实现的会话密钥生成、对等实体认证、消息源认证等流程,建立有色Petri网(Colored Petri Net,CPN)模型,模型构造过程中执行有限步数的仿真,保障模型本身正确。利用模型检验方法,通过分析状态空间报告,验证了模型满足活性、家态性、公平性等基本行为属性,不存在冗余、死锁、活锁等设计缺陷。通过计算树逻辑(Computation Tree Logic,CTL)语句,验证了保密性、认证性等特定安全属性。结果表明,该模型满足文本设计规范中的功能安全性要求,为协议工程后续的协议实现、一致性检验奠定理论基础。