One Year of Verifpal: Understanding Verifpal’s Relationship With Cryptographic Protocol Security

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.
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.

Towards Freshness Queries, Unlinkability Queries, Automated Model Translation and Formalized Semantics in Verifpal

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 a and b satisfy 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 a and b both 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, a and b can 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:

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:

How Verifpal Dramatically Sped Up the Formal Modeling Efforts for a New Pandemic-Tracing Protocol

Last week, numerous researchers published the timely fruits of their recent collaboration to provide a proximity-tracking solution that can help during pandemics while still being privacy-preserving: the result, Decentralized Privacy-Preserving Proximity Tracing (DP-3T), provides a promising first step in bringing real-world cryptography into the effort to combat the COVID-19 pandemic. As mentioned in Troncoso et al.’s whitepaper, the goal of DP-3T is:

“…to simplify and accelerate the process of identifying people who have been in contact with an infected person, thus providing a technological foundation to help slow the spread of the SARS-CoV-2 virus. The system aims to minimise privacy and security risks for individuals and communities and guarantee the highest level of data protection.”

Troncoso et al, Decentralized Privacy-Preserving Proximity Tracing

In support of this project, we at Symbolic Software decided to test out Verifpal, our open source protocol verification framework, to see how well its promises of easier and more accessible protocol modeling and verification can hold up in the face of a new and ambitious protocol that targets a novel use case.

In this post, we will go through DP-3T while modeling it using the Verifpal Language, and conclude by comparing our results to the designers’ security goals.

Modeling DP-3T

To demonstrate DP-3T, we will assume that the principals participating in this simulation are the following:

  • A population of 3 individuals: Alice, Bob, and Charlie, each of them possessing a smartphone: SmartphoneA, SmartphoneB, and SmartphoneC respectively;
  • A Healthcare Authority serving this population;
  • A Backend Server, that individuals can communicate with to obtain daily information.

After installing Verifpal, we can start by creating a new model called “dp-3t.vp” in which we begin by defining an attacker which matches with our security model. In this case we will be using an active attacker (i.e. one that can not only monitor but also intercept and overwrite unprotected messages on the network):

attacker[active]

We then proceed to illustrate our model as a sequence of days in which DP-3T is in operation within the lifecycle of a pandemic.

Day 0 (setup phase)

We assume that no new individuals were diagnosed with the disease on Day 0 of using DP-3T. This means that the Healthcare Authority and the Backend Server will not act at this stage and we can simply ignore them for now.

The DP-3T specification states that every principal, when first joining the system, should generate a random secret key (SK) to be used for one day only. For every SK value, and the knowledge of a public “broadcast key” value, principals should compute multiple Unique Ephemeral ID values (EphID) using a combination of a PRG and a PRF. The method of generating EphID is analogous with the HKDF function from Verifpal. We could add the following lines of code to our file in order to model Alice’s SmartphoneA:

// All lines that start with "//" are treated as comments and ignored by Verifpal
// A principal block looks like the following
principal SmartphoneA[
	// In the line below we state that Alice knows the public BroadcastKey
	
	knows public BroadcastKey
	
	// SK is going to be a secret random value
	// To define it we use the "generates" keyword
	// We will use the following template for SK variable names
	// SK[day number][principal initial]
	
	generates SK0A
	
	// We will use the following template for EphID variable names
	// EphID[day number][value number][principal initial]
	
	EphID00A, EphID01A, EphID02A = HKDF(nil, SK0A, BroadcastKey)
]

The same thing goes for Bob, and Charlie:

principal SmartphoneB[
	knows public BroadcastKey
	generates SK0B
	EphID00B, EphID01B, EphID02B = HKDF(nil, SK0B, BroadcastKey)
]

principal SmartphoneC[
	knows public BroadcastKey
	generates SK0C
	EphID00C, EphID01C, EphID02C = HKDF(nil, SK0C, BroadcastKey)
]

Whenever two principals would come be in physical proximity of each other, they would automatically exchange EphIDs. Once a principal uses an EphID value, they discard it and use another one when performing an exchange with another principal.

Let’s imagine that Alice and Bob came into contact. It would mean that Alice sent EphID00A in a message to Bob and that Bob sent EphID00B to Alice:

Here is how the above message exchange is modeled in Verifpal:

// Sender -> Recipient : Name of Value

SmartphoneA -> SmartphoneB: EphID00A
SmartphoneB -> SmartphoneA: EphID00B

Now, let’s say that in the conclusion of Day 0, Bob sits behind Charlie in the Bus:

Modeling this is equally simple:

SmartphoneC -> SmartphoneB: EphID01C
SmartphoneB -> SmartphoneC: EphID01B

Day 1

On Day 1, the Backend Server will automatically publish the SK values of people who were infected to the members of the general population. These values were previously unpublished and thus were private and only known by their generators and the server.

// A server is just like any other principal

principal BackendServer[
	// Let's assume that infectedPatients0 is the list of infected patients on day 0
	knows private infectedPatients0
]

BackendServer -> SmartphoneA: infectedPatients0
BackendServer -> SmartphoneB: infectedPatients0
BackendServer -> SmartphoneC: infectedPatients0

We should not forget that every day starting from Day 1, DP-3T mandates that principals will generate new SK values. The new value will be equal to the hash of the SK value from the day before. Principals will also generate EphIDs just like before.

principal SmartphoneA[
	SK1A = HASH(SK0A)
	EphID10A, EphID11A, EphID12A = HKDF(nil, SK1A, BroadcastKey)
]

principal SmartphoneB[
	SK1B = HASH(SK0B)
	EphID10B, EphID11B, EphID12B = HKDF(nil, SK1B, BroadcastKey)
]

principal SmartphoneC[
	SK1C = HASH(SK0C)
	EphID10C, EphID11C, EphID12C = HKDF(nil, SK1C, BroadcastKey)
]

Thankfully, Alice, Bob and Charlie are committed to self-confinement and have stayed at home, so they did not exchange EphIDs with anyone.

Day 2

On Day 2, a similar sequence of events takes place. Since it is sufficient to define the values that we will need later on in our model, we will just define a block for Alice.

principal SmartphoneA[
	SK2A = HASH(SK1A)
	EphID20A, EphID21A, EphID22A = HKDF(nil, SK2A, BroadcastKey)
]

Fast-Forward to Day 15

Unfortunately, Alice tests positive for COVID-19. Since this breaks the routine that happened between Day 1 and Day 15, we will announce a new phase in our protocol model:

phase[1]

Alice decides to announce her infection anonymously using DP-3T. This means that she will have to securely communicate SK1A (her SK value from 14 days ago) to the Backend Server, using a unique trigger token provided by the healthcare authority. Assuming that the Backend Server and the Healthcare Authority share a secure connection, and that a private key encryption key ephemeral_sk has been exchanged off the wire by the Healthcare Authority, Alice, and the Backend Server, the Healthcare Authority will encrypt a freshly generated triggerToken using ephemeral_sk and send it to both Alice and the Backend Server.

principal HealthCareAuthority[
	generates triggerToken
	knows private ephemeral_sk
	m1 = ENC(ephemeral_sk, triggerToken)
]

// The brackets around m1 here mean that the value is guarded
// ie: an active attacker cannot inject a value in its place

HealthCareAuthority -> BackendServer : [m1]
HealthCareAuthority -> SmartphoneA : m1

Then, Alice would have to use an AEAD cipher to encrypt SK1A using ephemeral_sk as the key and triggerToken as additional data and send the output to the Backend Server. Note that Alice can only obtain triggerToken after decrypting m1 using ephemeral_sk.

principal SmartphoneA[
	knows private ephemeral_sk
	m1_dec = DEC(ephemeral_sk, m1)
	m2 = AEAD_ENC(ephemeral_sk, SK1A, m1_dec)
]

SmartphoneA -> BackendServer: m2

The Backend Server will now have to decrypt m1 to receive the triggerToken in the same way that Alice did, then attempt to decrypt m2. If that decryption was successful, the server would obtain SK1A and would be sure that the value came from Alice because it is only Alice who knows both triggerToken and SK1A at the same time as defined in the protocol.

Finally, the Backend Server will add SK1A to the list of infected patients previously defined, and then send this list to all of the individuals in this community.

principal BackendServer [
	knows private ephemeral_sk
	m2_dec = AEAD_DEC(ephemeral_sk, m2, DEC(ephemeral_sk, m1))?
	infectedPatients1 = CONCAT(infectedPatients0, m2_dec)
]

BackendServer -> SmartphoneA: infectedPatients1
BackendServer -> SmartphoneB: infectedPatients1
BackendServer -> SmartphoneC: infectedPatients1

Everything that happened in Day 15 can be summarized in the following diagram:

Queries

Now, we may finally define the queries block, in which we ask Verifpal about the state of certain security guarantees that we expect from the protocol.

SinceSK1A is now shared publicly, the DP-3T software running on anyone’s phone should be able to re-generate all EphID values generated by the owner of SK1A starting from 14 days prior to the day of diagnosis. These values would then be compared them with the list of EphIDs they have received. Everyone who came in contact with Alice will therefore be notified that they have exchanged EphIDs with someone who has been diagnosed with the illness without revealing the identity of that person.

queries[
	// Would someone who shared a value 15 days before they got tested get flagged?
	// ie in phase[0], before phase[1]
	confidentiality? EphID02A
	// Will people who came in contact with Alice be able to compute
        // all of Alice's EphIDs starting from Day 1
	confidentiality? EphID10A
	confidentiality? EphID11A
	confidentiality? EphID12A
	confidentiality? EphID20A
	confidentiality? EphID21A
	confidentiality? EphID22A
	// Is the server able to Authenticate Alice as the sender of m2
	authentication? SmartphoneA -> BackendServer: m2
]

The results of our initial modeling in Verifpal suggest to us the following:

  • No EphIDs generated by Alice are known by any parties before Alice announces her illness.
  • EphID02A remains confidential even after Alice declaring her illness. Note that it was generated 15 Days before Alice got tested.
  • All of the following values EphID10A, EphID11A, EphID12A, EphID20A, EphID21A, EphID22A have been recoverable by an attacker in phase[1] after Alice announces her illness.

These results come in line with what is expected from the protocol. We note that the security of communication channels between Healthcare Authorities, Backend Servers, and Individuals have not been defined, and we have placed our hypothetical own security conditions with in order to focus on quickly sketching the DP-3T protocol. Further analysis will be required in order to better elucidate the extent of the obtained security guarantees.

Generating Models for Further Analysis in ProVerif and Coq

Verifpal generating ProVerif models live from the Verifpal model, through the Verifpal Visual Studio Code extension.

We’re very excited to be working on automatically generating ProVerif and Coq models directly from Verifpal models. The resulting ProVerif and Coq models will be human-readable and thus easily extensible, allowing for more profound protocol analysis and supplementing Verifpal’s insight with that of tools that have existed for more than two decades.

In working on DP-3T, we were able to generate baseline ProVerif and Coq models after less than an hour of work on the Verifpal model itself. This is an immeasurably huge leap forward in terms of obtaining working material for the formal modeling and analysis of a novel protocol, and we are very excited to post further updates as this new feature matures in Verifpal.

ProVerif and Coq model generation is currently under development, and we expect a beta release to be ready by the end of April.

Coming soon!