Based On The Model Test Of The Formal Agreement

With the development of society, science and information technology, thecomputer network and the distributed system are more and more widely used, in whichthe cryptographic protocol is more and more widely focused on, their reliability andsafety requirements are becoming higher and higher, and any unforeseen errors willhave extremely serious consequences. Model checking is a way to ensure the protocolproved to be correct at the time of the design of the system, it is a kind of powerfulautomatic verification technolgy which can be found right or wrong in the design. Thisis a detection of the fundamental principles of the state migration system to representthe behavior of the system, to model or temporal logic to describe the nature of thesystem. If the system has the desired properties, and whether the State transition systemis a model of a formula, which converted to a mathematical formula. In this way, thematter of the safety of the cryptographic protocol turns to be a mathematical problem.By system model building, built to detect whether the nature of the expected meeting ofmodel, if not met, will render out examples to the contrary.This article mainly is the study of formal analysis to the protocol Leap series andits improved protocol Leap+A and Leap+B with the systerm of several verification toolsSpin and Avispa; Find out the attack to the protocol and existing holes with Promelaand HLPSL modeling; In the meantime, describle and testify the constructure, priciplesand operating processes of above main itms; Analyse, research and improve the projectof solving the existing problems.