GitLab

Phases are an exciting new feature that allows Verifpal to reliably
model post-compromise security properties such as forward secrecy or
future secrecy.

When modeling with an active attacker, a new phase can be declared thus:

```
principal Alice[...]
principal Bob [...]
Bob -> Alice: b1

phase[1]

principal Alice[...]
Alice -> Bob: a2
```

In the above example, the attacker won't be able to learn a2 until the
execution of everything that occured in phase 0 (the initial phase of
any model) is concluded. Furthermore, the attacker can only manipulate
a2 within the confines of the phases in which it is communicated. That
is to say, the attacker will have knowledge of b1 when doing analysis
in phase 1, but won't be able to manipulate b1 in phase 1. The attacker
won't have knowledge of a2 during phase 0, but will be able to
manipulate b1 in phase 0.

Values are learned at the earliest phase in which they are communicated,
and can only be manipulated within phases in which they are
communicated, which can be more than one phase since Alice can for
example send a2 later to Carol, to Damian...

Importantly, values derived from mutations of b1 in phase 0 cannot be
used to construct new values in phase 1.

A pertinent example of how phases can be used has been added to the
signal.vp and signal_small.vp models, where phases are used to model
forward secrecy in the Signal Protocol for exchanges involving three
messages and one message respectively.

Phases support was already added to the Visual Studio Code and Vim
extensions in a previous commit (ad26547f) and those extensions will be
pushed onto their respective marketplaces shortly. The Verifpal User
Manual will also be updated.