Research On Security Analysis Of IEEE 802.1AS Protocol Using Colored Petri Nets

In the situation of Industrial Internet,the interconnection and intercommunication between various elements are put forward higher requirement in the industrial control network,and the problem that some industrial Ethernet protocol standards are inconsistent and incompatible with each other is increasingly exposed.Toward this aim,the IEEE 802 task group has developed a series of Time-Sensitive Networking standards to establish a set of universal time deterministic mechanisms for industrial Ethernet protocols.As one of the most important protocols in these standards,IEEE 802.1AS protocol is designed without an inherent security mechanism and may present great security threats.Therefore,this thesis deeply studies the security problem of IEEE 802.1AS.This thesis deeply studies the security analysis issues of IEEE 802.1AS from three aspects.Firstly,in order to quantitatively analyze the security of the synchronization protocol,in view of the poor practicability and insufficient scalability of the current IEEE802.1AS protocol model analysis framework,a formal model of IEEE 802.1AS protocol is proposed based on the Colored Petri Net theory and the CPN Tools.The validity and practicability of the proposed model are verified by state space results and simulation results analysis.Secondly,based on the qualitative analysis of attack behavior against the protocol,an attacker model of the IEEE 802.1AS protocol is established.On the basis,the security of the protocol under the attack state is evaluated and verified quantitatively.The results indicate that the attack actions of malicious timestamp modification,splitting and combination,eavesdropping and replay are successfully executed.Finally,in order to improve the security of Time-Sensitive Networks,in view of the lack of protection mechanism of IEEE 802.1AS,the suitable method is investigated to improve the security of the protocol.Based on the security evaluation results,an IEEE 802.1AS-Sec security synchronization mechanism based on MACsec is designed under the constraint of the synchronization performance.On the basis of the formal model,the functional property and security property of the IEEE 802.1AS-Sec mechanism are analyzed and verified.As is shown in the analysis results,on the one hand,the strong connectivity,reachability and liveness meet the original protocol specifications,and the synchronization deviation meets the original protocol constraints,which indicates that the synchronization function of IEEE802.1AS-Sec is valid.On the other hand,the dead transitions and dead markings show that none of the attack actions are successfully executed,and the slave clock is synchronized correctly,which improved the security property of the original protocol.Aiming at the security evaluation and improvement of IEEE 802.1AS,the protocol behavior model and attacker model based on the Colored Petri Net are proposed in this thesis,which realize the effective evaluation of the protocol security property.On this basis,a MACsec-based IEEE 802.1AS-Sec security synchronization mechanism is proposed,which can fulfill safe and reliable time synchronization process between master and slave clocks.