The Extension And Application Of Strand Space Model And Authentication Tests

Security protocol providing security services is the infrastructure of network security. With the rapid development of network,more and more cryptographic techniques are applied to security protocols in order to guarantee different levels of network security. However,different kinds of attacking techniques also appear ceaselessly,which bring forward much higher requirement of the analysis of security protocols.Formal method is a very effective instrtment to analyze security protocols.The appearance of strand space model and related theories promote the research of formal analysis of security protocols.However,the original strand space model and its authentication method have some drawbacks when analyzing some security protocols. Therefore,this thesis extends this model and its method according to the complex security protocols based on rich cryptographic primitives and the security protocol based on guessing attacks.As the original strand space model only consider poor cryptographic primitives,and thus cannot describe and analyze some cryptographic primitives in security protocols such as hash function and sign operation,so it is necessary to extend the strand space model. Since authentication test is based on the strand space model,some deficiencies in the strand space model also exist in authentication test.Thus,this thesis presents an extended authentication test method based on rich cryptographic primitives.The extended model and method can better describe and analyze the security of protocols,and applied in more entensive fields.When analyzing guessing attacks of security protocols,it needs to take the problem of imperfect cryptographic system into account.However,the original authentication test method assumes that the cryptographic system is perfect and relys on three basic hypotheses,so it can hardly find the guessing attacks existing in security protocols.This thesis proposes an extended authentication test method based on guessing attacks.Firstly, we define the guessing data and term to verify formally;and introduce them into the strand space model.Then we present verifying rules and verifying algorithms of terms;and introduce them into the authentication test method.The extended model and method can detect guessing attacks in security protocols.To validate the effectiveness of the extended strand space model and the extended authentication test method,we analyze SSL3.0 and TLS1.0 handshaking protocol with the proposed approach and verify the properties of authentication;and then analyze Yahalom-BAN and EXE protocol,finding guessing attacks exsiting in these protocols. Analyses results of these examples demonstrate correctness and effectiveness of the extended model and the extended test method.