信息网络安全

信息网络安全 ›› 2016, Vol. 16 ›› Issue (7): 7-8.doi: 10.3969/j.issn.1671-1122.2016.07.002

• • 上一篇    下一篇

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

陆德彪, 和晟姣, 王剑   

  1. 北京交通大学电子信息工程学院,北京100044
  • 收稿日期:2016-06-01 出版日期:2016-07-20 发布日期:2020-05-13
  • 作者简介:

    作者简介： 陆德彪（1986—）,男,江苏,副教授,博士,主要研究方向为列控系统安全;和晟姣（1992—）,女,云南,硕士研究生,主要研究方向为列控系统通信安全协议;王剑（1978—）,男,山西,教授,博士,主要研究方向为列控系统。

  • 基金资助:
    国家自然科学基金 [61490705];中国铁路总公司科技研究开发计划 [2014X003-J、2016X008-B]

RSSP-II Protocol Security Analysis Based on Communicating Sequential Process Method

Debiao LU, Shengjiao HE, Jian WANG   

  1. College of Electric Information Engineering, Beijing Jiaotong University,Beijing 100044, China
  • Received:2016-06-01 Online:2016-07-20 Published:2020-05-13

RichHTML

8

PDF (PC)

476

摘要：

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

关键词: RSSP-II, 通信协议, 安全性分析, 通信顺序进程方法

Abstract:

Nowadays, the increasing number of cyber security events in industry control system (ICS) are emerged. Railway Signalling System as a specific application of the industrial control system, including reliability and completeness, the transmission network security is also the stringent task to be focused on. This paper analysed the RSSP-II protocol as the security protocol for railway signalling system, the Communication Sequential Processes (CSP) method was introduced. CSP is one of the model checking method, this method using discrete event to describe the system, the process and its environment were described by algebraic operations in formal language. Each CSP process can be converted into equivalent state. The processes of the key service and peer entity authenticating are analysed through CSP. At last the model checking tool Casper-FDR was applied to verify the confidentiality and authenticity properties of the protocol. The result showed that the parameters are acceptable, and the reverse item number is 0, thus verified RSSP-II in key service and peer entity authenticating.

Key words: RSSP-II, communication protocol, security analysis, communicating sequential process method

中图分类号: