Key management
1Password
With Cure53, we reviewed key rotation, vault security under server compromise, and public-key validation in 1Password B5.
View report (PDF) : 1PasswordIndependent applied cryptography
Design-level security for the AI era.
A correct implementation can still implement an unsafe design. We review your protocol, threat model, and cryptographic code to find weaknesses before they become part of your product.
300+ engagements. Every engagement is led by a senior cryptographer.
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
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
Security has to start at the design level.
We review the threat model, protocol, primitive choices, formal models, and implementation. More than 300 engagements since 2017 have followed that approach.
Public work
See what our reviews uncover.
Threshold signatures
dWallet Labs
With 3MI Labs, we identified critical nonce reuse during presigning by comparing the Rust implementation with the 2PC-MPC protocol.
View report (PDF) : dWallet LabsPost-quantum libraries
CE Labs libcrux
We published five findings in libcrux and analyzed the gaps between the code, Cryspen's hax pipeline, and the library's verification claims.
Read the series : CE Labs libcruxSymbolic Software is run by an accomplished researcher, with significant contributions in the area of applied cryptography. They're the right team for projects that require rigorous design and engineering.
Our practice areas
01 / Security
Audits
Protocol design, cryptographic implementations, threat models, and formal analysis.
300+ engagements since 2017
02 / Software
Tools
Verifpal, Crucible, hpke-ng, Kyber-K2SO, and the Post-Quantum Migration Playbook.
Source and releases
03 / Course
Teaching
Applied Cryptography, an 18-topic university course with open materials.
Summer 2026 course
04 / Writing
Blog
Audit reports, security advisories, software releases, papers, and essays.
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
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 →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 →Teaching and community
Applied cryptography, taught in public.
Our university course publishes its materials freely. Cedarcrypt brings applied-cryptography teaching and research together with the IACR.