Verifpal 0.13.0

Verifpal 0.13.0 introduces support for the Verifpal for Visual Studio Code IDE, a video of which can be viewed here: https://twitter.com/verifpal/status/1253679064742756352

This update also includes bug fixes to the Verifpal Coq implementation generator and the Verifpal pretty-printer.

Verifpal 0.12.0

Verifpal 0.12.0 introduces freshness queries, unlinkability queries and highly experimental ProVerif and Coq model generation. For more information, please read the blog post at: https://blog.symbolic.software/2020/04/14/freshness-unlinkability-model-semantics-verifpal/

Verifpal 0.11.10

This update brings minor improvements and the addition of two new example models focusing on the Needham-Schroeder protocol.

Verifpal 0.11.9

This update brings no new changes and is purely meant to ensure that the new release pipeline functions correctly.

Verifpal 0.11.8

This update fixes some bugs with concatenation support.

Verifpal 0.11.7

This update fixes some bugs with concatenation support.

Verifpal 0.11.6

This release brings support for value concatenation! Learn more by reading the following commit notes: https://source.symbolic.software/verifpal/verifpal/commit/87eb78885212c8a40d42696a8156bc8b8cfc121b

Also, parser error messages are improved to be more informative.

Verifpal 0.11.5

This minor update provides Verifpal built with the latest Go 1.14 runtime, bringing performance improvements.

Verifpal 0.11.4

In this release, we build upon the performance improvements introduced in Verifpal 0.11.3 and offer even faster analysis. Overall, Verifpal 0.11.4 is dramatically, almost incomparably faster than Verifpal 0.11.2 and previous versions.

Verifpal 0.11.3

Verifpal 0.11.3 brings dramatic analysis speed improvements across the board, thanks to some optimizations to the heuristics logic and the rewriting of some core functions.

Verifpal 0.11.2

This release brings bug fixes to the analysis methodology.

Verifpal 0.11.1

This release brings bug fixes to the analysis methodology.

Verifpal 0.11.0

In this release, major improvements are made to Verifpal's stability and performance, thanks to analysis code optimizations and the elimination of some race conditions that could appear in rare conditions.

Verifpal 0.10.8

In this release, improvements are made to the heuristics that Verifpal uses in order to attempt to shorten analysis time and avoid state space explosions. The result should be significantly faster analysis for most models.

Verifpal 0.10.7

In this release, we attempt a new approach at dealing with state space explosions: bounding the analysis exclusively on HKDF primitive mutations, while keeping the analysis unbounded on everything else.

Verifpal 0.10.6

In this release, we add experimental support for a new ring signatures primitive, as suggested by Sebastian R. Verschoor:
https://lists.symbolic.software/pipermail/verifpal/2020/000157.html

Two primitives are added:

	- RINGSIGN(key_a, G^key_b, G^key_c, message): signature. In ring signatures, one of three parties (Alice, Bob and Charlie) signs a message. The resulting signature can be verified using the public key of any of the three parties, and the signature does not reveal the signatory, only that they are a member of the signing ring (Alice, Bob or Charlie). The first key must be the private key of the actual signer, while the subsequent two keys must be the public keys of the other potential signers.

	- RINGSIGNVERIF(G^a, G^b, G^c, m, RINGSIGN(a, G^b, G^c, m)). Verifies if a ring signature can be authenticated. The signer's public key must match one or more of the public keys provided, but the public keys may be provided in any order and not necessarily in the order used during the RINGSIGN operation.

Verifpal 0.10.5

In this release, we add the new "leaks" expression, which allows principals to leak values to the attacker without necessarily sending them to one another over the network, like this:

principal Alice[
    knows private verySecretSecret
    leaks verySecretSecret
]

The attacker now knows verySecretSecret.

Other minor improvements and optimizations are included.

Verifpal 0.10.4

In this release, the heuristics added in 0.10.3 to constrain HKDF mutation state explosion are relaxed in order to reduce missed attacks. Two new tests, subkey_hash.vp and subkey_hkdf.vp, are added in order to ensure that these missed attacks do not recur.

Verifpal 0.10.3

In this release, we continue the 0.10.x trend of focusing on a more comprehensive analysis. 0.10.2 improved the scope of the analysis by allowing HKDF values to be mutated by the attacker, but this introduced an enormous state space explosion overhead. In 0.10.3, we improve the heuristics used by Verifpal in order to attempt to reduce the potential for state space explosion and keep analysis fast/actually terminating. Heuristic improvements come at the risk of reduced analysis completeness, something which we will need to continue to evaluate as Verifpal grows.

Verifpal 0.10.2