Fear and Loathing in Protocol Analysis


Over at the Symbolic Software blog, I recently published a post celebrating Verifpal’s one-year anniversary and discussing in detail what it was that Verifpal has achieved in the past year in terms of three categories: usability, features and reliability. I also discussed how I saw Verifpal’s positioning in the protocol analysis space, and its future goals, so that people understand what the Verifpal aims to do (and more importantly, what it doesn’t aim to do).

What I didn’t mention in that post are some pretty dark experiences that I’ve had in my first year of working on Verifpal. Earlier in my life, I’ve been told to be quiet when people in my field are prejudicial or unfair towards either myself or work I’ve done, because otherwise I’d only be making the problem worse. As I’ve learned, that often meant only exchanging short-term relief for an assured long-term disaster, as those who did get away with their bullshit only felt further vindicated, empowered, and were given a bigger breathing room by my silence in order to define my work and even my self on their own terms.

In this post I’ll briefly summarize some of the more rotten experiences I’ve had working on Verifpal in the past year. Take it as the dark underbelly of that other post on the Symbolic Software blog, which is the one you should be reading if you’re purely interested in the more professional details. I don’t feel like I should stay quiet when dealing with so much bullshit from my field on a regular basis, continuously lobbed by people who never come close to being held accountable for it.

Private Sector: Zoom used Verifpal and lobbed public insults when I asked for a citation

In May of this year, Max Krohn from Zoom (previously Keybase) reached out and asked for help in analyzing Zoom’s new protocols using Verifpal. Here’s a PDF of all of our Twitter DMs. Over the span of a week, I helped Max look at eight Verifpal models. In one instance, we had a Signal call (that I wish I had recorded) in order to discuss a flaw that Verifpal had found and that Max’s team wasn’t able to understand how to spot and fix. The flaw was real, non-obvious and led to an attack on the protocol. Zoom’s team spotted it and fixed it because of Verifpal.

Zoom published their whitepaper without mentioning the Verifpal work or citing Verifpal, which flew in direct opposition to what Max Krohn promised me over the phone. Another Zoom team member also confirmed this:

I had a second Signal call with Max who again promised that Verifpal would be cited once some feedback Max had was implemented. Naturally, I haven’t heard back from Max or his team since; except, I did hear back from Lea Kissner, then co-leading Zoom’s end-to-end encryption effort and now recently hired at Apple, who attempted to assasinate my character on Twitter when I asked questions about Zoom’s end-to-end encryption:

Nobody else from Zoom (Max, etc.) had anything to add at that point. Despite working with them for over a week, having two conference calls, poring over eight models and identifying an actual non-obvious attack using Verifpal, all I got from Zoom were implicit threats, and Verifpal was never cited or credited in any of their published work.

Ultimately, NLnet, the organization that’s very kindly funded Verifpal research over the past year, published a post in which we discussed Verifpal’s contributions to Zoom – instead of having any input from Zoom on that post, I was worried that we’d hear from their lawyers the entire time.

Academia: Researchers in the domain openly displayed personal prejudice when evaluating Verifpal and were defended by other researchers

A couple of weeks ago, I sent an email on a mailing list dedicated to formal verification research touting Verifpal in a comedic fashion and sharing what we’ve accomplished over the first year. The lead developer of one of the oldest protocol analysis tools (dating over two decades) responded in the following fashion:

When I pointed out that the “counter-example” wasn’t a counter-example, and that this researcher was baselessly proselytizing their methodology as the only correct one, and ignoring all of our recent soundness/reliabiltiy work in order to attack me personally, I made sure to refer to what this researcher was saying as “bullshit” because, well, it was, and I felt that they needed to hear it.

Two of their co-researchers then privately emailed me, with a tone of panicked urgency, to explain to me the following:

Both of those co-researchers made sure to loudly proclaim their allegiance to the original researcher and to express great shock and disbelief at how I chose to point out all of the bullshit that the original researcher had written. Never mind that they had demonstrably showed that they were treating my work with prejudice and coming to conclusions without evaluating it. Never mind that their colleagues were resorting to racist tropes to defend them. The most egregious issue according to that group was that I had dared to call all of that “bullshit” in an email that otherwise was a perfectly correct point-by-point fisking of the researcher’s misplaced critiques and a defense of my work. None of these three researchers ever said a word about my defense of my work or of my discrediting of any unfair criticism addressed towards it.

So, I packed and left. Edit: some readers have wondered why I am anonymizing the researchers here, unlike how I wrote the Zoom section of this post. The reason is that some of these researchers are people I know to have anxiety issues, and I do not want to cause them problems by unnecessarily naming them in public.

The sad thing is that this same researcher had previously found valid bugs in Verifpal, which I had fixed. It was interesting to learn that what I thought were bugs being found in good faith turned out to be likely bugs that I was being sent out of anger and most likely a method of discouragement for further work in the field.

In a separate instance, a researcher working on another, unrelated protocol analysis tool publicly reproached me after I incorrectly claimed on Twitter that Verifpal was likely the first protocol analysis tool to accomplish multi-threaded analysis. It turned out that that wasn’t true, and I hastily corrected my mistake and apologized. I later found out that that same researcher had, in addition to politely pointing this out to me on Twitter, spent hours of their life dissing Verifpal and insulting me personally on a private Slack channel, which is odd given my complete willingness to go for a public correction.

All of the researchers mentioned above are people who I’ve copiously cited, thanked and listed as sources of inspiration in my work. I leave it as an exercise to the reader to figure out why they felt it was appropriate to finally let their bellies out and reveal all of the hidden prejudice that they’ve kept secret for so long.

All of this was only the first year of a new project

I’ve decided to start publicly documenting instances like this when they happen with Verifpal after not doing so with previous projects and work. I’ve regretted not doing so, as it seems to embolden people to abuse and take advantage of more junior and less reputable people in their field.

I don’t look forward to any future instances of abusive treatment, but do look forward to documenting them in similar posts should the case arise.