• Nadim Kobeissi's avatar
    Phases (experimental) · 221b85db
    Nadim Kobeissi authored
    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
    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.
attackerstate.go 3.3 KB