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.
Selected reports
Payment settlement
4Mica
We audited 4Mica's BLS-signed payment guarantees and on-chain settlement. The cryptography was correct; the serious risks were in settlement and key management.
View report (PDF): 4MicaPost-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
Security
Audits
Protocol design, cryptographic implementations, threat models, and formal analysis.
300+ engagements since 2017
Software
Tools
Verifpal, Crucible, hpke-ng, Kyber-K2SO, and the Post-Quantum Migration Playbook.
Source and releases
Course
Teaching
Applied Cryptography, an 18-topic university course with open materials.
Summer 2026 course
Writing
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. We have run it against 19 implementations in 7 languages.
View on GitHubtests 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
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.
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.
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.
Teaching and community
Our university course publishes its materials freely. Cedarcrypt brings applied-cryptography teaching and research together with the IACR.