Pith. sign in

REVIEW 3 minor 52 references

LLMs, even with dedicated reasoning modes, do not match formal verification tools when judging whether security protocols are vulnerable; at best they are pre-screening filters, not verifiers.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 09:33 UTC pith:WC3SO32W

load-bearing objection Solid empirical benchmark showing LLMs can't replace formal protocol verifiers; main caveat is the formal-tool ground truth, which is acknowledged and partly checked.

arxiv 2607.20712 v1 pith:WC3SO32W submitted 2026-07-22 cs.CR cs.AI

Evaluating Large Language Models for Symbolic Security Protocol Analysis

Paolo Modesti , Syed Ahmed , Ioannis Sfyrakis , Derek Enodolomwanyi This is my paper
classification cs.CR cs.AI
keywords security protocolsLLM evaluationsymbolic verificationProVerifOFMCchain-of-thoughtconfidence calibrationAnB/AnBx
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper asks whether large language models can replace formal verification tools like ProVerif and OFMC for judging whether security protocols are vulnerable. Testing GPT and DeepSeek in chat and reasoning modes on 130 obfuscated protocols with 388 security goals, it finds that no configuration comes close to the formal tools: chat models recall most attacks but cry wolf at precision below 31%, while reasoning models are more precise but detect just over half of true attacks. The paper also shows that all models fail most on authentication goals, that verdicts shift between runs, and that models attach high confidence to wrong answers. The author's conclusion is that LLM verdicts are data-driven heuristics, not sound proofs, and that their realistic role is cheap pre-screening, never independent verification.

Core claim

On 130 obfuscated AnB/AnBx protocols with 388 security goals, no tested GPT or DeepSeek configuration—chat or reasoning—matches formal verification. Chat models recall 69–81% of attacks but hold precision below 31%; reasoning models reach 66.5% (GPT) and 45.4% (DeepSeek) precision but recall just over half of true attacks. DeepSeek's two modes share one model, isolating a real reasoning effect: precision rises from 27.2% to 45.4%. Authentication goals are the blind spot (well under half of injective-agreement attacks), confidentiality the strength (F1 up to 95.7%). Verdicts are unstable across runs, and confidence scores are uniformly high yet uncorrelated with correctness.

What carries the argument

The load-bearing object is the definitive ground-truth verdict built by a waterfall over three formal sources—ProVerif first, then OFMC at two sessions, then OFMC at one session—against which every LLM verdict is scored per goal. ProVerif's unbounded-session analysis supplies the verdict for 370 of 388 goals; OFMC fills the remaining 18, inheriting a single-session horizon. A protocol-level cluster bootstrap, resampling whole protocols rather than individual goals, supplies honest confidence intervals, and the same DeepSeek model run with and without chain-of-thought isolates the effect of reasoning itself.

Load-bearing premise

The evaluation treats the formal tools' verdicts as correct ground truth; in particular, the 18 goals that ProVerif cannot resolve are decided by OFMC at a single session, so any multi-session attack among them would count as 'no attack' and the LLM would get credit for a correct verdict.

What would settle it

Replay the two-session attack traces the models report in a tool such as OFMC. If most traces prove to be genuine attacks under formal replay, the paper's claim that LLM verdicts are mostly heuristic false alarms would be weakened; the paper itself proposes this check but does not run it.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • LLMs, at best, act as pre-screening filters: chat models can flag candidates cheaply, reasoning models can confirm some of them, but every verdict needs independent formal confirmation.
  • Self-reported confidence must be ignored: the models assign 94–99% confidence to attacks they miss, so confidence scores cannot filter or rank verdicts.
  • Deployment should be goal-type-aware: LLM verdicts are usable for confidentiality screening (F1 up to 95.7%) but not for agreement goals, where recall stays below 41%.
  • Inter-run disagreement is a candidate escalation signal: 10–26% of goals change verdict across runs, and majority voting helps the less stable model.
  • DeepSeek's cost advantage (about 60x cheaper than GPT on the same workload) makes it the plausible engine for a large-scale first pass.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The stability data suggest a cheap operational test: if inter-run disagreement correlates with protocol difficulty rather than stochastic noise, escalation policies can be tuned from disagreement rates alone; the paper flags this as unconfirmed.
  • Mechanically replaying the models' two-session traces in OFMC would do more than validate — it could convert the binary-verdict comparison into a trace-level one, possibly showing that reasoning models find real attack shapes they then fail to report in the verdict field.
  • The 18 OFMC-filled goals are the single point where the reference standard could undercount attacks; an expert audit of residual disagreements, which the paper leaves out of scope, would either confirm or shift the reported recall numbers.
  • If the structural blindness to authentication goals persists across newer models, the meaningful near-term role for LLMs in this domain may be restricted to confidentiality screening, where measured F1 is already high.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 3 minor

Summary. The paper reports a multi-run benchmark of four LLM configurations—GPT-5.2 chat, GPT-5.4 reasoning, DeepSeek v4 Flash chat, and DeepSeek v4 Flash reasoning—applied to 130 obfuscated AnB/AnBx protocols containing 388 security goals. Each configuration is run three times on the full dataset, and the verdicts are scored against a definitive ground truth built from ProVerif (primary) and OFMC at one and two sessions using a waterfall priority scheme. The authors report precision, recall, F1, accuracy, confidence calibration, inter-run consistency, cost, and protocol-level clustered bootstrap confidence intervals. The main empirical findings are that chat models achieve high recall (69–81%) but very low precision (below 31%), reasoning models improve precision (GPT 66.5%, DeepSeek 45.4% against ProVerif) but detect only slightly more than half of the attacks, all models perform worst on authentication goals, and self-reported confidence is not a usable correctness filter. The paper concludes that LLMs are not substitutes for formal verification and may serve only as pre-screening filters, with goal-type-aware and cost-aware caveats.

Significance. If the formal-tool ground truth is accepted, this is a valuable and well-executed empirical contribution. The study has several notable methodological strengths: type-aware identifier obfuscation to mitigate training-data contamination, three independent runs per configuration, protocol-level cluster bootstrap confidence intervals rather than naive goal-level independence, a direct like-for-like comparison between chat and reasoning modes for DeepSeek, and a comparison of LLM verdicts against external formal tools rather than against the LLMs themselves. The central empirical claim—that current chat and reasoning LLM verdicts are fallible, unstable, and uncalibrated relative to ProVerif/OFMC—is supported by the reported numbers and by the bootstrap analyses. The main residual risk is the assumption that ProVerif/OFMC verdicts are correct ground truth, which the authors explicitly acknowledge in §6.2. I do not regard this as a load-bearing flaw: ProVerif covers 370 of 388 goals, inter-tool agreement on jointly resolved goals is 94–98%, and the sensitivity analysis bounding the 18 OFMC-filled goals shows at most a roughly two-point shift in precision and recall. The qualitative concl

minor comments (3)
  1. [§3.3] The sentence "OFMC 2022 results at two sessions (14 goals) and 1-session (4 goals) were used only when ProVerif coverage was absent" is easily misread as stating OFMC's total coverage. As later clarified in §5.3, OFMC 2-session resolves 245 goals and OFMC 1-session resolves all 388; the 14 and 4 are the subsets of the 18 ProVerif-uncovered goals filled by each OFMC configuration. Please rephrase to remove the apparent contradiction.
  2. [§2.2 / §3.4 / Appendix A] The background section defines weak secrecy as "the intruder cannot derive the protected value" and strong secrecy as indistinguishability of executions. However, the prompt in Appendix A defines "Secrecy" only as the indistinguishability notion, while the AnBx "secret between" goals used in the dataset appear to correspond to the weaker derivation-based notion. Please clarify which secrecy notion the models were instructed to evaluate and whether the goal categorization treats "secret between" as weak secrecy; otherwise the secrecy-goal results are difficult to interpret.
  3. [§6.2 / §8] The absence of a manual audit of residual LLM/tool disagreements is explicitly acknowledged, and the sensitivity analysis bounds the effect of the 18 OFMC-filled goals. Since this is the weakest point of the ground-truth construction, a sentence in the conclusion restating that the headline conclusions are unchanged by the reported ±2-point shift would help readers calibrate the strength of the claim.

Circularity Check

0 steps flagged

No circularity: LLM verdicts are scored against external formal-tool ground truth; the authors' AnBx self-citation concerns dataset tooling and is not load-bearing.

full rationale

The paper's central claim is an empirical comparison: LLM security verdicts are scored against ProVerif and OFMC outputs. The ground truth is external to the LLMs and to any parameter fitted by the authors: Section 3.3 states that "A ground-truth verdict for each goal was established using formal verification tools," with ProVerif as primary benchmark and OFMC filling only goals ProVerif leaves unresolved. No equation in the paper defines an LLM metric in terms of another LLM metric, and no fitted coefficient is renamed as a prediction; the reported precision, recall, and F1 are direct confusion-matrix counts of LLM verdicts versus tool verdicts. The main self-citation is to the AnBx compiler [15] for the protocol corpus and obfuscation functionality. This is not load-bearing circularity: the paper does not evaluate the AnBx compiler's correctness, and the measured quantity is LLM-versus-formal-tool agreement, not any property of AnBx. Even if the AnBx translation were imperfect, it would threaten validity of the benchmark, not make the LLM results equal to its inputs by construction. The acknowledged limitation that "the ground truth may itself under-count attacks" (Section 6.2) concerns the accuracy of the external formal-tool labels and is a correctness risk, not a circularity: nothing in the paper trains, tunes, or defines the LLM outputs using those labels beyond scoring them. The confidence-calibration analysis is likewise an empirical test, not a definitional claim; the models' self-reports are recorded and compared with correctness, and the finding that confidence is uninformative is an observed result. No uniqueness theorem from the authors' prior work is invoked to force a choice, and no ansatz is smuggled in via self-citation. The derivation chain is therefore self-contained against an external benchmark, and no specific circular reduction can be exhibited.

Axiom & Free-Parameter Ledger

1 free parameters · 5 axioms · 0 invented entities

There are no invented entities and no fitted model parameters. The only hand-chosen configuration item is the OpenAI chat temperature. The central claim rests on the validity of formal-tool ground truth, the Dolev-Yao abstraction, the semantics-preserving nature of obfuscation, and the waterfall consolidation, all of which the paper partially checks but does not independently prove.

free parameters (1)
  • OpenAI chat temperature = 0.1
    Hand-chosen in Section 4.2 to encourage stable output; affects run-to-run variability and therefore inter-run consistency estimates, though not fitted to the ground truth.
axioms (5)
  • domain assumption Dolev-Yao attacker model and perfect cryptography
    The prompt instructs the LLM to reason under Dolev-Yao rules (Section 3.4), and ProVerif/OFMC ground truth is defined relative to the same model (Section 2.1). Attack definitions depend on this abstraction.
  • domain assumption ProVerif and OFMC outputs are correct ground truth
    All LLM verdicts are scored against formal-tool outputs. Section 3.3 checks cross-tool agreement, and Section 6.2 admits no manual expert audit remains; the centrality of this assumption is the paper's weakest point.
  • domain assumption Type-aware identifier obfuscation preserves protocol semantics while preventing contamination
    Section 3.3 replaces user-defined identifiers with typed fresh names but leaves function symbols and DH generator unchanged. If renaming altered semantics, or if models still recognized structural fingerprints, the forced-reasoning conclusion would be affected.
  • domain assumption Waterfall consolidation (ProVerif then OFMC) yields a valid definitive verdict
    Section 3.3/4.3 uses ProVerif where it terminates and OFMC otherwise. The consistency checks and sensitivity analysis support it, but the 18 OFMC-filled goals retain OFMC's single-session limitation.
  • standard math Protocol-level cluster bootstrap gives valid confidence intervals
    Section 3.5 resamples protocols instead of goals to avoid pseudo-replication; this is a standard bootstrap correction and is appropriate for the correlated-goal structure.

pith-pipeline@v1.3.0-alltime-deepseek · 23900 in / 10102 out tokens · 94296 ms · 2026-08-01T09:33:51.197735+00:00 · methodology

0 comments
read the original abstract

Security protocol verification relies on formal tools such as ProVerif and OFMC. This study evaluates whether Large Language Models (LLMs) can perform comparable analysis. We test GPT and DeepSeek in chat and reasoning modes over three runs on 130 obfuscated AnB/AnBx protocols covering 388 security goals, scored against ProVerif and OFMC. Chat models reach 69 to 81% recall at precision below 31%. Reasoning models reverse this trade-off, reaching 66.5% precision for GPT and 45.4% for DeepSeek, but detect just over half the attacks. DeepSeek's two modes share one underlying model, so the comparison isolates reasoning itself, which raises precision from 27.2% to 45.4%. The GPT contrast spans a model-version change and is only suggestive. All models perform worst on authentication goals: reasoning models detect well under half of injective and non-injective agreement attacks, whereas chat models over-flag them at low precision. Confidentiality is the exception, with F1 up to 95.7% in reasoning mode. Verdicts are unstable across runs, identical on 89.7% of goals for GPT but 74.0% for DeepSeek. Self-reported confidence is uniformly high yet shows no meaningful correlation with correctness. On this benchmark LLMs do not match formal verification, but may serve, at best, as pre-screening filters.

Figures

Figures reproduced from arXiv: 2607.20712 by Derek Enodolomwanyi, Ioannis Sfyrakis, Paolo Modesti, Syed Ahmed.

Figure 1
Figure 1. Figure 1: Dolev-Yao intruder rules Two mature tools that mechanise symbolic protocol analysis are ProVerif and OFMC, each with distinct strengths and limitations. ProVerif. ProVerif [2] translates protocol specifications, expressed in a variant of the applied pi-calculus, into a set of Horn clauses and applies a resolution￾based algorithm to determine what the intruder can derive. It is notable for its ability to an… view at source ↗
Figure 2
Figure 2. Figure 2: AnB Protocol Example The Alice & Bob (AnB) [12] notation provides an intuitive, message-sequence oriented language for describing security protocols [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: AnBx Protocol Example Security goals in AnB/AnBx are classified into two broad families: authen￾tication goals and secrecy goals. Authentication goals. Lowe’s hierarchy [13] defines four authentication levels; we consider the two strongest. Non-injective agreement guarantees that the two principals agree on a set of data values, but allows a single run of the responder to be paired with multiple initiator … view at source ↗
Figure 4
Figure 4. Figure 4: Workflow of the protocol-analysis pipeline [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Confidence calibration: fraction of correct verdicts per reported-confidence bin, [PITH_FULL_IMAGE:figures/full_fig_p022_5.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

52 extracted references · 12 canonical work pages

  1. [1]

    Lowe, Breaking and fixing the needham-schroeder public-key protocol using fdr, in: T

    G. Lowe, Breaking and fixing the needham-schroeder public-key protocol using fdr, in: T. Margaria, B. Steffen (Eds.), Tools and Algorithms for the 29 Construction and Analysis of Systems, Springer Berlin Heidelberg, Berlin, Heidelberg, 1996, pp. 147–166.doi:10.1007/3-540-61042-1_43

    work page doi:10.1007/3-540-61042-1_43 1996

  2. [2]

    B. Blanchet, et al., Modeling and verifying security protocols with the applied pi calculus and proverif, Foundations and Trends®in Privacy and Security 1 (1-2) (2016) 1–135.doi:10.1561/9781680832075

    work page doi:10.1561/9781680832075 2016

  3. [3]

    Mödersheim, L

    S. Mödersheim, L. Viganò, The open-source fixed-point model checker for symbolic analysis of security protocols, in: Foundations of Secu- rity Analysis and Design, Springer, 2009, pp. 166–194.doi:10.1007/ 978-3-642-03829-7_6

    2009

  4. [4]

    Dolev, A

    D. Dolev, A. C. Yao, On the security of public key protocols, IEEE Trans- actions on Information Theory 29 (2) (1983) 198–208.doi:10.1109/TIT. 1983.1056650

    arXiv 1983

  5. [5]

    Wang, T.-S

    P.-Y. Wang, T.-S. Liu, C. Wang, Z. Li, Y. Wang, S. Yan, C. Jia, X.-H. Liu, X. Chen, J. Xu, Y. Yu, A survey on large language models for mathematical reasoning, ACM Computing Surveys 58 (8) (2026) 1–35.doi:10.1145/ 3786333

    2026

  6. [6]

    Q. Li, J. Han, L. Yuan, X. Li, X. Wang, Constructing formal models of cryptographic protocols from alice&bob style specifications via llm, Scien- tific Reports 15 (1) (2025) 11866.doi:10.1038/s41598-025-93373-y

    work page doi:10.1038/s41598-025-93373-y 2025

  7. [7]

    Z. Mao, J. Wang, J. Sun, S. Qin, J. Xiong, Llm-aided automatic model- ing for security protocol verification, in: 2025 IEEE/ACM 47th Interna- tional Conference on Software Engineering (ICSE), IEEE, 2025, pp. 642– 654.doi:10.1109/ICSE55347.2025.00197

    arXiv 2025

  8. [8]

    Curaba, D

    C. Curaba, D. D’Ambrosi, A. Minisini, N. P. Antolín, CryptoFormalEval: Integrating large language models and formal verification for automated cryptographic protocol vulnerability detection, in: The First Workshop on System-2 Reasoning at Scale, NeurIPS’24, 2024

    2024

  9. [9]

    Blanchet, Composition theorems for cryptoverif and application to tls 1.3, in: 2018IEEE31stComputerSecurityFoundationsSymposium(CSF), IEEE, 2018, pp

    B. Blanchet, Composition theorems for cryptoverif and application to tls 1.3, in: 2018IEEE31stComputerSecurityFoundationsSymposium(CSF), IEEE, 2018, pp. 16–30.doi:10.1109/csf.2018.00009

    arXiv 2018

  10. [10]

    Cheval, V

    V. Cheval, V. Cortier, A. Debant, Election verifiability with proverif, in: 2023 IEEE 36th Computer Security Foundations Symposium (CSF), IEEE, 2023, pp. 43–58.doi:10.1109/csf57540.2023.00032

    arXiv 2023

  11. [11]

    Basin, S

    D. Basin, S. Mödersheim, L. Viganò, An on-the-fly model-checker for se- curity protocol analysis, in: E. Snekkenes, D. Gollmann (Eds.), Computer Security – ESORICS 2003, Springer Berlin Heidelberg, Berlin, Heidelberg, 2003, pp. 253–270.doi:10.1007/978-3-540-39650-5_15. 30

    work page doi:10.1007/978-3-540-39650-5_15 2003

  12. [12]

    S. Mödersheim, Algebraic properties in alice and bob notation, in: Proceed- ings of the The Forth International Conference on Availability, Reliability and Security, ARES 2009, March 16-19, 2009, Fukuoka, Japan, IEEE Com- puter Society, 2009, pp. 433–440.doi:10.1109/ARES.2009.95

    work page doi:10.1109/ares.2009.95 2009

  13. [13]

    Lowe, A hierarchy of authentication specifications, in: CSFW’97, IEEE Computer Society Press, 1997, pp

    G. Lowe, A hierarchy of authentication specifications, in: CSFW’97, IEEE Computer Society Press, 1997, pp. 31–43

    1997

  14. [14]

    Bugliesi, S

    M. Bugliesi, S. Calzavara, S. Mödersheim, P. Modesti, Security protocol specification and verification with anbx, J. Inf. Secur. Appl. 30 (2016) 46– 63.doi:10.1016/J.JISA.2016.05.004

    work page doi:10.1016/j.jisa.2016.05.004 2016

  15. [15]

    Modesti, AnBx: Automatic generation and verification of security pro- tocols implementations, in: J

    P. Modesti, AnBx: Automatic generation and verification of security pro- tocols implementations, in: J. García-Alfaro, E. Kranakis, G. Bonfante (Eds.), 8th International Symposium on Foundations & Practice of Se- curity, Vol. 9482 of LNCS, Springer, 2015, pp. 156–173.doi:10.1007/ 978-3-319-30303-1_10

    2015

  16. [16]

    Blanchet, B

    B. Blanchet, B. Smyth, V. Cheval, M. Sylvestre, Proverif 2.05: Automatic cryptographic protocol verifier, user manual and tutorial (2023). URLhttps://bblanche.gitlabpages.inria.fr/proverif/manual.pdf

    2023

  17. [17]

    URLhttps://arxiv.org/abs/2303.08774

    OpenAI, GPT-4 technical report, CoRR abs/2303.08774 (2023).arXiv: 2303.08774,doi:10.48550/ARXIV.2303.08774. URLhttps://arxiv.org/abs/2303.08774

    Pith/arXiv arXiv doi:10.48550/arxiv.2303.08774 2023

  18. [18]

    J. Wei, X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. H. Chi, Q. V. Le, D. Zhou, Chain-of-thought prompting elicits reasoning in large language models, in: Proceedings of the 36th International Conference on Neural Information Processing Systems, NIPS ’22, Curran Associates Inc., Red Hook, NY, USA, 2022

    2022

  19. [19]

    URLhttps://openai.com/index/introducing-o3-and-o4-mini/

    OpenAI, Introducing OpenAI o3 and o4-mini, product release (April 2025). URLhttps://openai.com/index/introducing-o3-and-o4-mini/

    2025

  20. [20]

    DeepSeek-AI, Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning, CoRR abs/2501.12948 (2025).arXiv:2501.12948, doi:10.48550/ARXIV.2501.12948

    Pith/arXiv arXiv doi:10.48550/arxiv.2501.12948 2025

  21. [21]

    X. Liu, T. Chen, L. Da, C. Chen, Z. Lin, H. Wei, Uncertainty quantification and confidence calibration in large language models: A survey, in: Proceed- ings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining V. 2, 2025, pp. 6107–6117.doi:10.1145/3711896.3736569

    arXiv 2025

  22. [22]

    Schmidt, S

    B. Schmidt, S. Meier, C. Cremers, D. Basin, Automated analysis of Diffie- Hellman protocols and advanced security properties, in: Computer Security Foundations Symposium (CSF), 2012 IEEE 25th, IEEE, 2012, pp. 78–94. doi:10.1109/csf.2012.25. 31

    work page doi:10.1109/csf.2012.25 2012

  23. [23]

    OpenAI, Api pricing,https://openai.com/api/pricing/, accessed 14 April 2026 (2026)

    2026

  24. [24]

    OpenAI, Introducing GPT-5.4,https://openai.com/index/ introducing-gpt-5-4/, product release (March 2026)

    2026

  25. [25]

    Blanchet, Automatic verification of security protocols in the symbolic model: The verifier proverif, in: A

    B. Blanchet, Automatic verification of security protocols in the symbolic model: The verifier proverif, in: A. Aldini, J. Lopez, F. Martinelli (Eds.), Foundations of Security Analysis and Design VII: FOSAD 2012/2013 Tu- torial Lectures, Springer International Publishing, Cham, 2014, pp. 54–87. doi:10.1007/978-3-319-10082-1_3

    work page doi:10.1007/978-3-319-10082-1_3 2012

  26. [26]

    Magar, R

    I. Magar, R. Schwartz, Data contamination: From memorization to ex- ploitation, in: Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), 2022, pp. 157– 165.doi:10.18653/v1/2022.acl-short.18

    doi:10.18653/v1/2022.acl-short.18 2022

  27. [27]

    Sainz, J

    O. Sainz, J. A. Campos, I. García-Ferrero, J. Etxaniz, O. L. de La- calle, E. Agirre, NLP evaluation in trouble: On the need to measure LLM data contamination for each benchmark, in: H. Bouamor, J. Pino, K. Bali (Eds.), Findings of the Association for Computational Linguis- tics: EMNLP 2023, Singapore, December 6-10, 2023, Findings of ACL, Association for...

    doi:10.18653/v1/2023.findings-emnlp.722 2023

  28. [28]

    H. He, E. A. Garcia, Learning from imbalanced data, IEEE Transactions on Knowledge and Data Engineering 21 (9) (2009) 1263–1284.doi:10. 1109/TKDE.2008.239

    2009

  29. [29]

    Sommer, V

    R. Sommer, V. Paxson, Outside the closed world: On using machine learn- ing for network intrusion detection, in: 2010 IEEE symposium on security and privacy, IEEE, 2010, pp. 305–316.doi:10.1109/sp.2010.25

    doi:10.1109/sp.2010.25 2010

  30. [30]

    F. Trad, A. Chehab, To ensemble or not: Assessing majority voting strate- gies for phishing detection with large language models, in: A. Bennour, A. Bouridane, S. Almaadeed, B. Bouaziz, E. A. Edirisinghe (Eds.), In- telligent Systems and Pattern Recognition - 4th International Conference, ISPR 2024, Istanbul, Turkey, June 26-28, 2024, Revised Selected Pap...

    work page doi:10.1007/978-3-031-82150-9 2024

  31. [31]

    R. Ai, Y. Pan, D. Simchi-Levi, M. Tambe, H. Xu, Beyond majority voting: Llm aggregation by leveraging higher-order information (2026).arXiv: 2510.01499,doi:10.48550/arxiv.2510.01499

    Pith/arXiv arXiv doi:10.48550/arxiv.2510.01499 2026

  32. [32]

    S. H. Hurlbert, Pseudoreplication and the design of ecological field ex- periments, Ecological Monographs 54 (2) (1984) 187–211.doi:10.2307/ 1942661. 32

    1984

  33. [33]

    C. A. Field, A. H. Welsh, Bootstrapping clustered data, Journal of the Royal Statistical Society Series B: Statistical Methodology 69 (3) (2007) 369–390.doi:10.1111/j.1467-9868.2007.00593.x

    arXiv 2007

  34. [34]

    deepseek.com/guides/reasoning_model, deepSeek API Docs

    DeepSeek, Reasoning model (deepseek-reasoner),https://api-docs. deepseek.com/guides/reasoning_model, deepSeek API Docs. Accessed 15 April 2026 (2026)

    2026

  35. [35]

    Accessed 14 April 2026 (2026)

    DeepSeek, Models & pricing,https://api-docs.deepseek.com/quick_ start/pricing, deepSeek API Docs. Accessed 14 April 2026 (2026)

    2026

  36. [36]

    Sheng, Z

    Z. Sheng, Z. Chen, S. Gu, H. Huang, G. Gu, J. Huang, Llms in software security: A survey of vulnerability detection techniques and insights, ACM Computing Surveys 58 (5) (2025) 1–35.doi:10.1145/3769082

    doi:10.1145/3769082 2025

  37. [37]

    Y. Yao, Y. Tian, M. Savvides, Y. Bai, S. Li, Y. Zhang, C. Qian, Q. Sun, H. Wang, R. Zhang, L. Lu, Y. Liu, A survey on large language model (llm) security and privacy: The good, the bad, and the ugly, High-Confidence Computing 4 (2024) 100211.doi:10.1016/j.hcc.2024.100211

    arXiv 2024

  38. [38]

    Pearce, B

    H. Pearce, B. Ahmad, B. Tan, B. Dolan-Gavitt, R. Karri, Asleep at the keyboard? assessing the security of github copilot’s code contributions, in: 2022 IEEE Symposium on Security and Privacy (SP), 2022, pp. 754–768. doi:10.1109/SP46214.2022.9833571

    arXiv 2022

  39. [39]

    J. Bae, S. Kwon, S. Myeong, Enhancing software code vulnerability de- tection using gpt-4o and claude-3.5 sonnet: A study on prompt en- gineering techniques, Electronics 13 (13) (2024) 2657.doi:10.3390/ electronics13132657

    2024

  40. [40]

    Z. Wu, J. He, X. Hu, et al., Prompt-enhanced software vulnerability detection using chatgpt, arXiv preprint arXiv:2308.12697 (2024).doi: 10.48550/arXiv.2308.12697

    Pith/arXiv arXiv doi:10.48550/arxiv.2308.12697 2024

  41. [41]

    Conceição, N

    T. Conceição, N. Cruz, P. Simões, Evaluation of the maturity of llms in the cybersecurity domain, International Journal of Information Security (2025).doi:10.1007/s10207-025-01112-1

    work page doi:10.1007/s10207-025-01112-1 2025

  42. [42]

    Z. Li, Q. Zhang, H. Liu, X. Gu, X. Lu, H. Liu, B. Wang, H. Fan, Z. Zhao, R. Zhang, L. Zhou, Crypformbench: Benchmarking formal anal- ysis capability of large language models for cryptographic schemes, Pro- ceedings of the ACM on Software Engineering 3 (FSE) (2026) 4025–4047. doi:10.1145/3808184

    work page doi:10.1145/3808184 2026

  43. [43]

    White, Q

    J. White, Q. Fu, S. Hays, M. Sandborn, C. Olea, H. Gilbert, A. Elnashar, J. Spencer-Smith, D. C. Schmidt, A prompt pattern catalog to enhance prompt engineering with chatgpt, CoRR abs/2302.11382 (2023).arXiv: 2302.11382,doi:10.48550/ARXIV.2302.11382. 33

    Pith/arXiv arXiv doi:10.48550/arxiv.2302.11382 2023

  44. [44]

    Y. Nong, M. Aldeen, L. Cheng, H. Hu, F. Chen, H. Cai, Chain-of-thought prompting of large language models for discovering and fixing software vulnerabilities, CoRR abs/2402.17230 (2024).arXiv:2402.17230,doi: 10.48550/ARXIV.2402.17230

    Pith/arXiv arXiv doi:10.48550/arxiv.2402.17230 2024

  45. [45]

    X. Wang, D. Zhou, Chain-of-thought reasoning without prompting, Ad- vances in Neural Information Processing Systems 37 (2024) 66383–66409. doi:10.52202/079017-2123

    work page doi:10.52202/079017-2123 2024

  46. [46]

    Agarwal, A

    R. Agarwal, A. Singh, L. Zhang, B. Bohnet, L. Rosias, S. Chan, B. Zhang, A. Anand, Z. Abbas, A. Nova, et al., Many-shot in-context learning, Ad- vances in Neural Information Processing Systems 37 (2024) 76930–76966. doi:10.52202/079017-2447

    doi:10.52202/079017-2447 2024

  47. [47]

    N. T. H. Nguyen, A. Silva, L. Y. Zumot, L. Tupikina, A. Aghasaryan, M. Alam, Thinking before constraining: A unified decoding framework for large language models, CoRR abs/2601.07525 (2026).arXiv:2601.07525, doi:10.48550/ARXIV.2601.07525

    Pith/arXiv arXiv doi:10.48550/arxiv.2601.07525 2026

  48. [48]

    J. Yu, L. Li, Z. Lan, Beyond binary classification: a fine-grained safety dataset for large language models, IEEE Access 12 (2024) 64717–64726. doi:10.1109/access.2024.3393245. AbbreviationsAppendix A. Prompt Used for Protocol Analysis PROMPT_TEMPLATE = """ You are a security protocol verifier using symbolic reasoning. You are given:

    arXiv 2024

  49. [49]

    an anonymized Alice-and-Bob / AnB / AnBx protocol body, and

  50. [50]

    an explicit list of goals to analyze. --- NOTATION REFERENCE --- Use the following Alice-and-Bob notation when interpreting the protocol: Keys: pk(X) : public key of X used for encryption sk(X) : public key of X used for signature verification inv(pk(X)) : private key of X used for decryption inv(sk(X)) : private key of X used for signature shk(X,Y) : pre...

  51. [51]

    Non-injective Agreement: Adds the requirement that A and B agree on specific data items (such as nonces and keys) and the roles they played

  52. [52]

    attack found

    Injective Agreement: The strongest form -- adds a one-to-one relationship between the runs of A and B, preventing replay attacks where B believes multiple runs occurred corresponding to a single run by A. Equivalent to what OFMC/ProVerif verify as injective agreement. Secrecy: Confidentiality: An attacker cannot derive a protected term from intercepted me...