VerSecTis - An Agent based Model Checker for Security Protocols

We present VerSecTis-a new experimental tool for the verification of timed security protocols' (TSP) modelled by Timed Interpreted Systems (TIS). In addition to the TSP's time-independent properties, our tool can also examine the time dependencies of the TSP's executions on which their security depends. The verification method consists of a new TSPs' modelling method and a translation of the reachability problem for TIS to the Satisfiability Modulo Theories problem. We also deliver nineteen TSPs to verify, and we plan to expand the tool with further protocols.