[Verifpal] Verifpal 2020 Plans

[Nadim Kobeissi]

Hi everyone,

I wanted to share the roadmap for the things I’m planning to accomplish with Verifpal in 2020. January has already seen major improvements to analysis thanks to “skeleton-based value injection” (introduced in 0.8.x) and also multithreaded/multi-core analysis (introduced in 0.9.x). Moving forward, I’ll be focusing on:

Soundness and Implementations:
+ Full automated test suite.
+ Full argument for completeness and soundness properties of Verifpal’s verification methodology.
+ Generating functional, complete, readable and expandable ProVerif/CryptoVerif models from Verifpal models for further analysis, expansion and verification work.

Expanded Verification Features:
+ Having parametrized confidentiality and authentication queries which allow us to explain more fine-grained queries.
+ Make analysis results more readable and produce full attack traces.
+ Support for new advanced primitives, such as Oblivious Pseudorandom Functions (OPRFs)
+ Having stronger notions of “freshness” and introducing observational equivalence.
+ Allowing attackers to compromise principal session material such as keys at certain points in the analysis.
+ Having “phases” for analysis similar to ProVerif for analyzing pre-and post-compromise security.
+ Potentially modeling for protocols with unbounded principals.

Implementation Generation:
+ Generating implementations in Golang from sound verification methodology.

Expanded IDE Integration + Maintenance and Improvements
+ Live feedback and charts as protocol is modeled in Visual Studio Code.
+ Expanding the language's features as requested already by community members on the Verifpal Mailing List.
+ Ability to run Verifpal analysis and code generation features directly from Visual Studio Code.
+ VerifHub: Web interface for Verifpal models and results.
+ Bug fixes, general improvements and quality assurance.
+ Improve packaging and distribution.

I also wanted to discuss updates on addressing Verifpal’s analysis limitations. Earlier versions of Verifpal had the following text in the manual:

"Fresh values are not kept between sessions. This is expected behavior for many symbolic analysis tools, but, in Verifpal, it may lead to some less complete analysis for attacks based on intra-session fresh values, especially, for example, parallel or “multi-protocol” session executions.”

I forgot to mention this, but since Verifpal 0.8.0 (we are currently at 0.9.12), this has been resolved. Verifpal now keeps fresh values between sessions sufficiently to model specifically for multi-protocol session executions. So the warning has been removed from the manual.

Also, regarding this warning:

“`Reconstruct` is largely limited to reconstructing values known by principals, and will not attempt to construct arbitrary values outside of those used and expressed within principal declarations."

This is also no longer true, since Verifpal 0.8.0 also introduced a new method for determining which kinds of values are reconstructed, based on which values would fit the typing requirements that would allow the constructed value to be validly reused in the place of the original value.

Verifpal 0.9.12 is really shaping up to be great, and I am excited about what 2020 will bring.

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200123/f997803a/attachment.sig>