Tags give the ability to mark specific points in history as being important
  • v0.15.5   Verifpal 0.15.5 Verifpal 0.15.5 brings further improvements and optimizations to analysis logic.
    b782a8f3 · Verifpal 0.15.5 ·
    Release v0.15.5

    Changelog

    da5bbdb7 Brew formula update for verifpal version v0.15.4
    2c069928 Scoop update for verifpal version v0.15.4
    8a853bdf Smarter skeletons
    b782a8f3 Verifpal 0.15.5

  • v0.15.4   Verifpal 0.15.4 Verifpal 0.15.4 contains some minor performance improvements.
    c660b2b4 · Verifpal 0.15.4 ·
    Release v0.15.4

    Changelog

    052ad6e3 Brew formula update for verifpal version v0.15.3
    7e440964 Don't reconstruct core primitives into attackerState
    caef3444 Scoop update for verifpal version v0.15.3
    c660b2b4 Verifpal 0.15.4

  • v0.15.3   Verifpal 0.15.3 Verifpal 0.15.3 contains some minor performance improvements.
    dd8db7bb · Verifpal 0.15.3 ·
    Release v0.15.3

    Changelog

    493418bc Brew formula update for verifpal version v0.15.2
    5b018d2f Don't invent a new value on ASSERT pass
    9e5e184f Minor optimization
    08b065ab Remove constants from signal model
    42fd84bc Scoop update for verifpal version v0.15.2
    dd8db7bb Verifpal 0.15.3

  • 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.
    ec173291 · Verifpal 0.15.2 ·
    Release v0.15.2

    Changelog

    23429bf3 Brew formula update for verifpal version v0.15.1
    aaba095d Reinstate two goroutine spawning points
    874776f5 Scoop update for verifpal version v0.15.1
    b26c6818 Show flags in CLI help
    ec173291 Verifpal 0.15.2

  • v0.15.1   Verifpal 0.15.1 Verifpal 0.15.1 fixes an infinite recursion bug in Verifpal analysis.
    0916941a · Verifpal 0.15.1 ·
    Release v0.15.1

    Changelog

    a595f8d4 Brew formula update for verifpal version v0.15.0
    33722391 Fix Windows build script
    0a60cd0b Increase maximum stack size
    a4fac663 Print analysis count once every 500 times
    2e9fc4af Remove newline
    52f939f2 Remove stack size increase
    99205f65 Resolve attackerState
    1c328749 Restore mutationMapSkipValue type restrictions
    d904f4a3 Scoop update for verifpal version v0.15.0
    a6a9d9ff Simplify test
    0916941a Verifpal 0.15.1

  • v0.15.0   Verifpal 0.15.0 Verifpal 0.15.0 fixes even more bugs in Verifpal analysis detected by Sasha Lapiha.
    bf444ef1 · Verifpal 0.15.0 ·
    Release v0.15.0

    Changelog

    36c9ced6 Add more tests
    162d83c6 Brew formula update for verifpal version v0.14.9
    d1f1400c More bug fixes
    5410203e Scoop update for verifpal version v0.14.9
    a3f3550d Update .goreleaser.yml
    bf444ef1 Verifpal 0.15.0

  • v0.14.9   Verifpal 0.14.9 Verifpal 0.14.9 fixes a bug in Verifpal analysis detected by Sasha Lapiha.
    032f710e · Verifpal 0.14.9 ·
    Release v0.14.9

    Changelog

    403ad546 Address incomplete resolution logic
    8024656b Brew formula update for verifpal version v0.14.8
    20c7cb9e Experimentation with Go implementation generation
    60c30ed8 Scoop update for verifpal version v0.14.8
    b89337bd Simplify simple.vp
    032f710e Verifpal 0.14.9
    69c0360d libgogen

  • v0.14.8   Verifpal 0.14.8 Verifpal 0.14.8 fixes a bug in Verifpal analysis reported by our friends at Quarkslab.
    186dbb94 · Verifpal 0.14.8 ·
    Release v0.14.8

    Changelog

    d0f4dfe2 Brew formula update for verifpal version v0.14.7
    3d379eb6 Clean up libgo code so far
    5dc6a3a6 Clean up libgo code so far
    75cba08a Remove old code/bad attackerStateWrite operations
    802100d4 Scoop update for verifpal version v0.14.7
    186dbb94 Verifpal 0.14.8

  • v0.14.7   Verifpal 0.14.7 Verifpal 0.14.7 fixes a bug with the Verifpal pretty-printer.
    1ce048a4 · Verifpal 0.14.7 ·
    Release v0.14.7

    Changelog

    d84f8c0a Brew formula update for verifpal version v0.14.6
    0a77b7b7 Scoop update for verifpal version v0.14.6
    1ce048a4 Verifpal 0.14.7

  • v0.14.6   Verifpal 0.14.6 Verifpal 0.14.6 introduces VerifHub support. For more information, visit https://verifhub.verifpal.com.
    f9f85493 · Verifpal 0.14.6 ·
    Release v0.14.6

    Changelog

    0fa7c166 Brew formula update for verifpal version v0.14.5
    922e294c Scoop update for verifpal version v0.14.5
    f9f85493 Verifpal 0.14.6

  • 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.
    1802ce06 · Verifpal 0.14.5 ·
    Release v0.14.5

    Changelog

    4037e09d Brew formula update for verifpal version v0.14.4
    1dc70614 Scoop update for verifpal version v0.14.4
    1802ce06 Verifpal 0.14.5

  • 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.
    2cd4bcc3 · Verifpal 0.14.4 ·
    Release v0.14.4

    Changelog

    912f297d Brew formula update for verifpal version v0.14.3
    6ede4c0c Rework Verifpal's entire error handling logic
    92c8b765 Scoop update for verifpal version v0.14.3
    2cd4bcc3 Verifpal 0.14.4

  • 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.
    bd9416da · Verifpal 0.14.3 ·
    Release v0.14.3

    Changelog

    d584c26e Brew formula update for verifpal version v0.14.1
    f20a996b Brew formula update for verifpal version v0.14.2
    2d0d52b6 File permissions
    360a924b Fix .gitlab-ci.yml
    0c13e755 Make Verifpal logic exportable as a Go library called vplogic, with the Verifpal command acting as a wrapper
    0ee14f8c Minor tweaks to Cobra
    7a308c36 Prioritize resolution and rewrite of SPLITs
    a6eee297 Race condition fix
    5fd17435 Remove unnecessary resolution
    657cc25c Reorganize project structure
    d6ba27d2 Scoop update for verifpal version v0.14.1
    1876473d Scoop update for verifpal version v0.14.2
    01d109d0 Update .goreleaser.yml
    a9d98593 Update .goreleaser.yml
    f335c87a VerifHub integration
    82c25a2f Verifpal 0.14.2
    addbeeb7 Verifpal 0.14.3
    e4238a1b Verifpal 0.14.3
    bd9416da Verifpal 0.14.3

  • v0.14.2   Verifpal 0.14.2 Verifpal 0.14.2 introduces bug fixes and improvements to Verifpal model analysis.
    a9d98593 · Update .goreleaser.yml ·
    Release v0.14.2

    Changelog

    d584c26e Brew formula update for verifpal version v0.14.1
    2d0d52b6 File permissions
    0ee14f8c Minor tweaks to Cobra
    7a308c36 Prioritize resolution and rewrite of SPLITs
    a6eee297 Race condition fix
    5fd17435 Remove unnecessary resolution
    657cc25c Reorganize project structure
    d6ba27d2 Scoop update for verifpal version v0.14.1
    a9d98593 Update .goreleaser.yml
    01d109d0 Update .goreleaser.yml
    f335c87a VerifHub integration
    82c25a2f Verifpal 0.14.2

  • v0.14.1   Verifpal 0.14.1 Verifpal 0.14.1 fixes a bug in ProVerif model template generation.
    e3aa5e95 · Verifpal 0.14.1 ·
    Release v0.14.1

    Changelog

    98c84d07 Brew formula update for verifpal version v0.14.0
    213af6c5 Fix ProVerif template generation issue
    753fafca Scoop update for verifpal version v0.14.0
    e3aa5e95 Verifpal 0.14.1

  • 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%.
    26cafde0 · Verifpal 0.14.0 ·
    Release v0.14.0

    Changelog

    bd233aa8 Add PGP public key
    7c237d64 Brew formula update for verifpal version v0.13.7
    11c60a07 Clearer analysis output
    9f3022a6 Fix class of false positives
    04772cef Improve email template
    836d0990 Merge Coq branch
    b4e5dd41 Merge branch 'coq' into 'master'
    b4df4c6e Merge branch 'coq' into 'master'
    91f207c5 Minor changes to release pipeline
    c90fde90 Passive Attacker in Coq
    9ea0d7b9 Refactor code to remove indentation
    7df03238 Refactoring for freshness and unlinkability queries
    0ad2d6d4 Scoop update for verifpal version v0.13.7
    992b69ee Update Makefile
    26cafde0 Verifpal 0.14.0

  • 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
    e58a9831 · Verifpal 0.13.7 ·
    Release v0.13.7

    Changelog

    89812845 Add -trimpath to go build parameters
    0385338f Add pw_hash2.vp
    d9e702ac Brew formula update for verifpal version v0.13.6
    bb10e517 Check confidentiality matches against fully resolved values every time
    6c1b7d9e More fine-grained rules for password hashing primitives
    47026962 Qualify Verifpal as Beta software
    636951d9 Remove email.sh
    77a1095e Remove releases from CI/CD pipeline except for Snapcraft
    e0d8301a Remove tag.sh
    5af47cd6 Scoop update for verifpal version v0.13.6
    aace097f Update Makefile
    e58a9831 Verifpal 0.13.7

  • 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.
    cf9261ba · Verifpal 0.13.6 ·
    Release v0.13.6

    Changelog

    605bead2 Brew formula update for verifpal version v0.13.5
    6063260d Bug fix: query contradiction trace sometimes mentioned wrong values
    9942a147 Make Snapcraft happy
    aa4d6372 Merge branch 'master' of ssh://source.symbolic.software/verifpal/verifpal
    b33f684c Restore Snapcraft runs on tags only
    9b0666d0 Scoop update for verifpal version v0.13.5
    cbf0e784 Update README.md
    cf9261ba Verifpal 0.13.6

  • 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.
    adae3912 · Verifpal 0.13.5 ·
    Release v0.13.5

    Changelog

    cda5cbcd Add GOPATH bin path
    07d77047 Add git to snapcraft CD job
    fb3ec6b6 Add go generate to lint and test jobs
    3a90b178 Add go generate to lint and test jobs
    a5991807 Add lib artifacts to repo to make Snapcraft happy
    a2cafe45 Add lib artifacts to repo to make Snapcraft happy
    f043bdfd Add make to Snapcraft CD container
    22591356 Add test for Lowe's Needham-Schroeder fix (see previous commit)
    5ba9ec17 Analysis optimization
    7696cad3 Brew formula update for verifpal version v0.13.4
    1965171c Deal with baffling Gitlab CI behavior
    3e148792 Delete lib artifacts
    ae87a424 Force trigger Snapcraft
    463d067c Force trigger Snapcraft
    c98966d0 Goroutine experiments (WIP)
    50922404 Improve build strategy
    88c525cf Install go latest in snapcraft image
    8bda7b99 Merge branch 'master' of ssh://source.symbolic.software/verifpal/verifpal
    d5c65b0a Minor cleanup
    45b6d849 Minor cleanup
    67d1cd10 Output formatting fixes
    4944fc95 Remove dep step from Makefile test job
    ef0fc4c0 Restrict snapcraft to cmd/verifpal and attempt core20 one last time
    4283ed0b Scoop update for verifpal version v0.13.4
    1fe38a29 Setting GOOS on go generate causes toolchain problems
    5701e232 Snapcraft core20 seems unable to connect
    a4ea642a Specify which output of primitives was recovered by attacker
    15153a68 Thanks Snapcraft, we're good
    29695d76 Try snapcraft from source
    13f28d15 Try snapcraft with golang image
    73063528 Use 18.04 on the Docker side and 20.04 on the snapcraft core side
    a318bc7a Use 18.04 on the Docker side and 20.04 on the snapcraft core side
    53f953b7 Use 19.10 on the Docker side and 20.04 on the snapcraft core side
    adae3912 Verifpal 0.13.5
    5dcad768 Verifpal did not detect Lowe's Needham-Schroeder Attack
    3d0ecab9 core20 seems broken on Snap's side
    a9dac125 go 1.10 compat
    e0b2d429 libgo: Hash shared secret for PKE_ENC/PKE_DEC

  • 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.
    b2ab5187 · Verifpal 0.13.4 ·
    Release v0.13.4

    Changelog

    2b6c03a7 Add BLIND and UNBLIND to ProVerif models
    9cbf6f10 Add unlinkability query to DP-3T model
    19a31127 Break Go subcommand
    0e0afe5c Brew formula update for verifpal version v0.13.3
    351bf41b Clean up arity spec
    0c13b526 Coq
    96b5b26c Delete lib artifacts
    d4c0c3db Fix CI
    743c0eb7 Fix CI
    3f2e3670 Fix go.mod and go.sum
    29efd93a Merge branch 'coq' into 'master'
    ef5fd574 New CLI interface!
    c256ce7a Permissions
    01ade806 Remove comment
    cd8489e0 Rename ProVerif and Implement files and subcommands
    36b8e6eb Reorganize project structure into "lib" internals
    07f5c4e6 Restrict overly permissive rebuild rule checker
    d6375747 Scoop update for verifpal version v0.13.3
    8a09b49e Significant code cleanup
    f189e119 Some scratch notes for libgo
    07854dc2 Split pretty.go into info.go
    62a8bdd1 Update verifpal.rb
    5f354cbd Use SPDX
    b2ab5187 Verifpal 0.13.4
    a0abe4a4 WIP on libgo
    e92348e2 WIP on libgo
    f518bc3a WIP on libgo