[Verifpal] New Primitive: SHAMIR_SPLIT/SHAMIR_JOIN

[Nadim Kobeissi]

Hello everyone,

Verifpal 0.8.8 is now available with an exciting new feature:

Verifpal offers a simple interface for modeling Shamir Secret Sharing, which allows a secret (such as a key) to be split into multiple shares such that only some (and not all) of these shares are required to reconstitute it. In Verifpal, we allow splitting the key into three shares such that only two shares are required to reconstitute it:

SHAMIR_SPLIT(k): s1, s2, s3

Here, sa and sb must be two distinct elements out of the set (s1, s2, s3) in order to obtain k:

SHAMIR_JOIN(sa, sb): k

Hopefully this will allow for modeling more scenarios!

Verifpal 0.8.8 also contains some significant improvements to Verifpal’s analysis logic and other general improvements (thanks to Brian O’Connor for feedback and suggestions for improving the analysis logic.)

The Verifpal User Manual, Visual Studio Code and vim extensions have been updated to reflect the new primitives.

Nadim Kobeissi
Symbolic Software • https://symbolic.software