The Formal Description Of The Property With Parameters And Prove

“State space explosion” has been an inevitable problem in the field of verifying. In the process of verification, we found that many properties with parameters that can be summarized. For example, the length of the path, the scope of the random number, the number of state space, communication steps, etc. Using the characteristics of induction we can combine the model checking techniques and the method of inductive proof. In this paper, we choose two cases about the verification of properties which can be summarized to study. Case one relates to the logic verification in the field of integrated circuit, the terminal property has the feature of induction according to the length of the path. In this paper, we put forward the terminal model checking algorithm(TMC) based on the theories which have been proposed by generalized symbolic trajectory evaluation(GSTE). TMC can avoid some redundant calculations and reduce the complexity of calculations by using the nature of induction. In the experiment of verifying a hardware circuit Round-Robin arbiter, the result shows that the time cost by the enumeration method is 14.3? with TMC in the case. On the other hand, TMC can solve some limitations in SMC which proposed by GSTE. In the end, we prove that TMC is sound and complete.Second case involves the research about the security and privacy in RFID system. With the wide application of RFID technology, more and more people pay attention to the privacy for consumer. Design authentication protocol or scheme is an effective means of protection. At the same time, the verification of protocol cannot be ignored. Although many formal verification models have been existed, each method has its own shortcomings. This paper mainly describes the method of random graph and induction. Random graph can analyzed RFID protocols in qualitative. The method which called random graph is more intuitive. On the other hand, the complexity of computational will be increase by exponential if the range of random value is large. Inductive method designed(r,s,t)-privacy experiment which based on cryptography IND-CPA security standards.The range of random number and the steps of communication have no effect on inductive method. This paper designed the(r,s,t)-security experiment which based on the experiment of(r,s,t)-privacy in RFID system. In the end, we analyzed the protocol of OSK and VOSK. We conclude that OSK neither meet the(r,s,t)-privacy nor(r,s,t)-security. VOSK does not meet the(r,s,t)-privacy, but VOSK satisfies the(r,s,t)-security.OSK protocol can not resist denial of service attacks, nor can replay attack. VOSK protocol can not resist denial of service attacks, but can resist replay attack.