Formal Security Evaluation And Improvement Of IPP Protocol Based On HCPN Model Detection Method

Internet Printing Protocol(IPP)is one of the most important printing protocols.The protocol claims that its security components can guarantee confidentiality,integrity and non-repudiation.There are many methods in the academic circle to verify the security properties of the protocol,among which the model checking method is a widely used method.Some researchers use the Scyther to verify the security of the protocol,but it completely encapsulates the implementation details of the adversary model,and it is impossible to understand the details of the behavior of each participant during the operation of the protocol.In contrast,CPN Tools can easily observe the specific actions of each participating entity with the help of the coloring Petri-nets theory,which helps researchers quickly locate protocol security flaws.Therefore,this paper uses the CPN Tools to study the Internet Printing Protocol’s zero-round-trip-time authentication mechanism under pre-shared key mode.First of all,this paper models the standard protocol authentication process,and extracts the key states that affect the security for breakpoint testing.After ensuring the consistency between the model and the standard protocol,the improved DolevYao adversary model is introduced to verify protocol security assessment.By limiting the number of session participants and the number of concurrent sessions,using state reduction technology to cut unnecessary search paths,and improving the attack model selective attack sequence,etc.,the problem of state space explosion in the model detection method is effectively avoided,and a large amount of invalid data is avoided.After using the CPN Tools to complete the experiment,the simulated attack result shows that: the standard protocol authentication process can resist the adversary’s tampering and forgery attacks on user information,but it cannot resist the adversary’s replay attack on the user’s early data.Then,further analysis of the behavior of the protocol entity reveals that the unsafe factor lies in the fact that the server lacks the necessary identification means to judge whether the data is replayed by the adversary after the server decrypts the early data.In view of the above defects,this paper enhances the ability of the server to identify replay attacks by introducing random number signatures,realize the improvement of the original protocol,and introduce the improved Dolev-Yao attack model again to analyze and verify the security properties of the new scheme.The simulated attack results show that compared with the original scheme,the improved scheme can indeed resist the adversary’s replay attack.The improvement scheme proposed in this paper enhances the server’s ability to perceive authentication replay attacks at the small cost of adding a signature on the client side,and can quickly terminate the illegal user authentication request process and minimize potential risks.The research method used in this paper also has reference significance for the security analysis of other communication protocols.