AIF-Omega

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:

Revocation of keys
Webservers that maintain a database of orders
Security tokens like hardware security modules

AIF-Omega consists of two things:

A specification language:
- You can model a number of sets (or databases): for instance
  db(Server,User,{valid,revoked})
  to model one database for every Server, that stores for every User both the currently valid and the currently revoked keys.
- Each of these sets can contain any number of elements
- In contrast to the previous AIF (without the omega), parameters like Server and User can be infinite sets of participants. The only restriction is that the members of each infinite family must be disjoint.
- You can specify transitions that create fresh elements, add them to any sets, remove them from any sets, check whether an element is in a set or not, or pick any element from a set.
The corresponding verification tool: AIF-Omega computes an over-approximation of the set of reachable states, yielding a set of Horn clauses that can be solved with ProVerif or SPASS.

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

AIF-Omega v.1.2 with source code and examples.
Set-Pi v.0.1.0 The sister tool of AIF with a process calculus interface.
AIF-Omega v.1.1 including source code, executable for Mac, and examples.
AIF-Omega v.1.0

Contact

	Sebastian Mödersheim DTU Informatics Richard Petersens Plads, Building 324, Room 160 DK-2800 Kgs. Lyngby, Denmark Email: samo@dtu.dk 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 Email: brun@itu.dk

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