ASPASYA stands for Heuristic-ASPASyA and extends ASPASyA. ASPASYA is a conventional model checker for security protocols verification. H-ASPASYA incorpoartes heurisctic techniques into ASPASyA and is therefore a directed model checker. The protocols to be inputted to H-ASPASyA are formalized in cIP (a process calculus) and properties to be verified are specified in PL (Protocol Logic). The theroretical foundation of H-ASPASyA are based on |
||||
|
||||
H-ASPASyA can search the state space using three different heuristics, called H1, H2, and H3.
|
||||
Note that H-ASPASyA requires Linux and 32 bit machines. The tool can give some problems on 64 bits machines. |