Verifpal 0.27.0

Verifpal 0.27.0 fixes an analysis bug caused by an ill-thought "performance optimization". It also updates a few dependencies.

Thanks to Oskar Goldhahn (NTNU) for detecting the issue.

Verifpal 0.26.1

Verifpal 0.26.1 fixes analysis unreliabilty that could arise when equivalence queries are used.

Equivalence queries remain unstable, and should be used with caution for the time being.

Verifpal 0.26.0

Verifpal 0.26.0 fixes analysis unreliabilty that could arise when a Verifpal model contains a very large number of different queries.

Verifpal 0.25.0

Verifpal 0.25.0 fixes additional analysis bugs reported by "Melanie" on the Discord chat.

Verifpal 0.24.1

Verifpal 0.24.0 fixes a bug that could cause misleading confidentiality query outputs. Verifpal 0.24.1 is a minor follow-up release with improvements to the command-line interface.

Verifpal 0.24.0

Verifpal 0.24.0 fixes a bug that could cause misleading confidentiality query outputs.

Verifpal 0.23.3

Verifpal 0.23.3 fixes a crash that could sometimes occur with models that use the `password` value type.

Verifpal 0.23.2

Verifpal 0.23.2 fixes a crash that could sometimes occur with models that use the `password` value type.

Verifpal 0.23.1

Verifpal 0.23.1 fixes a crash that could sometimes occur with models that use the `password` value type.

Verifpal 0.23.0

Verifpal 0.23.0 introduces equivalence queries.

For many protocols, it could be useful to check whether shared secrets derived between Alice and Bob are equivalent in all completed executions of the protocol. Equivalence queries check whether any protocol scenario can be derived such that the given values are not equivalent to one another.

For example, one could use the following query to check if shared secrets calculated by Alice and Bob will always be equivalent in all protocol executions:

equivalence? ss_a, ss_b

Verifpal 0.22.0

Verifpal 0.22.0 provides native support for the new Apple Silicon platform.

Verifpal 0.21.5

Verifpal 0.21.5 brings analysis bug fixes thanks to feedback from Friedrich Wiemer.

Verifpal 0.21.4

Verifpal 0.21.4 brings analysis bug fixes.

Verifpal 0.21.3

Verifpal 0.21.3 brings further performance improvements to analysis speeds and some analysis bug fixes.

Verifpal 0.21.2

Verifpal 0.21.2 brings further performance improvements to analysis speeds.

Verifpal 0.21.1

Verifpal 0.21.1 brings further performance improvements by improving multithreading strategies.

Verifpal 0.21.0

Verifpal 0.21.0 brings strong performance improvements due to the elimination of string comparison operations from the analysis logic. Verifpal now assigns uint16 IDs for all string values (constant names, principal names, value qualifiers and attributes, etc.) before analysis and compares those instead of comparing strings.

The resulting performance benefits are quite substantial, ranging between 20% and 33% depending on the model being analyzed.

No change was made to the analysis logic itself, aside from eliminating string comparison operations.

Verifpal 0.20.1

Verifpal 0.20.1 fixes a serious bug that prevented attackers from learning values with the `password` qualifiers even when leaked directly. Definitely update.

Thanks to "Mike" for reporting this bug.

Verifpal 0.20.0

Verifpal 0.20.0 fixes a minor bug regarding comments parsing, reported by "Mike". It also fixes a more impactful bug with the resolution of SIGNVERIF checks, also reported by "Mike". Finally, Verifpal 0.20.0 includes a new command, `verifpal about`, which when executed prints out a list of individuals that have contributed meaningful suggestions, bug reports, ideas or discussions to the Verifpal project.

Verifpal 0.19.5

Verifpal 0.19.5 includes minor bug fixes to analysis logic thanks to reports from "Mike".