Security proofs for cryptographic protocols
Formal analysis of cryptographic protocols to establish precise security guarantees under clearly defined adversary and hardness assumptions.
Security proofs define what security means for your protocol, specify the attacker’s capabilities, and show—via mathematical reduction—that breaking the protocol would be as hard as solving well-studied computational problems. This makes assumptions and guarantees explicit, rather than relying on intuition or the absence of known attacks.
TRUSTED BY:
TRUSTED BY:
Veridise was engaged by Monero to validate and strengthen the soundness guarantees behind a cryptographic proof technique used in privacy-focused protocols. We reviewed the existing proof approach, found a subtle gap that could appear in real implementations, and delivered a hardened proof with clearly stated assumptions and quantitative security bounds.
Meet Alp Bassa:Leading cryptography at Veridise
I’m Alp, and I lead cryptography at Veridise. I previously served as a professor and have spent over two decades working in mathematics and cryptography.
My background includes number theory, algebraic geometry, algebraic curves over finite fields, modular curves, the arithmetic of function fields, algebraic surfaces, line arrangements, and applied cryptography.
At Veridise, I lead our cryptography research and security proof efforts, helping teams rigorously justify the security claims behind new or modified protocols.
If you’re building or modifying a cryptographic protocol, I’d love to hear about it and explore how we can think about its security together.
What are security proofs?
The Veridise difference: Why us?
Seasoned professionals
Veridise is composed of a team of seasoned security professionals, blending the latest research insights from academia with extensive industry expertise.
In-house tooling
In addition to rigorous human auditing, our in-house tools detect bugs that the human eye has a difficult time finding. This enhances the quality and effectiveness of our audits.
Confidentiality and ownership
Upon request, we uphold the confidentiality of the report, although many of our clients find value in publishing it. Additionally, our reports become fully yours upon completion of the audit, unlike with some other providers.
Veridise’s edge: our in-house security tools
Veridise combines professionals who manually review code with our in-house tools.
Our in-house tools enable us to detect hard-to-find bugs that are difficult for the human eye to identify.
OrCa
Specification-guided fuzzer
Vanguard
Static analysis tool for smart contracts and ZK circuits
Picus
Zero-Knowledge Proof auditing tool finding bugs in arithmetic circuits
Special considerations with Security Proofs
A security proof is a mathematical argument that demonstrates what security guarantees a cryptographic protocol provides, under clearly defined assumptions about the adversary and the environment in which the protocol operates. Rather than relying on intuition or the absence of known attacks, a security proof makes precise statements about what it means for a system to be secure and why those guarantees hold.
At the foundation of any security proof is a formal definition of security. What does it mean for an encryption scheme to be secure? What does it mean for a digital signature to be unforgeable? What does it mean for a protocol to achieve zero knowledge? These are not vague claims, but exact definitions that determine what an attacker is and is not allowed to do. Without this clarity, security claims are meaningless.
Read more
A proof also requires a well-defined adversary model. Security depends critically on assumptions about an attacker’s capabilities: whether they can tamper with messages, inject data, observe internal state, or exploit computational resources. A security proof makes these assumptions explicit, so that guarantees are not overstated or misunderstood.
Most cryptographic security proofs are reduction proofs. Rather than claiming that a protocol is “unbreakable,” the proof shows that breaking the protocol would be at least as hard as solving a problem that is widely believed to be computationally infeasible—such as factoring large integers or computing discrete logarithms. In this way, the security of a protocol is reduced to the hardness of problems that have been studied extensively by the cryptographic community over decades.
Security proofs do not offer absolute guarantees. No proof can claim that a system can never be broken. What they provide instead is structured confidence: if the stated assumptions hold, then breaking the protocol is no easier than solving a well-understood hard problem. This clarity is essential not only for designers, but also for auditors, implementers, and users of cryptographic systems.
Equally important, security proofs expose the assumptions under which guarantees apply. Cryptographic protocols are often composed of multiple components, each with its own assumptions and guarantees. A well-defined proof framework ensures that these components can be composed without silently invalidating security claims—an essential requirement for complex modern systems.
Security proofs are a cornerstone of trust, adoption, and long-term confidence in cryptographic protocols.
Our security proof work process
1. Scope &threat model
We begin by understanding the protocol, its goals, and its trust assumptions. We define the attacker model and environment under which security claims are expected to hold.
2. Securitydefinitions
We formalize what security means for your system—privacy, soundness, unforgeability, zero knowledge, or other properties. These definitions precisely state what an adversary can and cannot achieve.
3. Proof strategy & reductions
We identify the appropriate proof framework and reduction strategy. This step connects protocol security to well-studied hardness assumptions and highlights where guarantees critically depend on them.
4. Proof & assumption review
We rigorously review the proof logic, assumptions, and composition of components. This includes checking for gaps, implicit assumptions, or mismatches between theory and real-world usage.
5. Final report
We deliver clear documentation of proven guarantees, assumptions, and limitations. The result is a precise security statement that engineers, auditors, and stakeholders can rely on.
Case Study: Monero
Monero’s roadmap includes FCMP++ (Full-Chain Membership Proofs), a next-generation privacy upgrade where cryptography, circuits, and real-world implementation details all have to line up. MAGIC Grants and the Monero community brought Veridise in to pressure-test that stack end-to-end—because in privacy tech, “looks right” isn’t a security argument.
Read the Monero case study
The challenge
A Liam Eagen proposal reduces a group-law claim on an elliptic curve—whether
P₁ + … + Pn = O —to checking properties of a committed witness function.
The “obvious” soundness argument works if the verifier samples truly random lines, but a practical optimization (restricting to lines with rational intersection points) changes the sampling distribution and makes the final Schwartz–Zippel step nontrivial / potentially unsound without extra work.
What Veridise did
Alp Bassa produced a full, implementation-aligned soundness proof (Soundness Proof for Eagen’s Proof of Sums of Points).
Key steps:
- Diagnosed the gap introduced by rationality-restricted line sampling and documented why the standard reduction no longer cleanly applies.
- Reframed the check on the surface E×E: instead of fragile line-sampling arguments, the verifier evaluates at random rational points on the surface and uses degree/point-count bounds (a Schwartz–Zippel analogue for varieties) to conclude soundness.
- Hardened “engineering-friendly” variants, including a careful derivation for using logarithmic derivatives through the norm construction (where the subtlety actually lives).
Results and impact
- Explicit, tunable soundness bound: the final theorem bounds cheating probability at approximately 18N/q
- Clear separation of completeness vs. soundness requirements: normalization (e.g., monic witness) is required for completeness, but not for the soundness argument—helping implementers avoid mixing “protocol convenience” with “security necessity.”
- Practical guidance: the note flags that even when the scheme is sound, ill-conceived implementations (especially around normalization/log-derivative variants) can introduce vulnerabilities.
Why this is relevant to Monero
Monero-class privacy systems depend on ZK/cryptographic components where “minor” sampling or algebra choices can silently invalidate proof sketches. This work demonstrates Veridise’s ability to (1) find those gaps, and (2) replace them with proofs that match real implementation constraints—yielding explicit assumptions and quantitative guarantees.
Conference presentation on cryptography
We’ve delivered presentation at numerous conferences about cryptography, zero-knowledge and other areas of blockchain security.
Veridise is the choice of industry leaders
We have audited some of the most critical protocols in the blockchain space, with billions of dollars in Total Value Locked
Considering a security proof?
Make your security claims precise, explicit, and defensible.
Get rigorous security proofs from Veridise’s cryptography experts.