For the past few weeks, repeated requests have appeared for Verifpal to provide more analysis features in the way of detecting replay attacks and also in supporting the analysis of the unlinkability of values in protocols.

Friedrich Wiemer pointed out that Verifpal was not flexible enough to detect replay attacks in Needham-Schroeder, while Anders N. also requested replay attack detection recently in relation to other protocols. Others have also made such a request. Unlinkability became a pertinent feature especially after our attempts to sketch a model of the DP-3T pandemic-tracing protocol in Verifpal) last week.

Furthermore, there have been many requests since Verifpal’s inception to allow for more in-depth analysis of Verifpal models using tools that have existed for decades longer, such as ProVerif, CryptoVerif, Tamarin and Coq.

As such, Verifpal 0.12.0 will introduce many new features that will allow it to expand and mature in ways meant to address the above:

Freshness Queries in Verifpal

Freshness queries are useful for detecting replay attacks. In passive attacker mode, a freshness query will check whether a value is “fresh” between sessions (i.e. if it has at least one composing element that is generated, non-static). In active attacker mode, it will check whether a value can be rendered “non-fresh” (i.e. static between sessions) and subsequently successfully used between sessions. An example of freshness queries is available in examples/test/freshness.vp.

Freshness queries are currently fairly well-defined in themselves, but it is unclear still whether they are flexible enough to detect the kinds of replay attacks that are envisioned by our users. As such, further discussion is welcome on the Verifpal Mailing List in order to understand how replay attack detection in Verifpal can be further improved.

Unlinkability Queries in Verifpal

Protocols such as DP-3T, voting protocols and RFID-based protocols posit an “unlinkability” security property on some of their components or processes. Definitions for unlinkability vary wildly despite the best efforts of researchers. Complicating matters further, the actually-formalized definitions for unlinkability tend to pertain to processes and not to values like the definition used by, for example, DP-3T.

In DP-3T, definitions for unlinkability are suggested to go along these lines: “for two observed ephIDs, the adversary cannot distinguish between a game in which they belong to the same user and a game in which they belong to two different users.” (definition elucidated with Benjamin Lipp; the DP-3T whitepaper itself does not currently have one).

Hirschi, Delaune et al have a couple of papers exploring the formalization of unlinkability: A Method for Unbounded Verification of Privacy-type Properties, followed by A Method for Proving Unlinkability of Stateful Protocols. In these papers, the unlinkability of processes is defined as the satisfaction of two properties: “frame opacity” and “well-authentication”:

Frame opacity seems clear enough, and well-authentication seems to be the combination of the traditional notion of “strong authentication” or “mutual authentication”, combined with an assumption of honest protocol-following on behalf of the other party (i.e. the protocol “executing correctly”).

Based on the above, Verifpal 0.12.0 will introduce experimental support for a notion of unlinkability in Verifpal that centers more on values than on processes. For example, one could write unlinkability? a, b as a query to test whether a and b are unlinkable from one another. Unlinkability checks for the following:

Further testing of this definition of unlinkability in Verifpal is strongly welcome, as it is very much expected that it will be further elucidated since it is highly doubtful that it covers all cases on unlinkability. Again, Verifpal Mailing List.

Formalizing Verifpal in Coq, and Experimental ProVerif/Coq Model Generation

Work has been ongoing on allowing for the automated translation of Verifpal models to the languages of other tools for those interested in carrying out further analysis:

Experimental ProVerif and Coq model generation will be available for testing in Verifpal 0.12.0. Type verifpal help to find out more on how to use Verifpal to generate these models.

Once support for ProVerif and Coq in Verifpal has matured, and especially once attacker and verification logic is captured in Coq on top of the current semantics, another more detailed blog post will follow.

Looking Towards a Bright 2020

Finally, Verifpal 0.12.0 will also support phases in passive attacker mode, and not just in active attacker mode as before.

These developments in Verifpal are incredibly exciting. They come hot on the heels of many other new features and improvements that have been introduced so far in 2020:

All of this is in line with our announced Verifpal 2020 plans, and the progress on these plans so far has been highly encouraging.

The list of projects using Verifpal continues to grow, and none of this would have been possible without the help of our supporters:

And, of course, users like you. Thank you!

Get involved in Verifpal discussions today, either through: