[Verifpal] New feature: Queries as preconditions

Nadim Kobeissi nadim at symbolic.software
Tue Feb 4 15:53:29 CET 2020

Hello everyone,

Verifpal brings an interesting new feature, which allows us to
use queries as preconditions for message events:

Imagine that we want to check, in the following model, if Alice will
only send some message to Alice if it has first authenticated it from

principal Bob[
    knows private psk
    generates m
    e = ENC(psk, m)
    h = MAC(psk, e)
Bob -> Alice: e, h
principal Alice[
    knows private psk
    _ = ASSERT(MAC(psk, e), h)?
    m2 = DEC(psk, e)
Alice -> Carol: [m2]
principal Carol[]

This can now be accomplished using the following query:

    authentication? Bob -> Alice: e[
precondition[Alice -> Carol: m2]

The above query essentially expresses: "The event of Carol receiving m2 from
Alice shall only occur if Alice has previously received and
authenticated an encryption of m2 as coming from Bob."

This new syntax allows us to obtain some insight on the communication of
m2 based on the result of other queries, and to also link the
authentication of that communication on the authentication of other
values, which can be important when m2 is being communicated as a
guarded constant, which is the case in the above.

A new class of Verifpal language syntax is introduced here, called
"query options". Right now, "precondition" is the only query option, but
others may be added later, resulting in queries that look like this:

    confidentiality? x[
precondition[Alice -> Carol: x2]
precondition[Alice -> Carol: x3]

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/20200204/bef3208c/attachment.htm>

More information about the Verifpal mailing list