Documentation / Introduction
Introduction
Start with a story from VerifCity, then learn how symbolic models help you check a cryptographic protocol.
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?
A cryptographic protocol should protect messages from disclosure and impersonation. Some protocols also protect past or future messages when a key is compromised. These properties depend on how the protocol combines cryptographic operations, which keys each participant trusts, and what it checks before accepting a message.
In Verifpal, you describe the protocol in a model: name the participants, specify what they know and send, and write the security properties to check. Verifpal searches for attacks against those properties and reports the steps of each attack it finds.
You need some familiarity with encryption, hashes, Diffie–Hellman and signatures. You do not need a background in formal methods.
A symbolic model
A model describes cryptographic operations using fixed symbolic rules. For example, a ciphertext can be decrypted with its matching key, and a signature can be checked against its message and public key. These rules describe the protocol’s logic. They omit byte lengths, timing, implementation bugs and computational probabilities.
You choose an active or passive attacker and specify trust assumptions, key disclosures and any weakened primitives. Results depend on these choices. A query passes when the search finds no contradiction within its limits. When a query fails, the trace shows how its condition was violated.
The analysis guide explains the search and its limits, and the research paper gives formal definitions. See the comparison for the differences between Verifpal, ProVerif and Tamarin.
Find your starting point
- Run your first analysis
- Model a signed challenge, find an attack and test a repair in your browser.
- Look up the language
- Search declarations, queries, primitive interfaces and their symbolic rules.
- Build your own model
- Define the participants, messages and assumptions needed to test a security claim.
- 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.