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: “Intuitively, this condition aims to prevent attacks in which, for some possible behaviour of the attacker, there exists a relation between messages that leaks information about the involved agents. Practically speaking, this condition requires that any reachable frame must be statically equivalent to an idealised frame that does not depend on identity parameters. A very simple way to obtain an idealisation of a frame is to replace each output message by a fresh nonce. In that case, if the real frame and the idealised frame are statically equivalent, it is obvious that the attacker cannot learn anything by analysing the relations between the messages, since there is no relation between disctinct fresh nonces. Nevertheless, it is not satisfying because too restrictive as e.g. a pair is distinguishable from a nonce.”
- Well-authentication: “The idea behind this second condition is to avoid that the outcome of conditionals leaks information about identities to the attacker. To do so, we require that whenever a conditional (let or lookup) is positively evaluated, the corresponding agent is having an honest interaction with another participant. In practice, protocols often have some conditionals for which the attacker already knows the outcome: these safe conditionals can (and must) be excluded from our condition.”
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:
- First, Verifpal checks to see if
aandbsatisfy freshness. If they do not, the query fails. Similarly to regular freshness queries, if an attacker can coerce a value to be non-fresh across sessions, then it is non-fresh and the query fails. - If
aandbboth satisfy freshness, Verifpal then checks to see if the attacker can determine them as being the output of the same primitive (for example, the first and second output of the same HKDF construction with the same inputs.) Of course,aandbcan indeed be the outputs of that HKDF and be unlinkable; unless the attacker is able to reconstruct that same HKDF primitive and thereby use it to determine that both values are the outputs of it.
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:
- ProVerif: ProVerif is the verification software that inspired Verifpal and which was written by my former thesis co-advisor Bruno Blanchet. ProVerif has existed for around 20 years and can perform a more diverse set of analyses than Verifpal despite both softwares belonging to the same category of verifiers (symbolic model protocol verifiers).
- Coq: Coq is a full-fat theorem prover that can do way more than handle the description of protocols. Georgio Nicolas has been handling Coq translations, with Mukesh Tiwari recently joining our effort and lending a hand (welcome, Mukesh!). Currently, we have fully formalized the semantics of Verifpal in Coq, and we are working on also formalizing the attacker and verification logic in Coq as well for both active and passive attackers. At that point, we will have fully implemented Verifpal in Coq.
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:
- New primitives, such as public-key encryption, Shamir secret sharing and ring signatures.
- Multi-threaded, concurrent analysis using Go’s excellent multithreading support. Put that gaming PC to work!
- Password-hashing modeling, which allows for models to capture when a weak/guessable/bruteforceable password is used as, for example, an encryption or signing key.
leaksexpression, which allows simulating the leaking of a value on the network without sending is as a message.- Queries as preconditions for messages.
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:
- NLNet Foundation: Verifpal is sponsored by the NLNet Foundation. Funding was provided through the NGI0 Privacy Enhancing Technologies Fund, a fund established by NLnet with financial support from the European Commission’s Next Generation Internet program, under the aegis of DG Communications Networks, Content and Technology under grant agreement №825310.
- Cure53: Verifpal is also supported by Cure53, a Berlin-based security auditing firm which provides penetration testing for online services, security analysis and architectural advice for security and cryptographic applications, training, consulting, incident management and malware analysis.
And, of course, users like you. Thank you!
Get involved in Verifpal discussions today, either through:
- Verifpal Mailing List, for more long-form and serious discussions, or,
- Verifpal Discord, where you can chat with Verifpal contributors, users and enthusiasts!