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 consultancy
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
1Security
Audits
Protocol design, cryptographic implementations, threat models, and formal analysis.
300+ engagements since 2017
2Software
Tools
Verifpal, Crucible, hpke-ng, Kyber-K2SO, and the Post-Quantum Migration Playbook.
Source and releases
3Course
Teaching
Applied Cryptography, an 18-topic university course with open materials.
Summer 2026 course
4Writing
Blog
Audit reports, security advisories, software releases, papers, and essays.
Read the blog
Conformance testing
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
Recent posts
Writing.
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 →Meet the Symbolic Software Summer 2026 Team
Five people joined us this summer: two research interns formalizing zkVM soundness bounds in Lean, and three teaching assistants running the Applied Cryptography course. Here they are, in their own words.
Read →Why I Teach Cryptography in Lebanon
Cedarcrypt's first edition has concluded. On what a year of teaching cryptography in and for Lebanon has meant, why the conference met in Cyprus rather than Beirut, and the decades of work ahead.
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.