Open AccessModeling and Verification of CBTC system security Communication protocol based on time Automaton
Author(s) -
Yan Zhao,
Tao He,
Qiang Li
Publication year - 2020
Publication title -
journal of physics. conference series
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.21
H-Index - 85
eISSN - 1742-6596
pISSN - 1742-6588
DOI - 10.1088/1742-6596/1601/6/062026
Subject(s) - computer science , protocol (science) , retransmission , key (lock) , process (computing) , computer network , computer security , operating system , medicine , alternative medicine , pathology , network packet
With the rapid growth of population and economy, passengers’ demand for urban rail transit is increasing, and it is difficult for single-line rail transit to meet passengers’ demand for rapid transfer. Therefore, the interconnection between urban rail lines has been the focus of development in recent years. Therefore, the secure communication between various devices is a very important link in the interconnection test. Chongqing Metro Line 10 is the first metro line to realize the interconnection based on the secure communication protocol, in which the specific parameter setting in the secure communication protocol is specified, so the method is needed to verify the security of the protocol. In this paper, the time automaton theory is adopted to carry out the corresponding modeling work for the two key safety key contents of the safety communication protocol in the railway, namely the protocol chain building process and the protocol retransmission process, and verify its security and timeliness. Finally, a test platform is built to test the communication function between the systems.