Tags give the ability to mark specific points in history as being important
  • v0.15.2
    ec173291 · Verifpal 0.15.2 ·
    Release v0.15.2
    Verifpal 0.15.2
    
    Verifpal 0.15.2 is the result of a large amount of testing dedicated to allowing the Go runtime to manage stack allocations optimally for very large Verifpal models.
  • v0.15.1
    0916941a · Verifpal 0.15.1 ·
    Release v0.15.1
    Verifpal 0.15.1
    
    Verifpal 0.15.1 fixes an infinite recursion bug in Verifpal analysis.
  • v0.15.0
    bf444ef1 · Verifpal 0.15.0 ·
    Release v0.15.0
    Verifpal 0.15.0
    
    Verifpal 0.15.0 fixes even more bugs in Verifpal analysis detected by Sasha Lapiha.
  • v0.14.9
    032f710e · Verifpal 0.14.9 ·
    Release v0.14.9
    Verifpal 0.14.9
    
    Verifpal 0.14.9 fixes a bug in Verifpal analysis detected by Sasha Lapiha.
  • v0.14.8
    186dbb94 · Verifpal 0.14.8 ·
    Release v0.14.8
    Verifpal 0.14.8
    
    Verifpal 0.14.8 fixes a bug in Verifpal analysis reported by our friends at Quarkslab.
  • v0.14.7
    1ce048a4 · Verifpal 0.14.7 ·
    Release v0.14.7
    Verifpal 0.14.7
    
    Verifpal 0.14.7 fixes a bug with the Verifpal pretty-printer.
  • v0.14.6
    f9f85493 · Verifpal 0.14.6 ·
    Release v0.14.6
    Verifpal 0.14.6
    
    Verifpal 0.14.6 introduces VerifHub support. For more information, visit https://verifhub.verifpal.com.
  • v0.14.5
    1802ce06 · Verifpal 0.14.5 ·
    Release v0.14.5
    Verifpal 0.14.5
    
    Verifpal 0.14.5 is an internal release meant to prepare Verifpal for use with VerifHub, an upcoming service. There is no benefit for users to update to Verifpal 0.14.5. Users should wait for 0.14.6, which will provide new functionality.
  • v0.14.4
    2cd4bcc3 · Verifpal 0.14.4 ·
    Release v0.14.4
    Verifpal 0.14.4
    
    Verifpal 0.14.4 is an internal release meant to prepare Verifpal for use with VerifHub, an upcoming service. There is no benefit for users to update to Verifpal 0.14.4. Users should wait for 0.14.5, which will provide new functionality.
  • v0.14.3
    bd9416da · Verifpal 0.14.3 ·
    Release v0.14.3
    Verifpal 0.14.3
    
    Verifpal 0.14.3 renders Verifpal usable as a Go library within other go applications, by exposing a vplogic package.
  • v0.14.2
    a9d98593 · Update .goreleaser.yml ·
    Release v0.14.2
    Verifpal 0.14.2
    
    Verifpal 0.14.2 introduces bug fixes and improvements to Verifpal model analysis.
  • v0.14.1
    e3aa5e95 · Verifpal 0.14.1 ·
    Release v0.14.1
    Verifpal 0.14.1
    
    Verifpal 0.14.1 fixes a bug in ProVerif model template generation.
  • v0.14.0
    26cafde0 · Verifpal 0.14.0 ·
    Release v0.14.0
    Verifpal 0.14.0
    
    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%.
  • v0.13.7
    e58a9831 · Verifpal 0.13.7 ·
    Release v0.13.7
    Verifpal 0.13.7
    
    Verifpal 0.13.7 fixes two bugs in Verifpal's analysis, both identified and reported by Georgio Nicolas:
    
    - Values declared using Verifpal's password qualifier may result in false positives being identified by Verifpal despite no such attack having taken place in the model.
    
    - Partial resolutions of targeted values in confidentiality queries may have led to missed attacks in certain scenarios.
    
    This release also improves the reproducibility of Verifpal builds and introduces code-signed releases, as discussed on this mailing list thread:
    https://lists.symbolic.software/pipermail/verifpal/2020/000255.html
  • v0.13.6
    cf9261ba · Verifpal 0.13.6 ·
    Release v0.13.6
    Verifpal 0.13.6
    
    Verifpal 0.13.6 fixes an issue where attack traces could sometimes mention the wrong values as being implicated in an attack.
  • v0.13.5
    adae3912 · Verifpal 0.13.5 ·
    Release v0.13.5
    Verifpal 0.13.5
    
    Verifpal 0.13.5 introduces many important fixes:
    
    - A class of missed attacks has been resolved. See the discussion here: https://lists.symbolic.software/pipermail/verifpal/2020/000250.html
    
    - In many cases, Verifpal's analysis speed has been sped up significantly. For example, Verifpal's integration test suite now finishes in roughly half the time compared to before.
    
    - Verifpal's analysis output is now significantly improved. For example, Verifpal now mentions which output of a primitive was recovered by the attacker.
    
    - Some minor fixes.
  • v0.13.4
    b2ab5187 · Verifpal 0.13.4 ·
    Release v0.13.4
    Verifpal 0.13.4
    
    Verifpal 0.13.4 introduces a new command-line interface for Verifpal and minor improvements to Coq and ProVerif translation.
  • v0.13.3
    b095c3d9 · Verifpal 0.13.3 ·
    Release v0.13.3
    Verifpal 0.13.3
    
    Verifpal 0.13.3 introduces two new primitives, BLIND and UNBLIND, which can be used to implement ring signatures.
    
    More information about BLIND and UNBLIND is available in the latest version (print 12) of the Verifpal User Manual, as well as in this commit log: https://source.symbolic.software/verifpal/verifpal/-/commit/d2261c6b0daddbdccee9ef72e06604ede463d405
    
    Verifpal for Visual Studio Code version 1.0.8 supports BLIND and UNBLIND.
  • v0.13.2
    768af7ef · Verifpal 0.13.2 ·
    Release v0.13.2
    Verifpal 0.13.2
    
    Verifpal 0.13.2 provides some minor bug fixes.
  • v0.13.1
    7af1acc8 · Verifpal 0.13.1 ·
    Release v0.13.1
    Verifpal 0.13.1
    
    Verifpal 0.13.1 fixes a bug that would incorrectly deem some model filenames to be too long. This bug only affected Verifpal on Microsoft Windows.