Verifpal Takes on TLS 1.3
An overnight analysis, nineteen security queries, and three expected counterexamples: modeling TLS 1.3 with concurrent sessions, malicious certified peers, completion preconditions, and staged key compromise.
Read →Design-level security
for the AI era.
Symbolic Software is an independent applied-cryptography consultancy. We review protocols, cryptographic designs, threat models, formal models, and implementations.
attacker[active]
principal Alice[
generates a
ga = PUBKEY(a)
]
Alice → Bob: ga
principal Bob[
generates m1, b, n
gb = PUBKEY(b)
gab = DH_KEX(ga, b)
e1 = AEAD_ENC(gab, n, m1, nil)
]
Bob → Alice: gb, n, e1
principal Alice[
kab = DH_KEX(gb, a)
m1_a = AEAD_DEC(kab, n, e1, nil)?
]
protocol diagram
2 actors · 2 messages
queries — security goals
✗
confidentiality?
m1
ATTACK FOUND
✗
authentication?
Bob → Alice: e1
ATTACK FOUND
attacker[active]
principal Alice[
generates a
ga = PUBKEY(a)
]
Alice → Bob: [ga]
principal Bob[
generates m1, b, n
gb = PUBKEY(b)
gab = DH_KEX(ga, b)
e1 = AEAD_ENC(gab, n, m1, nil)
]
Bob → Alice: [gb], n, e1
principal Alice[
kab = DH_KEX(gb, a)
m1_a = AEAD_DEC(kab, n, e1, nil)?
]
protocol diagram
2 actors · 2 messages
queries — security goals
✓
confidentiality?
m1
PASS
✓
authentication?
Bob → Alice: e1
PASS
attacker[active]
principal Alice[
generates a
ga = PUBKEY(a)
]
Alice → Bob: ga
principal Bob[
generates m1, b, n
gb = PUBKEY(b)
gab = DH_KEX(ga, b)
e1 = AEAD_ENC(gab, n, m1, nil)
]
Bob → Alice: gb, n, e1
principal Alice[
kab = DH_KEX(gb, a)
m1_a = AEAD_DEC(kab, n, e1, nil)?
]
protocol diagram
2 actors · 2 messages
queries — security goals
✗
confidentiality?
m1
ATTACK FOUND
✗
authentication?
Bob → Alice: e1
ATTACK FOUND
Security has to start at the design level.
We review the threat model, protocol, primitive choices, formal models, and implementation. More than 250 engagements since 2017 have followed that approach.
Our practice areas
01 / SECURITY
Audits
Protocol design, cryptographic implementations, threat models, and formal analysis.
○ Mozilla · 1Password · Coinbase
○ Zoom · Bitwarden · MetaMask
250+ engagements since 2017 →
02 / SOFTWARE
Tools
Verifpal, Crucible, hpke-ng, Kyber-K2SO, PQ Migration Playbook.
$ verifpal verify tls13.vp
→ ✓ no attack found · 0.34s
Source and releases →
03 / COURSE
Teaching
Applied Cryptography, an 18-topic university course with open materials.
∫ provable security
⊕ TLS · ZK · PQC · MPC
Summer 2026 course →
04 / WRITING
Blog
Audit reports, security advisories, software releases, papers, and essays.
Researchpapers
Securityreports
Read the blog →
Crucible.
ML-KEM and
ML-DSA tests.
Crucible runs 129 conformance tests across 12 categories. Each test cites the relevant FIPS section and, where applicable, the audit finding that prompted it.
129tests
12categories
19implementations tested
7languages supported
tests available
129 / 129
78 ML-KEM
51 ML-DSA
kem/compression12 tests
kem/ntt21 tests
kem/bounds9 tests
kem/decapsulation12 tests
kem/serialization12 tests
kem/sampling12 tests
dsa/norm-checks9 tests
dsa/arithmetic9 tests
dsa/signing9 tests
dsa/verification9 tests
dsa/serialization9 tests
dsa/timing6 tests
Writing
How Verifpal Finds a 3-of-5 Threshold-Signature Forgery
A walkthrough of Verifpal 1.4.4's FROST-shaped model: two signing oracles and one leaked share cross a 3-of-5 threshold, producing a valid signature without disclosing the group key.
Read →Verifpal 1.4: More Accurate Protocol Analysis
Verifpal 1.4 fixes false positives caused by combining incompatible protocol runs, detects two previously missed attacks, corrects precondition semantics, adds clearer verdict labels, gives AEAD a nonce so that nonce reuse can be modelled, and removes password-specific syntax.
Read →The program
1Welcome & FoundationsMon, Jul 13
2Applied Cryptography in PracticeTue, Jul 14
3Protocols & PrimitivesWed, Jul 15
4Advanced Constructions & ClosingThu, Jul 16