Documentation / Introduction
Introduction
Learn to ask precise questions about cryptographic protocols. First, a story from VerifCity.
A case in VerifCity
A math teacher, a suspicious mayor, and an alarming key schedule. The original eight-page Verifpal manga, by Collateral Damage Studios.
Read page 1 as text
Credits: Michelle Tan and Cardi Chow, artists. Low Zi Rong, art lead and character design. Nadim Kobeissi, writing, storyboarding and direction.
Narrator: VerifCity 20xx. A new era is dawning on VerifCity. An era where everything happens through smartphones.
Messages: “OK, sure!” “Cool! See ya soon!”
Narrator: Friendships, breakups, elections, checkups, bank accounts… Everything goes through a single window into people’s lives.
Read page 2 as text
Narrator: VerifCity’s leader, Mayor N. D. Middle, promised everyone that their digital lives would have full privacy. But instead, he poisoned VerifCity’s communication protocols, letting him monitor everyone.
Private messages pass through the compromised network.
Narrator: Ever since his election, people’s lives have been at risk of exposure. Nobody knows where it’s coming from, or when it will stop. Well, almost nobody.
Read page 3 as text
Teacher: OK, everyone! Class dismissed!
Narrator: By day, she is a math teacher at VerifCity High School. By night, she is… Verifpal, the hero who can expose the mayor’s hidden tyranny.
Read page 4 as text
Verifpal: So… this is supposed to be the secure protocol everyone is using to communicate… I’m sure I’ve modeled it correctly… Alice’s ephemeral key… it’s the only thing keeping her messages safely encrypted… But something’s not right…
Years earlier. ProVerif: No, Verifpal. A compromised ephemeral key can still mean trouble.
Verifpal: But ProVerif-sama! The long-term keys have mutual authentication!
ProVerif: So, have you checked if the authentication is chained down past the key exchange messages?!
Read page 5 as text
Verifpal: That’s right! Normally, message keys are derived not only from Alice’s ephemeral key, but also from a root key… This is what ties the messages to Alice and Bob’s identities… But… the root key is never getting mixed into Alice’s new message encryption key!
The diagram shows a master secret feeding a root key through HKDF. The missing connection should mix that root key with Alice’s ephemeral contribution to derive the encryption key.
Verifpal: Which means… if an active attacker replaces the ephemeral key, the entire session gets compromised! They can read everything!
Read page 6 as text
Mayor: Excellent deduction as always, Verifgal!
Verifpal: Mayor N. D. Middle!
Mayor: Indeed, the key exchange is quite worthless… but did you think that was the only ace up my sleeve?!
Verifpal: No, I didn’t…
Read page 7 as text
Verifpal: Even if communications were confidential… you’d still learn a lot from who’s talking to who… isn’t that, Mayor, why you don’t… encrypt the initiator’s long-term public key?!
Mayor: IM-IMPOSSIBLE!!!
Read page 8 as text
The next day. Headlines: Hero reveals communications surveillance. Interest in learning formal verification spikes. City mayor arrested for surveillance plot. Population confused as to how name was not sufficient tip-off.
Citizens: How didn’t we see that? The encryption… it wasn’t secure! Why didn’t we spot it?
Verifpal: Secure communications are critical to our daily lives… and everyone should be able to verify the security of these designs. My name is Verifpal! Together, we can learn formal verification for any cryptographic protocol! It’s nice to meet you; let’s get started!
Read left to right. Use the arrow keys or swipe to turn the page. Art credits.
Why verify a protocol?
Cryptographic protocols determine who can read a message, who can impersonate a participant, and what survives a compromised key. Secure primitives alone do not answer those questions. Their arrangement, the information each participant trusts, and the checks performed before accepting a message all matter.
Verifpal lets you write that arrangement as a small model. You name the participants, describe what they know and send, and ask specific security questions. The verifier searches for ways an attacker could contradict your claims and explains its findings through attack traces.
Built around the person writing the model, Verifpal assumes familiarity with encryption, hashes, Diffie–Hellman and signatures, but no background in formal methods.
A symbolic model
A model represents cryptographic operations through fixed symbolic rules. A ciphertext can be opened with its matching key; a signature can be checked against its message and public key. This abstraction makes protocol logic manageable while omitting byte lengths, timing, implementation bugs and computational probabilities.
You choose an active or passive attacker, express the deployment’s trust assumptions, and declare any key disclosures or weakened primitives. The result concerns that model and those assumptions. A passing query means that the implemented search found no contradiction within its limits. A failing query must be understood through its exact predicate and supporting trace.
The analysis guide explains the search and its limits. The research paper supplies formal definitions. The comparison explains when Verifpal, ProVerif or Tamarin fits the task.
Find your starting point
- Run your first analysis
- Write a signed challenge, find the attack and change the trust assumption. Everything runs in the browser.
- Look up the language
- Search declarations, queries, primitive interfaces and their symbolic rules.
- Build your own model
- Translate a security claim into principals, messages, phases and peer scenarios, then work through focused experiments.
- Study a complete protocol
- Follow Signal, Scuttlebutt and a hybrid post-quantum exchange through their models, variants and results.
- Use the command line
- Export reports, compare session counts, automate checks and diagnose surprising results. Installation and editor integrations are on the software page.