Abstract: Otway-Rees protocol is to complete the two-way authentication between the initiator and the responder,and to distri-bute the session key generated by the server.The feature of this protocol is simple and practical.It does not use complicated synchronous clock mechanism or double encryption,and provides good timeliness with only a small amount of information.This protocol allows individual communications to be authenticated through a network,while also preventing replay attacks and eavesdropping,as well as modifying detection.The analysis of security protocols is a key issue that cannot be avoided in the information age.Formal method,which is based on strict mathematical and mechanical methods,is an important method to improve and ensure the quality of computing system.Its model,technology and tools have become an important carrier of computing thinking.The formal method can accurately reveal all kinds of logic rules,make corresponding logic rules,and make all kinds of theoretical systems more rigorous.Formal method is a mathematical description of what a program does,a description of the function of a program written in a formal language with precise semantics.It is not only the starting point of designing and programming,but also the basis of verifying whether a program is correct,so as to improve the reliability and robustness of the design.By abstracting the Otway-Rees protocol,we can get the abstract model.On this basis,the formal description based on process algebra is gi-ven and the formal verification is carried out.The verification results show that the parallel system in the form of this protocol shows the expected external behavior.

Key words: Formalization, Otway-Rees, Process algebra, Protocol verification, Security protoco