[Verifpal] [ANNOUNCE] Verifpal 0.14.0

Symbolic Software Drone drone at drone.symbolic.software
Tue Jun 2 19:47:49 CEST 2020


Hello,

Verifpal 0.14.0 is now available. Verifpal updates bring new features, performance improvements and/or bug fixes.

-------------------------------
1. Release Notes
-------------------------------
Verifpal 0.14.0 is a major release that brings a variety of exciting improvements and additions:

*** Verifpal Reaches Beta Software Stage ***

Verifpal now benefits from a higher level of assurance due to the formalization of its syntax, semantics and analysis methodology, both by hand and using the Coq theorem prover. However, it remains classified as beta software due to its relatively young age, especially when compared to similar tools, such as ProVerif, that have been in development for more than twenty years.

Aside from the soundness and Coq translation improvements, Verifpal has also seen an increasingly large and exciting feature set, including full Visual Studio Code integration (https://www.youtube.com/watch?v=it_hJkVU-UA), translation to ProVerif and soon also translation to full prototype implementations in Go.

I am still very proud to announce that Verifpal is now in its beta stage, with this release bolstering the reliability of its analysis, its Coq translation and more. Verifpal is now almost one year old (!!!) and it's incredibly exciting to arrive to this milestone, which would not have been possible without the help of more than a dozen individuals. In no particular order: Loup Vaillant David, Bruno Blanchet, Mike, Jason Donenfeld, Jean-Philippe Aumasson, Georgio Nicolas, Mukesh Tiwari, Benjamin Lipp, Sasha Lapiha, and many many more.

We'd like to especially thank our sponsors, NLnet and Cure53, for their support.

*** Coq Translation Major Improvements ***

The semantics, lemmas and proofs for all primitivies in the Coq translation component of Verifpal have been radically deepened and improved, with further improvements to come in the future, including support for active attacker analysis in Coq. Currently, only passive attacker analysis is supported. This was accomplished via the Herculean work of Georgio Nicolas and Mukesh Tiwari.

*** Fix a Class of False Positives ***

A class of false positives, initially reported in Verifpal by Max Krohn (Keybase/Zoom) has been fixed. 

Consider the following two scenarios:

```
// Example A
Alice -> Bob: [ga_enc]
principal Bob[
    _ = SIGNVERIF(ga, gea, siga)?
    ga_dec = AEAD_DEC(gea^eb, ga_enc, c1)?
    _ = ASSERT(ga, ga_dec)?
]
principal Alice[
    generates sesskey
    enc_sesskey = AEAD_ENC(kb, sesskey, c2)
]
Alice -> Bob: enc_sesskey
```

```
// Example B
Alice -> Bob: [ga_enc]
principal Alice[
    generates sesskey
    enc_sesskey = AEAD_ENC(kb, sesskey, c2)
]
principal Bob[
    _ = SIGNVERIF(ga, gea, siga)?
    ga_dec = AEAD_DEC(gea^eb, ga_enc, c1)?
    _ = ASSERT(ga, ga_dec)?
]
Alice -> Bob: enc_sesskey
```

Previously, depending on the rest of the model, Verifpal would find a false attack in Example B whereas it would not in Example A, because in Example A, the failed checked primitives in Bob's principal Block would correctly prevent `enc_sesskey` from being communicated. In Example B, Verifpal would still consider `enc_sesskey` being communicated despite the protocol execution supposedly halted.

The reason for this was due to some parallel protocol execution logic that allowed to find some pretty crafty attacks but was still not sufficiently refined to avoid this kind of false attack. This commit provides the required refinements.

*** Improvements to Analysis and Performance ***

Some minor analysis bugs have been fixed, the clarity of the analysis output has been improved and general analysis speed appears to have been boosted by around 15%.

-------------------------------
2. PGP-Signed Releases
-------------------------------
Official signed, pre-compiled release builds are provided for Windows, Linux, macOS and FreeBSD in x86, amd64 and arm64 variants, here:
https://source.symbolic.software/verifpal/verifpal/-/releases/v0.14.0

Verifpal releases are signed using the following PGP key:
https://source.symbolic.software/verifpal/verifpal/-/blob/master/assets/pgp.txt

In order to verify the PGP signature of your downloaded Verifpal release binary, please first verify the signature of the checksum file, verifpal_0.14.0_checksums.txt, against its signature, verifpal_0.14.0_checksums.txt.sig. Both files are located in the releases directory linked above.

Once the signature of the checksum file is verified, ensure that the SHA256SUM of your downloaded release archive matches the one listed inside the checksum file for your chosen platform.

-------------------------------
3. Updating Via Package Manager
-------------------------------
If you have installed Verifpal via the Scoop package manager for Windows, simply run the following commands to update to Verifpal 0.14.0:
scoop update
scoop update verifpal

If you have installed Verifpal via the Homebrew package manager on Linux and macOS, simply run the following commands to update to Verifpal 0.14.0:
brew update
brew upgrade verifpal

On Linux, Verifpal is also available via the Snap Store: https://snapcraft.io/verifpal

-------------------------------
4. More Information
-------------------------------
Verifpal is supported by research grants as well as contributions from its users. If you have found Verifpal to be useful, please consider contributing via a donation: https://verifpal.com/donate

Don't forget to join the conversation on the official Verifpal Discord: https://verifpal.com/discord

For more general information about Verifpal, please visit: https://verifpal.com

Thank you,
Symbolic Software Drone


More information about the Verifpal mailing list