Analysis of the Security Design, Engineering, and Implementation of the SecureDNA System

Analysis of the Security Design, Engineering, and Implementation of the SecureDNA System

Speakers: Alan T. Sherman

Conference: NDSS Symposium 2026

YouTube: https://www.youtube.com/watch?v=T8Ti5kmd7aI

Overview

The SecureDNA system enables DNA synthesizers to screen synthesis requests against a curated database of hazardous pathogen sequences, addressing the alarming convergence of AI capabilities and accessible DNA synthesis technology that could enable biological attacks. Developed by expert cryptographers and biologists including researchers at MIT, SecureDNA is considered the most promising screening protocol because it preserves both the secrecy of synthesis requests (protecting intellectual property) and the secrecy of the hazard database. This talk presents a rigorous security analysis using formal methods (CPSA, Cryptographic Protocol Shapes Analyzer) that uncovered two fundamental protocol weaknesses: a mutual authentication failure caused by inadequate binding (achieving only one-way authentication instead of mutual), enabling man-in-the-middle attacks that could expose the hazard database, and a response swapping vulnerability caused by improper binding of responses. The researchers proposed a fix (SC+) requiring only about five lines of code change, which SecureDNA has now implemented. The work underscores that even systems designed by expert cryptographers with sound UC proofs can have critical security engineering flaws.

Background

▶ Watch: SecureDNA system overview: screening DNA synthesis against hazard database (1:30)

DNA synthesis technology has advanced to the point where a single individual with a limited budget can order custom DNA sequences and have them mailed to their home. Most commercial synthesizers do not screen these orders against databases of known dangerous pathogens, creating a biosecurity risk. The SecureDNA Foundation (headquartered in Switzerland) provides a screening system that honest synthesizers can use to check requests against a curated hazard database.

The system's architecture involves four roles: a customer ordering DNA, a synthesizer processing the order, a distributed key server (distributed to eliminate single points of failure), and a hash database containing the hazard information. The underlying cryptography uses blinding operations to protect request secrecy and oblivious search protocols to query the database without revealing the query content.

The security goals are: (1) keep the hazard database secret (preventing adversaries from reconstructing the list of dangerous sequences), (2) keep synthesis requests secret (protecting customer IP), (3) return correct screening results, and (4) support authorized exceptions (allowing permitted researchers to order dangerous sequences).

The researchers used the Dolev-Yao adversarial model, where participants may not follow the protocol, major roles may be corrupt, and the adversary has complete control over the network (injecting, blocking, recombining messages) but cannot break cryptography.

Key Findings

▶ Watch: Ron Rivest suggested the analysis; SecureDNA refused to communicate for 2 years (5:30)

One-way authentication instead of mutual: The main protocols in SecureDNA call a subprotocol called SC (Secure Channel) that is intended to provide mutual authentication. However, due to a logical error in the binding of nonces, identities, and cookies, SC achieves only one-way authentication -- the synthesizer is authenticated to the key server, but the key server is not authenticated to the synthesizer. This is directly analogous to the classic Needham-Schroeder public key protocol vulnerability.

Man-in-the-middle attack on the hazard database: The authentication failure enables a man-in-the-middle attack where a corrupt key server (KP') can impersonate a synthesizer when communicating with the real key server. This allows the adversary to issue arbitrary queries against the hazard database, defeating the rate limiting defense (which restricts queries per synthesizer) by masquerading as multiple different synthesizers.

Response swapping vulnerability: Due to improper binding of responses, in some reconnection scenarios (using the same TLS keys), an adversary can swap responses, causing the synthesizer to receive incorrect screening results.

Custom authentication was unnecessary: SecureDNA chose not to use mutual TLS (mTLS) because they considered it "too complicated," instead inventing their own mutual authentication protocol. The researchers strongly disagree with this assessment and recommend mTLS as the proper solution. SecureDNA chose the alternative fix (SC+ with proper bindings) and has implemented it.

Protocol specifications were imprecise: The white paper describing SecureDNA's protocols was not precisely specified, requiring the researchers to reverse-engineer the actual protocols from source code. This highlights the importance of precise protocol specifications for security analysis.

Technical Deep Dive

▶ Watch: SC protocol flaw: one-way authentication due to improper binding (7:30)

The formal analysis used CPSA (Cryptographic Protocol Shapes Analyzer), a tool for exhaustive search over essentially different protocol executions. The methodology involved: (1) formally modeling the protocol with all roles and message flows, (2) specifying security goals precisely, (3) using CPSA to exhaustively search for violations from specified starting positions. CPSA provides a soundness guarantee: if the program terminates without finding a violation, the security goal is proven to hold.

The SC protocol exchanges identities, nonces, and a cookie for session resumption, all over one-way TLS (not mutual TLS). The vulnerability is that nonces and identities are not properly bound to the context -- they are not cryptographically tied to the specific protocol session, allowing an adversary to relay them between sessions.

The attack construction follows the classic MITM pattern: a synthesizer connects to a corrupt key server KP', which simultaneously initiates a session with the real key server KP, relaying messages between the two sessions. Because the SC protocol does not bind the exchanged values to a specific session partner, the real key server KP cannot distinguish the legitimate synthesizer from the adversary.

The proposed fix, SC+, adds proper cryptographic bindings to the critical values exchanged in the protocol -- approximately five lines of code change. CPSA verification of SC+ confirms that all security properties (confidentiality of the cookie from both perspectives, agreement on basic values from both perspectives) are satisfied.

The formal analysis results are summarized in a table showing that the original SC protocol achieves security properties only from the synthesizer's perspective, while SC+ achieves them from both perspectives.

Demo / Proof of Concept

▶ Watch: SC+ fix: five lines of code, formally verified with CPSA (11:00)

The CPSA-generated counterexample directly translates to a constructive attack. A corrupt key server KP' positions itself between a legitimate synthesizer and the real key server KP. By exploiting the one-way authentication, KP' can masquerade as the synthesizer to the real key server, enabling unrestricted queries against the hazard database. The response swapping attack is also constructively demonstrated. The researchers practiced responsible disclosure: SecureDNA was notified, the SC+ fix was proposed and formally verified, and SecureDNA has implemented the fix in the current version of the system. Complete artifacts (CPSA models, analysis results) are published on GitHub and IACR/arXiv.

Defensive Implications

▶ Watch: Lesson: custom protocols fail even with expert cryptographers; use mTLS (14:00)

For biosecurity infrastructure developers, this work provides a concrete lesson: even systems designed by expert cryptographers with sound abstract cryptographic proofs can have critical protocol-level vulnerabilities. The UC proofs for SecureDNA's oblivious search were sound; the vulnerability was in the security engineering of the surrounding authentication protocol.

For protocol designers broadly, the finding reinforces two well-established principles: (1) do not invent custom authentication protocols when standard solutions (mTLS) exist, and (2) use formal methods throughout the design process, not just as a post-hoc audit tool. The researchers note that the SecureDNA team refused to communicate with them for approximately two years until the paper was about to be published.

For policy makers involved in DNA synthesis regulation, the SecureDNA Foundation is urging countries to adopt legislation requiring synthesizers to use screening protocols. This security analysis strengthens the system by identifying and fixing vulnerabilities before widespread mandatory adoption.

For security engineers working on any system with custom protocols, the key management findings are also relevant: the researchers found that in some cases, cryptographic keys were stored in unencrypted files rather than hardware security modules like TPMs.

Key Takeaways

• SecureDNA's custom mutual authentication protocol (SC) achieved only one-way authentication due to improper binding of nonces and identities
• The vulnerability enables man-in-the-middle attacks that could expose the hazard database by defeating rate limiting
• Formal methods analysis using CPSA produced a constructive attack analogous to the Needham-Schroeder public key protocol vulnerability
• The fix (SC+) requires approximately five lines of code and has been formally verified and deployed
• Custom authentication protocols are unnecessary when mTLS exists -- SecureDNA's rationale that mTLS was "too complicated" led directly to the vulnerability
• Sound abstract cryptographic proofs (UC proofs) do not guarantee protocol-level security; security engineering review is essential
• Keys stored in unencrypted files should be protected with TPMs

About the Speaker(s)

Alan T. Sherman is a professor of computer science at the University of Maryland, Baltimore County (UMBC). The research is a collaboration with Jeremy Romano, Andis Gollesvski, Ed Ziggler (NSA research staff), Jonathan Fuchs, and William Bird (University of Alabama). The project was initiated at the suggestion of Ron Rivest, one of the cryptographers on the SecureDNA project, and originated as a student project in Sherman's cybersecurity research class under the National INSuRE program.