Design-level security
for the AI era.
An applied cryptography practice. We audit the layer above implementation: protocol architecture, primitive selection, threat modeling, formal verification. AI bug-finders do not work at that layer.
attacker[active]
principal Alice[
knows public c0
generates a
ga = PUBKEY(a)
]
Alice → Bob: ga
principal Bob[
knows public c0
generates m1, b
gb = PUBKEY(b)
gab = DH_KEX(ga, b)
e1 = AEAD_ENC(gab, m1, c0)
]
Bob → Alice: gb, e1
protocol diagram
2 actors · 2 messages
queries — security goals
✗
confidentiality?
m1
ATTACK FOUND
✗
authentication?
Bob → Alice: e1
ATTACK FOUND
attacker[active]
principal Alice[
knows public c0
generates a
ga = PUBKEY(a)
]
Alice → Bob: [ga]
principal Bob[
knows public c0
generates m1, b
gb = PUBKEY(b)
gab = DH_KEX(ga, b)
e1 = AEAD_ENC(gab, m1, c0)
]
Bob → Alice: [gb], e1
protocol diagram
2 actors · 2 messages
queries — security goals
✓
confidentiality?
m1
SECURE
✓
authentication?
Bob → Alice: e1
SECURE
attacker[active]
principal Alice[
knows public c0
generates a
ga = PUBKEY(a)
]
Alice → Bob: ga
principal Bob[
knows public c0
generates m1, b
gb = PUBKEY(b)
gab = DH_KEX(ga, b)
e1 = AEAD_ENC(gab, m1, c0)
]
Bob → Alice: gb, e1
protocol diagram
2 actors · 2 messages
queries — security goals
✗
confidentiality?
m1
ATTACK FOUND
✗
authentication?
Bob → Alice: e1
ATTACK FOUND
2026.08.26
Verifpal 1.3: Who Alice Thinks She's Talking To
2026.08.15
Verifpal Reaches 1.0: A Toy Becomes an Instrument
2026.08.08
Verifpal 0.80.0: Nuancing Weak Cryptography Modeling and Witness-Based Unlinkability
2026.08.05
Verifpal 0.70.0: Post-Quantum Key Exchange, and an Attacker That Works Backwards
Security has to start at the design level.
Protocol architecture, primitive selection, threat modeling, formal verification: everything downstream is a consequence of those decisions. More than 250 engagements since 2017 have started from that premise.
Our practice areas
01 / SECURITY
Audits
Protocol architecture, cryptographic review, threat modeling, formal verification.
○ Mozilla · 1Password · Coinbase
○ Zoom · Bitwarden · MetaMask
250+ engagements →
02 / SOFTWARE
Tools
Verifpal, Crucible, hpke-ng, Kyber-K2SO, PQ Migration Playbook.
$ verifpal verify tls13.vp
→ ✓ verified · 0.34s
open source →
03 / COURSE
Teaching
Applied Cryptography. Free for 50 Lebanese students this summer.
∫ provable security
⊕ TLS · ZK · PQC · MPC
2026 cohort in session →
04 / RESEARCH
Lab
Post-Quantum Migration Playbook, advisories, papers, the audit floor.
PQ Playbook3247×
Advisories shipped12
new: PQ Playbook →
From the audit floor
Recurring bug classes from our audit work, with client details removed.
Constant-time leak in ECC point doubling
AEAD nonce reuse under concurrent state
Incorrect rounding in lattice solver
Public key not validated to correct subgroup
Unchecked length field in TLV parser
Crucible.
Bug classes,
encoded as tests.
129 tests across 12 categories, each tagged with the bug class, the FIPS spec section, and the audit it came from. Wire any ML-KEM or ML-DSA implementation up over stdin/stdout and get a pass or fail in seconds.
129tests
12categories
19implementations tested
7languages supported
tests passed
127 / 129
98.4% pass
2 fail
kem/compression12/12
kem/ntt21/21
kem/bounds8/9
kem/decapsulation12/12
kem/serialization12/12
kem/sampling12/12
dsa/norm-checks9/9
dsa/arithmetic9/9
dsa/signing9/9
dsa/verification9/9
dsa/serialization8/9
dsa/timing6/6
From the lab
Verifpal 1.3: Who Alice Thinks She's Talking To
Verifpal 1.3 adds peer scenarios, which instantiate a principal's counterparty differently across concurrent runs. That is what finally lets Verifpal find Lowe's attack on Needham-Schroeder and tell that protocol apart from its fix. Alongside it, every passing query now prints the envelope it was reached under, --saturate raises the session count until verdicts stop moving, and --auto-queries generates a query set from the model.
Read →Verifpal Reaches 1.0: A Toy Becomes an Instrument
Verifpal 1.0 removes the beta warning the tool has printed with every analysis since 2020, on the strength of a new paper. The language now covers post-quantum key exchange, declared weakening assumptions, witness-based unlinkability, and two concurrent sessions of every principal; the engine behind it comes with a soundness theorem that holds however the solver behaves, unconditional termination, and attack traces measured for readability against ProVerif and Tamarin.
Read →Verifpal 0.80.0: Nuancing Weak Cryptography Modeling and Witness-Based Unlinkability
Verifpal 0.80.0 lets a model declare that a particular piece of cryptography is broken (weak, forgeable, and from a chosen phase onward) instead of approximating the break with a list of leaked values, and decides unlinkability queries by searching for a concrete link witness that it then reports back to you.
Read →The program
1Welcome & FoundationsMon, Jul 13
2Applied Cryptography in PracticeTue, Jul 14
3Protocols & PrimitivesWed, Jul 15
4Advanced Constructions & ClosingThu, Jul 16