Pith. sign in

REVIEW 4 major objections 6 minor 34 references

CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection

T0 review · 4 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read 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…

desk verdict 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. read the letter →

arxiv 2411.13627 v1 pith:HAXUVWID submitted 2024-11-20 cs.CR cs.AIcs.SC

Cristian Curaba , Denis D'Ambrosi , Alessandro Minisini , Natalia Pérez-Campanero Antolín This is my paper · ORCID
classification cs.CRcs.AIcs.SC
keywords cryptographicprotocolsformalverificationLLMagentsTamarinprovervulnerabilitydetectionbenchmarkDolev-Yaomodelsymbolicreasoning
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

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.

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 (4)
  1. [Section 4, Figure 2] 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.
  2. [Section 3.3, footnote 4; Section 1.1] 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.
  3. [Section 3.2] 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).
  4. [Section 4; Section 5] 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.
minor comments (6)
  1. [Appendix B] The sentence 'From Table 2 and Table 2' should presumably be 'From Table 1 and Table 2'.
  2. [Appendix D] In the Protocol 5 entry for o1-preview, 'coping' should be 'copying'.
  3. [Appendix C] In the Protocol 3 entry, 'propriety' should be 'property'.
  4. [Section 3.1] 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.'
  5. [Section 3.3] 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.
  6. [Section 4] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper is an empirical benchmark study, not a derivation, and none of its central claims reduce to their own inputs by construction.

full rationale

CryptoFormalEval is an empirical benchmark paper rather than a derivation paper; no quantity is derived from another within the paper in a way that collapses to its own inputs. The protocol labels are manually curated inputs, and the model scores are manually assigned ratings. The paper itself discloses that the automated validation sandbox is not fully implemented (Section 3.3, footnote 4) and that final output is manually evaluated (Section 1.1), which is a limitation on objectivity but not a circular step. The mismatch between the headline capability (vulnerability detection) and the rubric (Tamarin code quality) evidenced in Appendix D is a construct-validity concern, not a formal circularity. There are no self-citations, no imported uniqueness theorems, and no fitted parameters renamed as predictions. Consequently, the circularity score is 0.

Assumptions & free parameters 4 free parameters · 4 assumptions · 0 invented entities

The central claim depends on no fitted mathematical constants. The hand-set hyperparameters are experimental configuration choices. The major uncharged assumptions are the correctness of the manually assigned vulnerability labels, Tamarin's soundness and completeness guarantee, the adequacy of the Dolev-Yao model, and the novelty of the generated protocols. No new theoretical entities are postulated; the middleware, sandbox, and agent architecture are software artifacts whose evidence is the unreleased repository and the described behavior.

free parameters (4)
  • temperature = 0.1, except o1-preview which defaults to 1
    Chosen by hand in Section 4; affects randomness of model outputs and therefore the reported performance.
  • max_api_calls_per_run = 20
    Set in Section 4; the agent is evaluated on whether it succeeds within this budget, so the number determines the result.
  • max_subtask_repetition = 3
    Set in Section 4; limits how many times the agent may retry a subtask, directly affecting error correction performance.
  • execution_timeout = 200 seconds
    Set in Section 4; a threshold for terminating Tamarin commands, though never reached during the experiments.
assumptions (4)
  • domain assumption The Dolev-Yao model captures the relevant security properties of the protocols
    Section 2.1 adopts Dolev-Yao; attacks outside this symbolic model are excluded from the benchmark.
  • domain assumption Tamarin's attack search is sound and complete with respect to the Dolev-Yao model
    Section 2.3 relies on this property of the prover for the validity of any found attack traces.
  • domain assumption Each dataset protocol contains exactly the manually assigned vulnerability and no unintended flaws
    Section 3.2 states the dataset is manually validated; no formal proof of the labels is provided for the full dataset.
  • domain assumption The protocols are genuinely novel and unseen by the tested LLMs
    Section 3.2 claims novelty and restricted distribution, but the protocols were generated with GPT-4 and contamination cannot be ruled out for GPT-family test models.

how reviews work

0 comments
Cite this review

Pith. "Pith review of CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection." pith.science (2026). https://pith.science/paper/HAXUVWID

@misc{pith2026241113627,
  author       = {Pith},
  title        = {Pith review of: CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HAXUVWID}},
  note         = {Machine review of arXiv:2411.13627}
}
read the original abstract

Cryptographic protocols play a fundamental role in securing modern digital infrastructure, but they are often deployed without prior formal verification. This could lead to the adoption of distributed systems vulnerable to attack vectors. Formal verification methods, on the other hand, require complex and time-consuming techniques that lack automatization. In this paper, we introduce a benchmark to assess the ability of Large Language Models (LLMs) to autonomously identify vulnerabilities in new cryptographic protocols through interaction with Tamarin: a theorem prover for protocol verification. We created a manually validated dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents. Our results about the performances of the current frontier models on the benchmark provides insights about the possibility of cybersecurity applications by integrating LLMs with symbolic reasoning systems.

Figures

Figures reproduced from arXiv: 2411.13627 by the authors.

Figure 1
Figure 1. Overview of the benchmark’s structure. The AI agent must identify a vulnerability in a novel protocol within a predetermined number of API calls by interacting with the Tamarin prover and iteratively adapting to its feedback until an attack is found. through a graphical interface. However, AI agents require command-line accessibility to automate interactions. To ad￾dress this, we developed a middleware system to ena… view at source ↗
Figure 2
Figure 2. Comparative performance evaluation of different frontier LLMs across five security protocol verification tasks (detailed in Appendix B). Performance ratings: 1 - Major difficulties with instruction following and frequent syntax errors; 2 - Basic Tamarin code generation with adaptation to feedback, but presence of trivial semantic errors; 3 - Production of syntactically valid Tamarin code with conceptual mistakes; 4 … view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 27 canonical work pages

  1. [1]

    URL https: //app.grayswan.ai/arena/leaderboard

    Gray swan ai arena: Leaderboard, 2024. URL https: //app.grayswan.ai/arena/leaderboard. Ac- cessed: 2024-10-22

    work page 2024

  2. [2]

    K., Näslund, M., O’Hanlon, P., Papay, J., Suomalainen, J., Surridge, M., Wary, J.-P., and Zahariev, A

    Arfaoui, G., Bisson, P., Blom, R., Borgaonkar, R., Englund, H., Félix, E., Klaedtke, F., Nakarmi, P. K., Näslund, M., O’Hanlon, P., Papay, J., Suomalainen, J., Surridge, M., Wary, J.-P., and Zahariev, A. A security architecture for 5g networks. IEEE Access, 6:22466–22479, 2018. doi: 10.1109/ACCESS. 2018.2827419

    arXiv 2018

  3. [3]

    and Compagna, L

    Armando, A. and Compagna, L. Satmc: A sat-based model checker for security protocols. In Logics in Artifi- cial Intelligence, volume 3229, pp. 730–733. Springer Berlin Heidelberg, Sep 2004. ISBN 978-3-540-23242-1. doi: 10.1007/978-3-540-30227-8_68

    work page doi:10.1007/978-3-540-30227-8_68 2004

  4. [4]

    Alice and bob meet equational theories

    Basin, D., Keller, M., Radomirovi´c, S., and Sasse, R. Alice and bob meet equational theories. Logic, Rewriting, and Concurrency: Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday, pp. 160–180, 2015

    work page 2015

  5. [5]

    Ex- ploring the dark side of ai: Advanced phishing attack design and deployment using chatgpt

    Begou, N., Vinoy, J., Duda, A., and Korczy ´nski, M. Ex- ploring the dark side of ai: Advanced phishing attack design and deployment using chatgpt. In 2023 IEEE Conference on Communications and Network Security (CNS), pp. 1–6. IEEE, 2023

    work page 2023

  6. [6]

    Denning, D. E. and Sacco, G. M. Timestamps in key dis- tribution protocols. Commun. ACM, 24(8):533–536, aug

    work page

  7. [7]

    and Yao, A

    Dolev, D. and Yao, A. On the security of public key protocols. IEEE Transactions on information theory, 29(2):198–208, 1983

    work page 1983

  8. [8]

    Doumbouya, M. K. B., Nandi, A., Poesia, G., Ghilardi, D., Goldie, A., Bianchi, F., Jurafsky, D., and Manning, C. D. h4rm3l: A dynamic benchmark of composable jailbreak attacks for llm safety assessment, 2024. URL https:// arxiv.org/abs/2408.04811

    arXiv 2024

Show all 34 references
  1. [9]

    Maude-npa: Cryptographic protocol analysis modulo equational proper- ties

    Escobar, S., Meadows, C., and Meseguer, J. Maude-npa: Cryptographic protocol analysis modulo equational proper- ties. In International School on Foundations of Security Analysis and Design, pp. 1–50. Springer, 2007

    2007

  2. [10]

    and Goldreich, O

    Even, S. and Goldreich, O. On the security of multi-party ping-pong protocols. In 24th Annual Symposium on Foun- dations of Computer Science (sfcs 1983), pp. 34–39. IEEE, 1983

    1983

  3. [11]

    Llm agents can autonomously exploit one-day vulnerabilities

    Fang, R., Bindu, R., Gupta, A., and Kang, D. Llm agents can autonomously exploit one-day vulnerabilities. arXiv preprint arXiv:2404.08144, 2024

    2024 arXiv

  4. [12]

    The OAuth 2.0 Authorization Framework

    Hardt, D. The OAuth 2.0 Authorization Framework. RFC 6749, October 2012. URLhttps://www.rfc-editor. org/info/rfc6749

    2012

  5. [13]

    Logic-lm++: Multi-step refinement for symbolic formulations, 2024

    Kirtania, S., Gupta, P., and Radhakirshna, A. Logic-lm++: Multi-step refinement for symbolic formulations, 2024. URL https://arxiv.org/abs/2407.02514

    2024 arXiv

  6. [14]

    Li, W., Yu, L., Wu, Y ., and Paulson, L. C. Isarstep: a bench- mark for high-level mathematical reasoning. arXiv preprint arXiv:2006.09265, 2020

    2006 arXiv

  7. [15]

    Lonvick, C. M. and Ylonen, T. The Secure Shell (SSH) Protocol Architecture. RFC 4251, January 2006. URL https://www.rfc-editor.org/info/rfc4251

    2006

  8. [16]

    An attack on the needham- schroeder public- key authentication protocol

    Lowe, G. An attack on the needham- schroeder public- key authentication protocol. Information processing letters, 56 (3), 1995

    1995

  9. [17]

    The tamarin prover for the symbolic analysis of security pro- tocols

    Meier, S., Schmidt, B., Cremers, C., and Basin, D. The tamarin prover for the symbolic analysis of security pro- tocols. In Computer Aided Verification , volume 8044, pp. 696–701, Jul 2013. ISBN 978-3-642-39798-1. doi: 10.1007/978-3-642-39799-8_48

    2013 doi

  10. [18]

    Needham, R. M. and Schroeder, M. D. Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993–999, Dec 1978. doi: 10.1145/359657. 359659

    1978 doi

  11. [19]

    and Nakabayashi, M

    Ohno, K. and Nakabayashi, M. A security verification framework of cryptographic protocols using machine learn- ing, 2023. URL https://arxiv.org/abs/2304. 13249

    2023

  12. [20]

    and Guven, E

    Renze, M. and Guven, E. Self-reflection in llm agents: Effects on problem-solving performance. arXiv preprint arXiv:2405.06682, 2024

    2024 arXiv

  13. [21]

    An in-context learning agent for formal theorem- proving, 2024

    Thakur, A., Tsoukalas, G., Wen, Y ., Xin, J., and Chaud- huri, S. An in-context learning agent for formal theorem- proving, 2024. URLhttps://arxiv.org/abs/2310. 04353

    2024

  14. [22]

    The cl-atse protocol analyser

    Turuani, M. The cl-atse protocol analyser. In Term Rewrit- ing and Applications, Lecture Notes in Computer Science , volume 4098, pp. 277–286, Aug 2006. ISBN 978-3-540- 36834-2. doi: 10.1007/11805618_21

    2006 doi

  15. [23]

    not Ex party mess #t1 #t2 . FreshTerm(party, mess)@#t1 & FreshTerm(party, mess)@#t2 & #t1 < #t2

    Wu, Y ., Jiang, A. Q., Li, W., Rabe, M. N., Staats, C., Jamnik, M., and Szegedy, C. Autoformalization with large language models, 2022. URL https://arxiv.org/abs/2205. 12615. 8 CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vuln...

    2022

  16. [25]

    ```shell

    Saving the file: ``` cat << 'EOF' > Agent_execution/protocol.anb Protocol Protocol2: Knowledge: [...] EOF ``` The following output is from Task 1.3 in executing Protocol 3 with core model Claude 3 Haiku. The output format required is not respected (missing “ ```shell ”). Outpu...

  17. [26]

    This would tie the sessions together

    Include a fresh nonce from B in the second message that A must echo back in the third message. This would tie the sessions together

  18. [27]

    Have both parties contribute fresh randomness that is mixed into the encryption key for each session

  19. [28]

    ``` **Next step** A similar behaviour can be drawn also from Protocol 2 execution (Claude 3 opus)

    Use timestamps or sequence numbers to ensure messages cannot be replayed from old sessions. ``` **Next step** A similar behaviour can be drawn also from Protocol 2 execution (Claude 3 opus). Output: Here is the analysis of the Tamarin feedback and the steps to address the iden...

  20. [29]

    Tamarin successfully loaded, translated, and analyzed the Protocol2 theory

  21. [30]

    The secrecy lemma was falsified, meaning Tamarin found an attack trace where the secret message M was revealed to the attacker

  22. [31]

    The attack trace shows: - The attacker sends the constant 'zero' to B - B responds with the shared key XORed with 'zero', revealing the key to the attacker - A sends a fresh nonce Na to the attacker - The attacker sends back Na XORed with the compromised shared key - A encrypt...

  23. [32]

    This directly reveals the key

    In rule B_1, B should not respond to an arbitrary message from the network by XORing it with the shared key. This directly reveals the key

  24. [33]

    The protocol should be redesigned with proper authentication of the messages, for example using a challenge-response with the nonces

  25. [34]

    Here are the changes made to the theory file to implement these fixes: ```shell execute: cat << 'EOF' > Agent_execution/final_protocol_and_property.spthy theory Protocol2 [...] 16

    The encryption of M should not be done by XORing it with the nonce, as this allows the attacker to cancel out the nonce if it can learn it. Here are the changes made to the theory file to implement these fixes: ```shell execute: cat << 'EOF' > Agent_execution/final_protocol_an...

  26. [1981]

    doi: 10.1145/358722.358740

    ISSN 0001-0782. doi: 10.1145/358722.358740. URL https://doi.org/10.1145/358722.358740. 7 CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.