Improvement of Key Management Mechanism for RSSP-II and Its Formal Modeling and Verification

摘要

As the RSSP-II protocol has hidden dangers in the management of transport keys and authentication keys, in order to strengthen the safety of the key management of RSSP-II and make the communication between the safety-related entities of the train control system safer and more reliable, an improved scheme is presented in this paper. This scheme adopted the Raft algorithm combined with elliptic curve cryptography and time-triggered mechanism to get all safety-related devices in a certain area of the system to update and consistently share an authentication key in a way that works without key management center and reduces human intervention. Then, the specification language TLA+ is used to model the consensus process, and the TLC model checker is used to verify the properties of the model. The results show that the scheme is feasible, safe and can simultaneously avoid the deadlock problem. At last, the safety analysis shows that the scheme is safe and meets EN50159 standard.