Trail of Bits fixes mermaid-to-proverif, which read ProVerif's results backwards

Trail of Bits has fixed mermaid-to-proverif, the skill that turns a Mermaid sequence diagram of a cryptographic protocol into a ProVerif model. It read the ProVerif reachability check backwards. So a correct model looked broken, and a broken model looked fine. If you have formally verified a protocol with this skill, those verdicts are worth a second look.

ProVerif checks whether an event can happen by trying to prove it never does. So when the event is reachable, it prints "not event, is false." The skill told the model that false meant a structural bug. Now false is the good case, and true means the event never fires.

That check is the skill's first query. If the protocol's last step can't be reached, every secrecy and authentication result after it is meaningless. With the reading flipped, a stuck model passed that check. The skill, both of its reference files and its example all carried the backwards reading, five places in total.

The forward secrecy pattern had a second problem. It handed both long-term keys to the attacker at the very start, so the attacker could impersonate either side, and secrecy failed for every authenticated protocol. Now the keys leak after the sessions finish, and on the example both secrecy queries hold.

The example the skill teaches from had a finding of its own. Its handshake has no challenge from the responder, so replaying the first message completes another responder session, and the replay check fails. The weaker authentication property holds. The example now reports that replay as a real finding.

The models the skill writes are unchanged. What changed is how it reads ProVerif's answers, and how it tests forward secrecy. A new test keeps that guidance matched to ProVerif's output, and only runs ProVerif itself where it is installed. The update ships in the trailmark plugin, which loads in Claude Code and in Codex.