TSPVT: An efficient verification tool for time sensitive security protocols

Automatical verification of time sensitive protocols is a difficult research topic in formal analyses, with the key problem being how to simply and efficiently check time constraints led by time stamps. TSPVT, which automatically verifies time sensitive protocols, was developed from the SPVT(security protocol verifying tool) in the Objective Caml language. TSPVT takes time sensitive protocols in an extended π-like calculus model with time events as its input model, then translates the π-like calculus model into a Horn logic model P extended by the time constraint system. The Horn logic model P is composed of a set of rules for honest participants as well as another set of rules for attackers. In the verification period, TSPVT computes the fix point of P when the tool needs to process the X-resolution among rules within the time constraint system and then verifies the authentication of the protocol based on the fixed point. A simplified description of the verification process using TSPVT is given in detail using the Denning-Sacco protocol as an example, with the results showing the validity of the verifier.