[Verifpal] New Feature: Phases

Nadim Kobeissi nadim at symbolic.software
Wed Jan 29 18:53:30 CET 2020

Hello everyone,

Verifpal 0.9.17 brings an exciting new feature, phases, 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


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

In the above example, the attacker won't be able to learn a2 until the
execution of everything that occurred 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.

I'm excited to see what all of you will do with phases!

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200129/60ebf086/attachment.htm>

More information about the Verifpal mailing list