AIF-Omega is an abstraction based verification tool for security protocols where participants have state that is beyond a single session, e.g. to model:
AIF-Omega consists of two things:

The Method

Sebastian Mödersheim and Alessandro Bruni. AIF-omega: Set-Based Protocol Abstraction with Countable Families. POST 2016. Preprint available.

Download AIF-Omega and Set-Pi


Sebastian Mödersheim
DTU Informatics
Richard Petersens Plads, Building 324, Room 160
DK-2800 Kgs. Lyngby, Denmark
Phone: +45 45 25 35 97

Alessandro Bruni
IT University of Copenhagen
Programming Logic and Semantics
Rued Langgaards Vej 7, Room 4C15
DK-2300 Copenhagen S, Denmark

The classic AIF Framework (Set-based abstraction)

  • Version 2010b (including source code and SEVECOM example).
  • Relevant papers: Abstraction by Set-Membership, Verifying SeVeCom Using Set-based Abstraction