Research On Automatic Analysis For Multi-Protocol Attacks On Security Protocols

In recent years, many formal analysis methods for security protocols have been proposed and they have been proved to be very useful.Nevertheless, these methods generally deal with one protocol system without tak ing into account other protocols running in the same environment of the protocol to verify. However, many computer systems employ different security protocols to provide protection for different kinds of services or applications, and they support more than one protocol for the same service or application to guarantee a higher compatibility. These environments are called multi-protocol systems. In such systems, the violation can arise from the use of the same cryptographic keys in different protocols. And each protocol may interact in a harmful way with the other protocols.Therefore, there is an urgent need for a method capable of protocol security analysis in multi-protocol systems. On the foundation of studying multi-protocol security theory and technology, rearch on modeling multi-protocol systems and automatic verification for multiprotocol attacks on security protocols is carried out. The main works are as follows:(1) Traditional formal analysis methods are not taking into account other protocols running in the same environment of the protocol to verify. To solve this problem, a new multi-protocol analysis model is given. The analysis model is based on the events and relationship between the events.In the analysis model, security protocols are modeling in static protocol describing and dynamic protocol executing aspects. Message items, protocol events and protocol describing rules are defined in the security protocol description, with which the input language for the automatic verification tool is provided. Run items, run events and adversary events are defined in the protocol execution description. And the event relational model is defined, by which the state space of multi-protocol concurrent execution is defined. Finally, secrecy and authentication properties are formally defined based on protocol traces.(2) Based on multi-protocol analysis model and the state and goal binding mechanism of Athena, an automated verification method for multi-protocol attacks is proposed. The goal binding method of Athena is limited to a single protocol.Therefore, according to the characteristics of multi-protocol concurrent execution, a new goal binding and next state generating methods are given. The adversary can intercept messages from one protocol and insert messages generated by it to another protocol, by which possible multi-protocol attacks are effectively detected. The corresponding attack traces are found exactly. The decryption sequence concept is utilized to deal with nestedly encrypted messages in verification algorithm, with which the search space is reduced.(3) A prototype system of automatic verification for multi-protocol attacks is designed and implemented. As the proposed verification algorithm is utilized to verify the security of multi-protocol systems, in order to get accurate results as far as possible, searching for more states is needed. According to the characteristics of state representations and search algorithm, a mechanism is designed in the verification algorithm implementation, with which a single global state is utilized to implement the state search algorithm. The storage of the system is greatly reduced with the mechanism. The test results show that the system can implement effective automatic verification for multi-protocol attacks.