{"id":"f9c13f64-2ebd-4c4d-a269-b154dd494578","arxiv_id":"2411.13627","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Current frontier LLMs show partial, uneven ability to find vulnerabilities in novel cryptographic protocols when guided by the Tamarin prover, according to a new 15-protocol benchmark.","lead":"This paper introduces a benchmark that tests whether large language models can find flaws in new cryptographic protocols by interacting with the Tamarin proof tool. It reports early results on five models, finding uneven performance and no fully automated success.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Benchmark scores conflate Tamarin syntax skill with vulnerability detection; o1's high attack-trace accuracy in Appendix D versus its low overall ratings shows the headline metric may not measure the stated capability.","rationale":"The reader's weakest assumption concerns the manual ground-truth labels: each protocol may not contain exactly the labeled vulnerability. That is a real threat, but I see a more fundamental construct-validity threat: even if all labels are correct, the reported overall score does not necessarily measure vulnerability-detection skill. The paper's Appendix D shows that o1-preview, the model with the best attack-trace inference, receives low overall ratings because of Tamarin syntax failures, while higher-rated models sometimes fail to complete the detection/validation step. This is internal evidence that the rating rubric is anchored to formalization quality rather than to the target construct. The formalization-oracle experiment would settle whether the benchmark score tracks detection ability once syntactic fluency is controlled. Because this concern is concrete, fixable, and consistent with the paper's own disclosures, it does not overturn the conditional-accept recommendation; it sharpens the condition: the accepted version must separate detection accuracy from Tamarin formalization skill, and ideally include the automated sandbox as an objective scorer. Thus I keep the reader's CONDITIONAL verdict unchanged, with partial agreement because the reader emphasized label correctness rather than score validity.","tokens_in":12167,"tokens_out":7417,"duration_ms":87490,"concrete_test":"Run the 5-protocol pilot in two conditions with o1-preview: (a) the full pipeline as reported, and (b) a formalization-oracle condition in which the agent is supplied a human-verified, Tamarin-checked .spthy file after Task 1.2, so it only has to run Tamarin, interpret the output, and produce the attack trace in AnB. If condition (b) yields substantially higher scores than condition (a) while Task 2.1 attack-trace accuracy is held constant, the overall metric conflates Tamarin-syntax skill with vulnerability detection. A weaker, immediately available check: compute the rank correlation between Figure 2 ratings and Task 2.1 attack-trace correctness on the existing five protocols; if it is not substantially positive, the headline metric is not measuring vulnerability detection.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that the benchmark measures LLM agents' ability to identify protocol vulnerabilities. The only reported scores (Figure 2) are holistic ratings of the full 1.x-2.x pipeline, and the rating rubric in Section 4 is defined almost entirely in terms of Tamarin code quality (e.g., 'syntactically valid Tamarin code', 'trivial semantic errors'), not detection success. The paper's own data expose this construct mismatch: in Appendix D, o1-preview produces a coherent, correct attack trace for Protocols 2-5 (the actual vulnerability-detection step), yet receives the lowest or second-lowest overall rating on all five protocols in Figure 2, because it fails to produce syntactically correct Tamarin code. Conversely, Claude 3 Opus scores highest on Protocol 1 while failing Task 2.2 by refusing to copy the Tamarin attack trace (Appendix C and E.2). Thus the overall scores are dominated by Tamarin formalization and instruction-following, not by vulnerability identification. Without a formalization oracle or a separately reported detection score, the headline 'assess the ability to identify vulnerabilities' is not supported by the reported metric. The unimplemented attack-validation sandbox (footnote 4) compounds this by leaving manual ratings unchecked against a formal oracle.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"CryptoFormalEval proposes a benchmark for evaluating whether LLM-based agents can identify vulnerabilities in novel cryptographic protocols by interacting with the Tamarin prover. The paper describes a four-stage pipeline (protocol input, formalization, verification with Tamarin, attack validation), a dataset of 15 manually validated flawed protocols generated with GPT-4, and CryptoFormaLLM, an agent architecture with profiling, memory, and error handling. It reports preliminary results on five protocols with five frontier models (Claude 3 Haiku, Claude 3 Opus, Claude 3.5 Sonnet, GPT-4o, o1-preview), concluding that current models show partial capability but are not robust enough for fully automated use.","tokens_in":12402,"tokens_out":5356,"duration_ms":52189,"significance":"The benchmark addresses a timely and relevant capability: combining LLM flexibility with the formal guarantees of Tamarin for cryptographic protocol auditing. If the metric measured what it claims, it could serve as a useful tracking benchmark for AI security capabilities and as a practical aid for auditors. Strengths include the effort to construct novel protocols to reduce memorization, the middleware for agent-Tamarin interaction, the qualitative error analysis in Appendices A and C-E, and the plan to release the software. However, the validity of the central claim is currently weakened by three gaps: the headline metric conflates vulnerability detection with Tamarin syntax and instruction-following; the automated attack-validation sandbox, a stated contribution, is not implemented; and the ground-truth labels of the dataset are not verified by a formal tool. These gaps make the preliminary results useful as a pilot but not yet as a fully valid benchmark measurement.","major_comments":[{"comment":"The reported ratings are defined by the rubric in Section 4 almost entirely in terms of Tamarin code quality (e.g., 'syntactically valid Tamarin code', 'trivial semantic errors') and instruction following, not by whether the underlying vulnerability was identified. The paper's own data in Appendix D show that o1-preview produced coherent, correct attack traces for Protocols 2, 3, 4, and 5 in Task 2.1, yet it receives the lowest or second-lowest overall rating on all five protocols in Figure 2 because it fails to produce syntactically correct Tamarin code. Conversely, Claude 3 Opus is rated highest on Protocol 1 while failing Task 2.2 by refusing to copy the Tamarin attack trace (Appendices C and E.2). Thus the headline scores conflate formalization and instruction-following skill with vulnerability detection and do not support the abstract's claim that the benchmark assesses 'the ability of LLMs to autonomously identify vulnerabilities.' Please report a separate detection score (e.g., whether the correct vulnerability was found and described independently of Tamarin syntax) or otherwise decouple detection from formalization in the metric.","section":"Section 4, Figure 2"},{"comment":"The automated attack-validation sandbox is listed as a contribution (Section 1.1, item 1(c)) and Section 3.3 describes its planned checks, but footnote 4 states 'The validation sandbox is not fully implemented yet,' and the Introduction states 'Currently, the final output is manually evaluated.' This is load-bearing because the central claim is a benchmark that automatically verifies detected vulnerabilities through interaction with Tamarin; without the sandbox (or a fully specified manual evaluation protocol with inter-rater agreement), the reported ratings are not objectively reproducible and the abstract's phrase 'designed a method to automatically verify the vulnerabilities found by the AI agents' overstates what was executed. The experiments should either include the sandbox or be explicitly framed as a pilot with manual assessment, with the manual rubric and raw scoring data provided.","section":"Section 3.3, footnote 4; Section 1.1"},{"comment":"The dataset ground truth is not formally established. The protocols are generated with GPT-4 and then manually filtered, and the paper asserts that each protocol contains exactly the labeled vulnerability and no other flaws, but no Tamarin analysis or other formal check is reported for all 15 protocols. If a protocol is actually secure for the labeled property, or if it contains an unintended additional flaw, model scores cannot be interpreted as measuring detection of the intended vulnerability. In addition, because the generator is GPT-4 and the evaluated models include GPT-4 Turbo, GPT-4o, and o1-preview, the claim that the protocols are unseen by the tested models is plausible but not demonstrated; training-data contamination cannot be ruled out from the information given. Please provide a formal verification pass over the dataset (for each protocol, confirm the labeled property is falsifiable and that no other properties are violated) or a detailed manual audit, and include a contamination analysis (e.g., probing the models for knowledge of the exact protocol texts).","section":"Section 3.2"},{"comment":"The experimental results cover 5 of the 15 protocols, and the paper repeatedly calls the evaluation 'preliminary,' yet the conclusions state that 'current LLMs show promise, but they are not yet robust enough to fully automate the entire process' as if it applied to the full benchmark. The 5-protocol pilot may support that statement for the tested subset, but it is not sufficient to support conclusions about the whole dataset or about frontier-model capability more generally. Please restrict all such claims to the pilot subset and clearly specify the selection criteria for the five protocols, since Table 1 suggests they are ordered by size and may not be representative.","section":"Section 4; Section 5"}],"minor_comments":[{"comment":"The sentence 'From Table 2 and Table 2' should presumably be 'From Table 1 and Table 2'.","section":"Appendix B"},{"comment":"In the Protocol 5 entry for o1-preview, 'coping' should be 'copying'.","section":"Appendix D"},{"comment":"In the Protocol 3 entry, 'propriety' should be 'property'.","section":"Appendix C"},{"comment":"The phrase 'unsatisfied security property' is unclear; consider 'a security property that is expected to hold for the protocol but has not yet been verified.'","section":"Section 3.1"},{"comment":"The manual proof-guiding feature is listed as a middleware capability, but the main text does not state that it is currently unused; footnote 3 should be reflected in the main text to avoid misleading readers.","section":"Section 3.3"},{"comment":"The evaluation does not control for sampling temperature: o1-preview runs at temperature 1 while all other models use 0.1; since this is a cross-model capability comparison, please report sensitivity to temperature or justify this choice.","section":"Section 4"}],"recommendation":"major_revision","confidential_remarks":"The paper is best read as a pilot/system description rather than a fully validated benchmark. The main obstacles are construct validity (the reported metric does not isolate vulnerability detection) and the unimplemented validator, both of which are fixable within the manuscript's scope. I would encourage revision rather than rejection because the qualitative material is useful and the research direction is timely; however, the authors should temper the abstract and conclusions until the validator and detection-specific scoring are in place."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about this paper. First, it is a real first attempt at a benchmark for LLM agents doing cryptographic protocol vulnerability detection with Tamarin, and the authors are unusually candid about its limits. Second, the reported scores do not yet measure what the abstract claims. The benchmark is a good idea; the evaluation as presented is not yet valid.\n\nWhat is genuinely new: a manually curated dataset of 15 novel flawed protocols, a middleware layer for LLM-Tamarin interaction, and an agent architecture (CryptoFormaLLM) that iterates with Tamarin. The qualitative appendix is the most useful part — it shows concrete failure modes, including Claude's tendency to \"fix\" the protocol instead of copying the attack trace, and o1's surprisingly good attack-trace reasoning. The decision to restrict dataset access to reduce memorization is sensible. The authors also disclose that the automated validation sandbox is not fully implemented (footnote 4) and that results are preliminary on 5 of 15 protocols.\n\nNow the soft spots, and they are load-bearing. The central claim is that the benchmark assesses \"the ability to identify vulnerabilities.\" But the only reported ratings (Figure 2) use a rubric defined almost entirely in terms of Tamarin code quality: syntactic validity, trivial semantic errors, adaptation to feedback. The paper's own data expose the mismatch: o1-preview produces coherent, correct attack traces for Protocols 2-5 (Appendix D) yet receives the lowest or second-lowest overall rating because it cannot write valid Tamarin syntax. Claude 3 Opus scores highest on Protocol 1 while refusing to copy the trace in Task 2.2. So the headline metric conflates formalization skill with detection ability. Without a formalization oracle or a separately reported detection score, you cannot conclude anything about vulnerability-detection capability from Figure 2.\n\nThere are also smaller issues: no error bars or multiple runs, no external baseline, and the ground truth that each protocol contains exactly one labeled vulnerability is manually asserted rather than formally verified for all 15. The GPT-4-generated protocols also raise a plausible contamination concern for GPT-family models, though the manual filtering and novelty checks mitigate it.\n\nWho is this for? Researchers building LLM benchmarks for security or formal methods, and anyone tracking AI capability for dual-use tasks. The paper deserves a serious referee, but the referee should ask for a redesigned evaluation: report detection success separately from formalization success, implement or clearly scope out the automated validation, and release at least the full dataset and middleware. The raw material is solid; the measurement is not yet.\n\nMy recommendation: send it to peer review with major revision required. It is a legitimate contribution in progress, not a reject.","headline":"A genuinely useful first attempt at an LLM+Tamarin vulnerability-detection benchmark, but the headline metric currently measures Tamarin formalization skill more than vulnerability detection, so it needs a major evaluation redesign before it supports the central claim.","tokens_in":12956,"tokens_out":1564,"would_cite":false,"duration_ms":18675,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper introduces CryptoFormalEval, a benchmark that asks LLM agents to find vulnerabilities in new cryptographic protocols by interacting with the Tamarin prover, and reports that current frontier models do not yet complete the task…","keywords":["cryptographic protocols","formal verification","LLM agents","Tamarin prover","vulnerability detection","benchmark","Dolev-Yao model","symbolic reasoning"],"falsifier":"Run Tamarin's complete attack search on all released protocols with the intended property and with a battery of related properties: if any labeled vulnerability is not reproduced or any protocol turns out to be secure, the ground truth is wrong. A complementary experiment is to hand the agent provably secure protocols and count false attack reports.","tokens_in":11963,"feed_emoji":"🔐","tokens_out":7603,"duration_ms":74876,"temperature":0.7,"pith_summary":"To establish whether large language models can do real cryptographic protocol auditing rather than recall known vulnerabilities, this paper builds a benchmark called CryptoFormalEval. The benchmark gives an LLM agent a new, flawed protocol in Alice-and-Bob notation plus a security property, and requires the agent to formalize the protocol for the Tamarin prover, drive the proof search, and translate any attack trace back for validation. The authors created 15 novel protocols by generating candidates with GPT-4 and manually filtering them so each is believed to contain exactly one detectable vulnerability. On a five-protocol subset, frontier models showed partial skill: some produced valid Tamarin code and found attacks, but no model completed the full pipeline without errors, with syntax mistakes, misplaced observables, and refusal to follow output rules being common failures. The point of the benchmark is to quantify a capability that could eventually automate parts of security auditing.","feed_headline":"LLM agents show partial skill at finding protocol flaws with Tamarin","feed_subtitle":"A new benchmark gives models unseen, flawed protocols and scores their full audit loop; none yet completes it reliably.","key_machinery":"The central machinery is the benchmark pipeline itself, built around the Tamarin prover, a theorem prover for symbolic security-protocol analysis whose attack search is sound and complete under the Dolev-Yao attacker model, in which an attacker controls the network and can replay, forward, and algebraically manipulate messages but cannot break the cryptography. The agent, called CryptoFormaLLM, works through two phases: first it translates the input Alice-and-Bob protocol into Tamarin rules and refines them until syntactically acceptable, optionally using an automated AnB-to-Tamarin conversion tool; then it asks Tamarin to falsify the specified security property, adapts to errors and timeouts, and translates any attack trace back into Alice-and-Bob notation. A middleware imposes timeouts, filters Tamarin output, and blocks unsafe shell commands, and a symbolic sandbox is intended to check that the reconstructed trace is executable, coherent with the protocol, and a genuine counterexample to the property. What carries the argument is the interaction loop: the LLM must produce formalizations that the prover accepts and must correctly interpret the prover's output, so the benchmark jointly tests language-model competence and symbolic-reasoning integration.","core_discovery":"The paper's central claim is that an LLM-driven agent can be meaningfully assessed on protocol vulnerability detection by making it do the full audit loop: translate an Alice-and-Bob protocol into Tamarin, iterate against Tamarin's feedback to obtain an attack trace, and translate the trace back into a human-readable counterexample. The authors report that this loop is currently only partially executable by frontier models. On the tested protocols, no model completed the whole task without errors; Claude 3 Opus and Claude 3.5 Sonnet handled Tamarin syntax best, while o1-preview showed strong conceptual understanding of protocol security but frequently produced syntactically incorrect Tamarin. The benchmark's validity as a measure of vulnerability-detection skill rests on the manually curated dataset: 15 novel protocols, each paired with one intended vulnerability such as a replay attack, a secrecy break, or a freshness violation.","pith_inferences":["If the manually assigned labels are ever checked by running Tamarin on all 15 protocols, any mismatch would change how the reported scores should be read; this check is not in the paper.","The same agent loop could in principle be pointed at other formal verification tools or other domains such as smart-contract security, though the paper does not make that claim.","Adding provably secure control protocols would measure false-positive attack reports, which the current benchmark does not do.","Rising scores from future models could come from better Tamarin code generation rather than better security judgment; separating those would require ablations that the paper leaves for future work."],"forward_implications":["If the benchmark is a valid measure, scores on CryptoFormalEval reflect a real audit skill: turning a protocol description into a machine-checked formalization and extracting an attack from the prover's output.","The preliminary results imply that no current frontier model can be trusted to run an end-to-end protocol audit without human oversight at the formalization and validation steps.","Because the protocols are new and the full dataset is restricted, the measured performance is evidence about reasoning and tool use rather than about memorization of published protocols.","Completing the attack-validation sandbox would allow the benchmark to be scored automatically, replacing today's manual evaluation.","The documented failure modes point to concrete improvement targets: Tamarin syntax competence, correct placement of observable facts, and adherence to output instructions."],"supporting_citations":[{"why":"Supplies the Tamarin prover, the symbolic engine whose sound and complete attack search the agent interacts with.","marker":"[17]"},{"why":"Defines the Dolev-Yao attacker model that fixes what counts as a valid attack on the formalized protocol.","marker":"[7]"},{"why":"Provides the Alice-and-Bob to Tamarin translation tool that the agent can call during formalization.","marker":"[4]"},{"why":"Establishes the undecidability of unbounded protocol verification, motivating the need for heuristic, agent-driven proof search.","marker":"[10]"},{"why":"Gives the published Needham-Schroeder attack that motivates proactive automated vulnerability detection.","marker":"[16]"},{"why":"Supports the chain-of-thought and self-reflection prompting used in the agent's formalization phase.","marker":"[20]"},{"why":"Represents recent LLM agent security work whose reliance on known vulnerabilities the benchmark aims to avoid with unseen protocols.","marker":"[11]"}],"fun_headline_variants":["LLM agents fail to fully automate protocol flaw hunting","New benchmark tests LLMs on crypto protocol attacks","LLMs vs. Tamarin: partial wins in protocol security audit","Can LLMs spot protocol flaws? Only with help from Tamarin"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The benchmark's validity depends on the manual claim that each of the 15 protocols contains exactly the labeled vulnerability and no other flaw, since that ground truth has not been established by a formal tool.","fun_headline_variants_meta":{"raw":{"variants":["LLM agents fail to fully automate protocol flaw hunting","New benchmark tests LLMs on crypto protocol attacks","LLMs vs. Tamarin: partial wins in protocol security audit","Can LLMs spot protocol flaws? Only with help from Tamarin"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000187,"raw_usage":{"total_tokens":1283,"prompt_tokens":856,"completion_tokens":427,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":472,"completion_tokens_details":{"reasoning_tokens":359}},"tokens_in":472,"tokens_out":427,"duration_ms":4955,"temperature":1.0,"reasoning_tokens":359,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T16:32:04.255213+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Tamarin's complete attack search on all released protocols with the intended property and with a battery of related properties: if any labeled vulnerability is not reproduced or any protocol turns out to be secure, the ground truth is wrong. A complementary experiment is to hand the agent provably secure protocols and count false attack reports.","supporting_citations":[{"cited_title":"and Yao, A","cited_arxiv_id":null,"evidence_quote":"Defines the Dolev-Yao attacker model that fixes what counts as a valid attack on the formalized protocol."},{"cited_title":"Alice and bob meet equational theories","cited_arxiv_id":null,"evidence_quote":"Provides the Alice-and-Bob to Tamarin translation tool that the agent can call during formalization."},{"cited_title":"and Goldreich, O","cited_arxiv_id":null,"evidence_quote":"Establishes the undecidability of unbounded protocol verification, motivating the need for heuristic, agent-driven proof search."},{"cited_title":"An attack on the needham- schroeder public- key authentication protocol","cited_arxiv_id":null,"evidence_quote":"Gives the published Needham-Schroeder attack that motivates proactive automated vulnerability detection."}],"review_version":1}