Last week, Verifpal, our cryptographic protocol modeling and analysis framework, celebrated its one-year anniversary. In its first year, Verifpal has made some significant achievements.
Improvements to Usability, Features, and Reliability
First, Verifpal has improved its relationship with users. Verifpal was part of Zoom’s effort to modernize its cryptography. Verifpal for Visual Studio Code and VerifHub allowed engineers to model and collaborate on cryptographic protocols more easily than ever. And better attack traces allowed for easier to understand analysis results.
Verifpal for Visual Studio Code allows visualizing and analyzing Verifpal models straight inside Visual Studio Code, with easy access to documentation for primitives and other functionality by hovering with the cursor.
Second, Verifpal obtained new features that allow it to capture more of a protocol’s workings. Verifpal gained the ability to model protocols where users can potentially input weak or strong passwords. This is very useful for modeling protocols that include user-provided passwords at points, and is a great way to separate guessable passwords from material that can actually securely be used as an encryption key of some kind. New primitives were introduced, allowing the usage of ring signatures, public key encryption, Shamir secret sharing and blind signatures. The leaks keyword now exists, allowing principals to leak constants to the attacker without necessarily sending them to another principal. Phases are an exciting new feature that allows Verifpal to reliably model post-compromise security properties such as forward secrecy or future secrecy. Query preconditions allow for illustration relationships between different Verifpal queries on a protocol. And dozens of small improvements and changes were made to Verifpal across its application stack.
Finally, and most importantly, Verifpal improved its analysis strength and reliability. As documented in a previous post, Verifpal’s formal semantics and passive attacker analysis are now fully modeled in the Coq theorem prover. While this does not include active attacker analysis methodology, it does indicate that we can capture Verifpal’s semantics elegantly in existing formalism methods as well as a basic component of its analysis methodology. Our revised Verifpal paper goes into further detail on the Verifpal active attacker analysis methodology and describes formally how primitives are defined, deconstructed and analyzed in Verifpal. Furthermore, valuable feedback was received from over a dozen Verifpal community members that allowed detecting and fixing analysis errors, misleading analysis results and that pushed us to more concretely define the meaning and function of Verifpal queries such as freshness and authentication. These discussions occurred on the Verifpal Mailing List, the Verifpal Discord as well as via private feedback.
Verifpal’s paper was revised to go into further detail regarding the analysis methodology, formal semantics and the limits of Verifpal analysis. PrimitiveSpecs were introduced in order to standardize how primitives are defined and how their semantics operate within Verifpal analysis, i.e. via the following operations:
• Decompose. Given a primitive’s output and a defined subset of its inputs, reveal one of its inputs. (Given ENC(k, m) and k, reveal m).
• Recompose. Given a subset of a primitive’s outputs, reveal one of its inputs. (Given a, b, reveal x if a ,b,_ = SHAMIR_SPLIT(x)).
• Rewrite. Given a matching defined pattern within a primitive’s inputs, rewrite the primitive expression itself into a logical subset of its inputs. (Given DEC(k, ENC(k, m)), rewrite the entire expression DEC(k, ENC(k, m)) to m).
• Rebuild. Given a primitive whose inputs are all the outputs of some same other primitive, rewrite the primitive expression itself into a logical subset of its inputs. (Given SHAMIR_JOIN(a, b) where a, b, c = SHAMIR_SPLIT(x), rewrite the entire expression SHAMIR_JOIN(a, b) to x).
Understanding Verifpal’s Purpose in the Protocol Security Space
Given Verifpal’s progress over its first year, it becomes ever more important to clearly answer the question: “Where is Verifpal positioned within the protocol security space in comparison to other tools?” What is Verifpal able to do for me, the protocol analyst, engineer or applied cryptography practitioner?
Verifpal appears to be evolving towards being software best suited for designing, modeling, analyzing and testing cryptographic protocols. Notably, this means that Verifpal is not likely to progress in the direction where it functions as a producer of protocol security proofs, nor does our experience lead us to believe that this is a space where more contributions are likely to be useful or impactful. This latter functionality will likely remain the jurisdiction of tools such as Tamarin.
Verifpal’s goal is to focus on the real-world priority of exceeding these tools in terms of how much time and effort it will take for the engineer or practitioner to obtain a meaningful model of their protocol that gives them meaningful analysis answers. However, the compromises to ease of use and modeling/analysis rapidity required for Verifpal to offer full proving capabilities are deemed too great given Verifpal’s design and functionality goals, and therefore will likely never be adopted fully into its functionality.
For example, Verifpal’s strategy for dealing with state space explosion imposes limitations on the completeness of its analysis, but this appears to only affect protocols that are unlikely to ever appear in real-world scenarios, while also granting Verifpal greater analysis speed and likelihood for analysis termination than other tools.
In deciding Verifpal’s priorities, we slam the brakes at the moment where the learning curve, effort and analysis cost begin to have strongly diminishing returns for the user. Our bet is that this path forward for Verifpal will lead to a hugely more substantial impact for engineers and practitioners than traditional automated proof modeling tools. In the example above, we can see how Verifpal makes compromises in analysis completeness that preclude its ability to output full proofs but that greatly increase the likelihood of analysis termination (a significant problem for tools such as ProVerif) without having an apparently significant impact on the analysis of real-world, non-Ivory-Tower protocols.
Ergo, Verifpal’s main responsibility is to straddle a balance between soundness/reliability and ease of use/relevance to real-world practitioners. The way we approach this responsibility is by making sure that Verifpal’s semantics are formally specified, that its analysis methodology is amply documented, and that its code is easy to understand. Verifpal’s formal semantics in Coq, the analysis methodology details in the Verifpal paper documented and easy-to-understand Go codebase aim to fulfill this purpose.
Simultaneously, Verifpal utilizes this formally specified base in order to maintain the development of a language and framework that is idiomatic to the extreme. The Verifpal language is meant to illustrate protocols close to how one may describe them in an informal conversation, while still being precise and expressive enough for formal modeling. Verifpal avoids user error by not allowing users to define their own cryptographic primitives. Instead, it comes with built-in cryptographic functions which nevertheless are defined and which operate according to a formally specified standard with concrete semantics. All of this is coupled with a high standard for documentation, accessibility and support in popular workflows and code editors (via Verifpal for Visual Studio Code and VerifHub).
So far, Verifpal’s chosen path has allowed it to provide value in the quick modeling and correct analysis of the DP-3T pandemic contact tracing protocol as it was being specified, and has helped Zoom, Monocypher and others achieve quick protocol modeling and prototyping insight as they developed their protocols, by offering a methodology and framework that allowed results to be obtained in hours (sometimes minutes!) instead of weeks. We hope to continue making exciting developments in Verifpal well into 2021, and can’t wait to see how the community makes use of it.