Tags give the ability to mark specific points in history as being important
  • 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.
    c64c6f4e · Verifpal 0.11.10 ·
    Release v0.11.10

    Changelog

    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.
    6df78304 · Verifpal 0.11.9 ·
    Release v0.11.9

    Changelog

    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.
    a61b52ae · Verifpal 0.11.8 [CI SKIP] ·
  • v0.11.7   Verifpal 0.11.7 This update fixes some bugs with concatenation support.
    8d50492c · Verifpal 0.11.7 [CI SKIP] ·
  • 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.
    f8aca6ec · Verifpal 0.11.6 [CI SKIP] ·
  • v0.11.5   Verifpal 0.11.5 This minor update provides Verifpal built with the latest Go 1.14 runtime, bringing performance improvements.
    8aea0974 · Verifpal 0.11.5 [CI SKIP] ·
  • 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.
    c39c54b6 · Verifpal 0.11.4 [CI SKIP] ·
  • 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.
    e9961851 · Verifpal 0.11.3 [CI SKIP] ·
  • v0.11.2   Verifpal 0.11.2 This release brings bug fixes to the analysis methodology.
    9f21720a · Verifpal 0.11.2 [CI SKIP] ·
  • v0.11.1   Verifpal 0.11.1 This release brings bug fixes to the analysis methodology.
    dc77143a · Verifpal 0.11.1 [CI SKIP] ·
  • 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.
    71ef02c6 · Verifpal 0.10.8 ·
  • 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.
    9549818a · Verifpal 0.10.7 ·
  • 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.
    93b69f99 · Verifpal 0.10.6 ·
  • 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.
    cdbeb44b · Modify tag script ·
  • 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.
    f880fb09 · Verifpal 0.10.4 ·
  • 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.
    c31cde64 · Verifpal 0.10.3 ·
  • v0.10.2   Verifpal 0.10.2
    a19f72f9 · Verifpal 0.10.2 ·
  • v0.10.1   Verifpal 0.10.1
    ed8acaba · Verifpal 0.10.1 ·
  • v0.10.0   Verifpal 0.10.0
    f505c084 · Verifpal 0.10.0 ·