Version 1.1.1

This release includes the following changes:

• updated threat model and procedures to address security advisories GHSA-v43c-fm6q-w8f8 and GHSA-w7jj-jfcc-gf89
• removed the Cryptol compiler and all references thereto, as we were not actually using it to generate code
• fixed a minor type inference issue that prevented the Cryptol model from working with current versions of Cryptol
• added continuous integration for the Isabelle E2E-VIV session
• reimplemented the browsable view of the threat model as a completely local HTML/JavaScript document with additional views, cross-linking, and many other quality-of-life enhancements; this is now part of each release, in addition to the PDF version of the threat model (direct download link)
• reimplemented CI/CD/CV orchestration across the repository
• updated Tamarin proof scripts to support a minor change necessitated by Tamarin 1.12's modified handling of functions declared by builtins
• fixed various spelling and typographical errors in the repository

Latest

This is the latest build of E2E-VIV artifacts from the main branch.

Version 1.1

This release includes the following changes:

• implemented mitigations for a reported clash attack, which was originally reported as a security advisory; the implemented mitigations are described in the issue
• updated the protocol descriptions and diagrams to include the implemented mitigations
• updated the threat model to include the reported clash attack and its mitigations, and did some additional threat model cleanup
• implemented a missing check for a matching ballot tracker within the voting application's check procedure
• modified cryptographic context function names and usage for clarity
• reimplemented the threat model in Python and provided an additional graph visualization for it

Initial Public Release (with Updated Documentation)

This is an update to the initial public release of the VoteSecure repository, including the generated artifacts (FAQ, refinement of concurrent models paper, threat model), to bring some of the documentation (threat model, protocol diagrams, informal protocol specifications) up to date as they were missed in the initial release preparations. The implementation is identical to that of the initial public release.

Initial Public Release

This is the initial public release of the VoteSecure repository, including the generated artifacts (FAQ, refinement of concurrent models paper, threat model).