Research On State Space Reduction Technology For Security Protocol Based On Partial Order Reduction

This paper provides a brief introduction to the research situation of state space reduction technologies, makes in-depth research of partial order reduction technique based on the problem that there are many redundant nodes in state space of security protocols, improves performances of the automatical security protocols analysis system—SPFA (Security Protocol Formal Analyzer). Its main contents include:Firstly, because of the problem that the order of some transitions is inconsistent with the actual situation in the state space of security protocols, a reversal order reduction algorithm is proposed on the base of partial-order reduction technique. The algorithm deletes the states which violate the protocol specification, and reduces the size of state space. Theoretical analysis and experimental results show that the algorithm has reduced the reversal states in the sessions between honest agents, and decreased the time verifying security protocols.Secondly, because of the problem that there are some redundant nodes caused by trace-equivalent transitions, a trace-equivalent transitions reduction algorithm is proposed on the base of partial-order reduction technique. The algorithm judges the relations between messages send by honest agents and the intruder knowledges, and reduces the redundant successors of trace-equivalent transitions. Theoretical analysis and experimental results show that the algorithm has reduced the number of states in state space, and decreased the time analyzing security protocols.Thirdly, because the trace-equivalent transitions reduction algorithm permutes based on actions, leading to a limited effect of reduction, a stuttering action reduction algorithm is proposed on the base of partial-order reduction technique. The algorithm consideres the action sequences in the same session as a stuttering action, judges the relations between messages send by honest agents and the intruder knowledges, and reduces the redundant successors of trace-equivalent stuttering transitions. Theoretical analysis and experimental results show that the algorithm is better than the trace-equivalent transitions reduction algorithm, and decreased the time analyzing security protocols.Finally, improvements are made for the automatical security protocol analysis system—SPFA based on the above algorithms, and conclusions of whole thesis are summed up and the future research is proposed.