v0.11.10 Verifpal 0.11.10 This update brings minor improvements and the addition of two new example models focusing on the Needham-Schroeder protocol.Release v0.11.10
239825af Add LICENSE
1a7700de Add utility function
a5ac6687 Add utility function
31d42697 Brew formula update for verifpal version v0.11.9
63d9542b Errorf, not Sprintf
3ed43036 Fix incorrect keyword in syntax highlighting plugins
f81570d5 Friedrich Wiemer's Needham-Schroeder model
95770823 Merge branch 'master' of ssh://source.symbolic.software/verifpal/verifpal
c7936403 Needham-Schroeder models
e55679e9 Replaces LICENSES with LICENSE
ff7911b2 Scoop update for verifpal version v0.11.9
14502ae8 Update .gitlab-ci.yml
63bb52ff Verifpal 0.11.10
c64c6f4e Verifpal 0.11.10
v0.11.9 Verifpal 0.11.9 This update brings no new changes and is purely meant to ensure that the new release pipeline functions correctly.Release v0.11.9
2df1bda8 Add home interface plug to Snapcraft YAML
24922fc4 Add lang to html header
43a594f0 Brew formula update for verifpal version v0.11.9
fbeebe32 Code cleanup and simplification
502e5be9 Experimenting with gitlab-ci
681847ae Experimenting with gitlab-ci
0134e95d Experimenting with gitlab-ci
6ffe4181 Experimenting with gitlab-ci
223cac48 Experimenting with gitlab-ci
78f72c40 Experimenting with gitlab-ci
fb7ca035 Experimenting with gitlab-ci
45207a8d Experimenting with gitlab-ci
3b0cbe54 Experimenting with gitlab-ci
57f8cab0 Move Snap to Makefile [CI SKIP]
540cdaba Play around with gitlab-ci
b4321b4b Prepare to test releases
ff720afa Prepare to test releases
ba265dbc Prepare to test releases
9a654071 Prepare to test releases
cdbd01ae Prepare to test releases
52f43804 Prevent accidental commits of snapcraft.login
8c09da6e Remove .drone.yml
eda46544 Remove badges
c013dbf0 Remove unnecessary booleans
d76a3813 Restore release email script
5257f1bf Scoop update for verifpal version v0.11.9
3851aeb8 Update package manager formulas [CI SKIP]
993b2534 Update some release URIs
6df78304 Verifpal 0.11.9
c0c1cf7c Verifpal 0.11.9 [CI SKIP]
v0.11.8 Verifpal 0.11.8 This update fixes some bugs with concatenation support.
v0.11.7 Verifpal 0.11.7 This update fixes some bugs with concatenation support.
v0.11.6 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.
v0.11.5 Verifpal 0.11.5 This minor update provides Verifpal built with the latest Go 1.14 runtime, bringing performance improvements.
v0.11.4 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.
v0.11.3 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.
v0.11.2 Verifpal 0.11.2 This release brings bug fixes to the analysis methodology.
v0.11.1 Verifpal 0.11.1 This release brings bug fixes to the analysis methodology.
v0.11.0 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.
v0.10.8 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.
v0.10.7 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.
v0.10.6 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.
v0.10.5 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.
v0.10.4 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.
v0.10.3 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.