H-ASPASyA

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

1. A Coordination-based Methodology for Security Protocol Verification
2. Heuristic Methods for Security Protocol Verification

H-ASPASyA can search the state space using three different heuristics, called H1, H2, and H3.

  1. Download H1-ASPASyA
  2. Download H2_ASPASyA
  3. Download H3_AsPASyA

Note that H-ASPASyA requires Linux and 32 bit machines. The tool can give some problems on 64 bits machines.