pith. sign in

arxiv: 2605.29465 · v1 · pith:QHYVP4FPnew · submitted 2026-05-28 · 💻 cs.CR

Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin

Leonard Tudorache , Ivan Kurtev , Mark van den Brand This is my paper

Pith reviewed 2026-06-29 06:48 UTC · model grok-4.3

classification 💻 cs.CR
keywords security propertiesformal verificationProVerifTamarintaxonomycryptographic protocolsexecutable modelsmodeling patterns
0
0 comments X

The pith

A taxonomy from 53 recent studies supplies executable models of security properties for ProVerif and Tamarin.

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

The paper sets out to create a structured taxonomy that translates theoretical security properties into forms that protocol designers can directly use in automated verification tools. It draws on recent literature to categorize properties, supply both informal and first-order logic definitions, and include modeling patterns plus working code. A sympathetic reader would care because formal verification often remains inaccessible to those with security rather than verification expertise. If successful, the taxonomy lowers the barrier to checking that protocols actually deliver confidentiality, integrity, and related guarantees.

Core claim

We introduce a systematic and evidence-based taxonomy of security properties derived from a literature review of 53 recent studies that used ProVerif and Tamarin. The taxonomy categorizes and defines these properties with informal definitions for comprehension and rigorous formal definitions in first-order logic, while also detailing modeling patterns and providing executable examples in both tools collected in an open repository.

What carries the argument

The taxonomy itself, which organizes security properties into categories with paired informal and formal definitions plus executable modeling patterns for ProVerif and Tamarin.

If this is right

  • Protocol designers without formal-methods training can now map their requirements directly to tool syntax.
  • Verification models become more consistent across different studies and teams.
  • The open repository of examples serves as a starting point for new protocol analyses.
  • Security properties receive uniform formal definitions that reduce ambiguity in tool input.

Where Pith is reading between the lines

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

  • The taxonomy could be maintained as a living document by periodically re-running the literature review on newer papers.
  • Similar executable taxonomies might be developed for other verification tools such as CryptoVerif or EasyCrypt.
  • The formal definitions could be used to generate automated checks that flag when a model deviates from the intended property.

Load-bearing premise

The 53 studies from 2022-2025 form a representative sample from which a complete and unbiased taxonomy can be built.

What would settle it

A new review of papers from the same period that identifies one or more frequently verified security properties absent from the taxonomy or whose provided models fail to run correctly in the tools.

read the original abstract

Security is critical for everything relying on modern digital systems. Because almost all digital interactions are governed by the Internet and cryptographic protocols, these protocols must serve as reliable mechanisms that guarantee core security properties, such as confidentiality and integrity. Formal verification of these protocols is a critical step in securing interconnected systems. Tools such as ProVerif and Tamarin are widely employed to perform automated verification. However, their effective use demands specialized domain knowledge, creating a significant learning curve for security protocol designers who often have a security, rather than a formal verification background. We therefore need structured, accessible resources to help protocol designers to express their design and requirements in the language of the formal verification tools. To address this, we introduce a systematic and evidence-based taxonomy of security properties. This taxonomy is derived from a literature review of 53 recent studies (2022-2025) that used ProVerif and Tamarin, providing an up-to-date view of verified properties. We systematically categorize and define these properties, providing both informal definitions for intuitive comprehension and rigorous formal definitions expressed in first-order logic for clarity and consistency. We further detail modeling patterns and implement executable examples in both ProVerif and Tamarin, collected in an open repository. This work advances the state of the art by bridging the gap between theoretical security property definitions and their practical, executable verification models.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper claims to introduce a systematic, evidence-based taxonomy of security properties for ProVerif and Tamarin. The taxonomy is derived from a literature review of 53 studies (2022-2025), with informal definitions, rigorous first-order logic formalizations, modeling patterns, and executable examples collected in an open repository. The central goal is to bridge theoretical security property definitions with practical verification models for protocol designers.

Significance. If the taxonomy is shown to be complete and representative, and the executable models correctly capture the properties, the work would offer a practical resource that lowers the barrier for non-experts to use automated verification tools. The provision of an open repository with ProVerif and Tamarin examples is a concrete strength supporting reproducibility and direct usability.

major comments (2)
  1. [Abstract] Abstract, paragraph 2: the claim that the taxonomy is 'systematic and evidence-based' and 'derived from a literature review of 53 recent studies' is load-bearing for the central contribution, yet no search strategy, databases, keywords, inclusion/exclusion criteria, or extraction process is described. Without this, it is impossible to evaluate whether the sample is representative or whether properties have been systematically omitted, directly undermining the 'evidence-based' framing.
  2. [Literature review / taxonomy construction] Literature review description (wherever the 53-study selection is detailed): the absence of any validation that the extracted properties are consistent across studies or that the formal first-order logic definitions match the informal ones and the executable models leaves the soundness of the taxonomy unverified, as the abstract supplies definitions and examples but no cross-checks or completeness argument.
minor comments (1)
  1. [Abstract] The abstract states that executable examples are 'collected in an open repository' but does not include a URL, DOI, or commit hash; adding this would improve immediate accessibility.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for these constructive comments highlighting the need for greater methodological transparency. We address each point below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [Abstract] Abstract, paragraph 2: the claim that the taxonomy is 'systematic and evidence-based' and 'derived from a literature review of 53 recent studies' is load-bearing for the central contribution, yet no search strategy, databases, keywords, inclusion/exclusion criteria, or extraction process is described. Without this, it is impossible to evaluate whether the sample is representative or whether properties have been systematically omitted, directly undermining the 'evidence-based' framing.

    Authors: We agree that the 'evidence-based' framing requires supporting methodological details. In the revised manuscript we will insert a dedicated subsection (likely in Section 2 or a new 'Taxonomy Construction' section) that explicitly describes the search strategy, the databases queried (IEEE Xplore, ACM DL, SpringerLink, Google Scholar), the precise keywords and Boolean combinations employed, the 2022-2025 time window, inclusion criteria (peer-reviewed papers that apply ProVerif or Tamarin to security-protocol verification), exclusion criteria (non-peer-reviewed works, tool tutorials without new protocols, papers outside the date range), and the property-extraction procedure. This addition will allow readers to assess representativeness and potential omissions. revision: yes

  2. Referee: [Literature review / taxonomy construction] Literature review description (wherever the 53-study selection is detailed): the absence of any validation that the extracted properties are consistent across studies or that the formal first-order logic definitions match the informal ones and the executable models leaves the soundness of the taxonomy unverified, as the abstract supplies definitions and examples but no cross-checks or completeness argument.

    Authors: The 53 studies were reviewed manually by the authors; recurring properties were identified and synthesized into the taxonomy. The first-order logic definitions constitute our formalizations of the informal descriptions found in the source papers, while the ProVerif and Tamarin models in the repository were written to realize those same definitions. We did not conduct quantitative inter-rater reliability checks or automated consistency proofs. In revision we will expand the taxonomy-construction narrative to document this derivation process, add a short limitations paragraph acknowledging that the taxonomy is representative rather than formally proven complete or exhaustive, and note that the open repository enables independent verification. A full soundness argument or completeness proof lies outside the paper's scope. revision: partial

Circularity Check

0 steps flagged

No circularity; taxonomy derived from external literature

full rationale

The paper's central derivation is a taxonomy extracted from a review of 53 external studies (2022-2025) that applied ProVerif and Tamarin. No self-citation load-bearing steps, self-definitional reductions, fitted inputs renamed as predictions, or ansatzes smuggled via prior author work appear in the abstract or described methodology. The claim that the taxonomy bridges theory and executable models rests on the external sample rather than reducing to the authors' own inputs by construction. This is the common case of an evidence-based survey whose validity hinges on sample quality, not circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review provides no information on free parameters, axioms, or invented entities; the work is described as a literature-derived taxonomy rather than a derivation resting on new mathematical assumptions.

pith-pipeline@v0.9.1-grok · 5778 in / 1042 out tokens · 24411 ms · 2026-06-29T06:48:32.771504+00:00 · methodology

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

98 extracted references · 66 canonical work pages

  1. [1]

    Version from16, 05–16 (2018)

    Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: Proverif 2.00: automatic cryp- tographic protocol verifier, user manual and tutorial. Version from16, 05–16 (2018)

    2018

  2. [2]

    In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13- 19, 2013

    Meier, S., Schmidt, B., Cremers, C., Basin, D.: The tamarin prover for the symbolic anal- ysis of security protocols. In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13- 19, 2013. Proceedings 25, pp. 696–701 (2013). 18 Springer

    2013

  3. [3]

    In: International Conference on Computer Aided Verification, pp

    Cremers, C.J.: The scyther tool: Verification, falsification, and analysis of security proto- cols: Tool paper. In: International Conference on Computer Aided Verification, pp. 414–418 (2008). Springer

    2008

  4. [4]

    In: Etessami, K., Rajamani, S.K

    Armando, A., Basin, D., Boichut, Y., Cheva- lier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., He´ am, P.C., Kouchnarenko, O., Man- tovani, J., M¨ odersheim, S., Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan` o, L., Vigneron, L.: The avispa tool for the automated validation of internet secu- rity protocols and applications. In: Etessami,...

    2005

  5. [5]

    In: Bhargavan, K., Oswald, E., Prabhakaran, M

    Kobeissi, N., Nicolas, G., Tiwari, M.: Verif- pal: Cryptographic protocol analysis for the real world. In: Bhargavan, K., Oswald, E., Prabhakaran, M. (eds.) Progress in Cryp- tology – INDOCRYPT 2020, pp. 151–202. Springer, Cham (2020)

    2020

  6. [6]

    In: 2025 ACM/IEEE 28th International Confer- ence on Model Driven Engineering Languages and Systems Companion, MODELS-C 2025, pp

    Tudorache, L.: Towards secure iot deploy- ments: A dsl and digital twin-based emu- lation platform for security verification. In: 2025 ACM/IEEE 28th International Confer- ence on Model Driven Engineering Languages and Systems Companion, MODELS-C 2025, pp. 71–76. Institute of Electrical and Elec- tronics Engineers, United States (2025). http s://doi.org/10...

    work page doi:10.1109/models-c68889.2025 2025

  7. [7]

    Applied Sciences 10(12), 4102 (2020) https://doi.org/10.339 0/app10124102

    Tawalbeh, L., Muheidat, F., Tawalbeh, M., Quwaider, M.: IoT Privacy and Security: Challenges and Solutions. Applied Sciences 10(12), 4102 (2020) https://doi.org/10.339 0/app10124102 . Accessed 2025-02-19

    2020

  8. [8]

    Science of Computer Programming63(1), 16–38 (2006) https://doi.org/10.1016/j.scico.2005.07.010

    Aldini, A.: Classification of security proper- ties in a linda-like process algebra. Science of Computer Programming63(1), 16–38 (2006) https://doi.org/10.1016/j.scico.2005.07.010

    work page doi:10.1016/j.scico.2005.07.010 2006

  9. [9]

    (eds.) Classifica- tion of Security Properties: (Part II: Net- work Security)

    Focardi, R., Gorrieri, R., Martinelli, F.: In: Focardi, R., Gorrieri, R. (eds.) Classifica- tion of Security Properties: (Part II: Net- work Security). Lecture Notes in Computer Science, vol. 2946, pp. 139–185. Springer, Berlin, Heidelberg (2004). ht t p s : / / d o i . o r g / 1 0 . 1 0 0 7 / 9 7 8- 3 - 5 4 0 - 2 4 6 3 1 - 24 .http://link.springer.com/10...

    work page doi:10.1007/978-3-540- 2004

  10. [10]

    arXiv:2505.14514 [cs]

    Sayar, I., Messe, N., Ebersold, S., Bruel, J.-M.: From what to how: A taxonomy of formalized security properties (arXiv:2505.14514) (2025) https://doi.org/10.48550/arXiv.2505.14514 . arXiv:2505.14514 [cs]

    work page doi:10.48550/arxiv.2505.14514 2025

  11. [11]

    Euro- pean Journal of Information Systems22(3), 336–359 (2013) https://doi.org/10.1057/ejis .2012.26

    Nickerson, R.C., Varshney, U., Muntermann, J.: A method for taxonomy development and its application in information systems. Euro- pean Journal of Information Systems22(3), 336–359 (2013) https://doi.org/10.1057/ejis .2012.26

    work page doi:10.1057/ejis 2013

  12. [12]

    IEEE Transactions on Infor- mation Theory29(2), 198–208 (1983) http s://doi.org/10.1109/TIT.1983.1056650

    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Infor- mation Theory29(2), 198–208 (1983) http s://doi.org/10.1109/TIT.1983.1056650 . Conference Name: IEEE Transactions on Information Theory. Accessed 2024-06-10

    work page doi:10.1109/tit.1983.1056650 1983

  13. [13]

    In: Democratizing Cryptogra- phy: the Work of Whitfield Diffie and Martin Hellman, pp

    Diffie, W., Hellman, M.E.: New directions in cryptography. In: Democratizing Cryptogra- phy: the Work of Whitfield Diffie and Martin Hellman, pp. 365–390 (2022)

    2022

  14. [14]

    In: Motahhir, S., Bossoufi, B

    Belfaik, Y., Lotfi, Y., Sadqi, Y., Safi, S.: A comparative study of protocols’ security verification tools: Avispa, scyther, proverif, and tamarin. In: Motahhir, S., Bossoufi, B. (eds.) Digital Technologies and Applications, pp. 118–128. Springer, Cham (2024). https: //doi.org/10.1007/978-3-031-68653-5 12

    work page doi:10.1007/978-3-031-68653-5 2024

  15. [15]

    In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp

    Cortier, V., Grimm, N., Lallemand, J., Maffei, M.: A type system for privacy properties. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 409–

    2017

  16. [16]

    https://doi.org/10.1145/3133956.3133998

    ACM, Dallas Texas USA (2017). https://doi.org/10.1145/3133956.3133998 . https://dl.acm.org/doi/10.1145/3133956.3133998 19

    work page doi:10.1145/3133956.3133998 2017

  17. [17]

    In: Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I - Volume I

    Focardi, R., Martinelli, F.: A uniform approach for the definition of security prop- erties. In: Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I - Volume I. FM ’99, pp. 794–813. Springer, Berlin, Heidelberg (1999)

    1999

  18. [18]

    In: 2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS), pp

    Rouland, Q., Hamid, B., Bodeveix, J.-P., Filali, M.: A formal methods approach to security requirements specification and verification. In: 2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 236–241. IEEE, Guangzhou, China (2019). https: //doi.org/10.1109/ICECCS.2019.00033 . https://ieeexplore.ieee.org/document/8882749/

    work page doi:10.1109/iceccs.2019.00033 2019

  19. [19]

    The MIT Press, USA (2012)

    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, USA (2012)

    2012

  20. [20]

    Cam- bridge University Press, USA (2010)

    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cam- bridge University Press, USA (2010)

    2010

  21. [21]

    ACM Trans

    Gelernter, D.: Generative communication in linda. ACM Trans. Program. Lang. Syst. 7(1), 80–112 (1985) https://doi.org/10.1145/ 2363.2433

    work page arXiv 1985

  22. [22]

    Empirical Software Engineering30(5), 117 (2025) https://doi

    Hermann, K., Schneider, S., Tony, C., Yardim, A., Peldszus, S., Berger, T., Scan- dariato, R., Sasse, M.A., Naiakshina, A.: A taxonomy of functional security features and how they can be located. Empirical Software Engineering30(5), 117 (2025) https://doi. org/10.1007/s10664-025-10649-7 . Accessed 2025-08-14

    work page doi:10.1007/s10664-025-10649-7 2025

  23. [23]

    Information and Software Technology51(1), 7–15 (2009) https://doi.org/10.1016/j.in fsof .2008.09.009

    Kitchenham, B., Pearl Brereton, O., Bud- gen, D., Turner, M., Bailey, J., Linkman, S.: Systematic literature reviews in software engineering – a systematic literature review. Information and Software Technology51(1), 7–15 (2009) https://doi.org/10.1016/j.in fsof .2008.09.009 . Special Section - Most Cited Articles in 2002 and Regular Research Papers

    work page doi:10.1016/j.in 2009

  24. [24]

    Jacomme, C., Klein, E., Kremer, S., Racou- chot, M.: A comprehensive, formal and auto- mated analysis of the edhoc protocol, vol. 8, pp. 5881–5898 (2023)

    2023

  25. [25]

    IEEE Transactions on Depend- able and Secure Computing, 1–15 (2024) ht tps://doi.org/10.1109/TDSC.2024.3522895

    Ren, X., Cao, J., Niu, B., Gan, L., Zhang, Y., Xiong, L., Luo, Y., Li, H.: A formal analysis of 5 g prose aka protocols for u2n relay com- munication. IEEE Transactions on Depend- able and Secure Computing, 1–15 (2024) ht tps://doi.org/10.1109/TDSC.2024.3522895

    work page doi:10.1109/tdsc.2024.3522895 2024

  26. [26]

    ASIA CCS ’24, pp

    Wang, B., Li, H., Guan, J.: A formal analysis of data distribution service secu- rity. ASIA CCS ’24, pp. 716–727. Asso- ciation for Computing Machinery, New York, NY, USA (2024). h t t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 6 3 4 7 3 7 . 3 6 5 6 2 8 8 . https://doi.org/10.1145/3634737.3656288

    work page doi:10.1145/3634737.3656288 2024

  27. [27]

    Concurrency and Computation: Practice and Experience35(7) (2023) https: //doi.org/10.1002/cpe.7602

    Chunka, C., Banerjee, S., Sachin Kumar, G.: A secure communication using multifac- tor authentication and key agreement tech- niques in internet of medical things for covid- 19 patients. Concurrency and Computation: Practice and Experience35(7) (2023) https: //doi.org/10.1002/cpe.7602

    work page doi:10.1002/cpe.7602 2023

  28. [28]

    Soft- ware and Systems Modeling (2024) https: //doi.org/10.1007/s10270-024-01201-0

    M´ er´ e, M., Jouault, F., Pallardy, L., Perdriau, R.: Evaluating formal model verification tools in an industrial context: the case of a smart device life cycle management system. Soft- ware and Systems Modeling (2024) https: //doi.org/10.1007/s10270-024-01201-0

    work page doi:10.1007/s10270-024-01201-0 2024

  29. [29]

    IEEE Transactions on Dependable and Secure Computing20(5), 4291–4310 (2023) https://doi.org/10.1109/TDSC.2022.321725 9

    Feng, H., Guan, J., Li, H., Pan, X., Zhao, Z.: Fido gets verified: A formal analysis of the universal authentication framework pro- tocol. IEEE Transactions on Dependable and Secure Computing20(5), 4291–4310 (2023) https://doi.org/10.1109/TDSC.2022.321725 9

    work page doi:10.1109/tdsc.2022.321725 2023

  30. [30]

    In: 2023 IEEE Conference on Standards for Communica- tions and Networking (CSCN), pp

    Bussa, S., Sisto, R., Valenza, F.: Formal ver- ification of the fdo protocol. In: 2023 IEEE Conference on Standards for Communica- tions and Networking (CSCN), pp. 290–295 (2023). https://doi.org/10.1109/CSCN 60443.2023.10453172 . journalAbbrevia- tion: 2023 IEEE Conference on Standards for Communications and Networking (CSCN) 20

    work page doi:10.1109/cscn 2023

  31. [31]

    15396 LNCS, pp

    Moustafa, M., Sethi, M., Aura, T.: Misbind- ing raw public keys to identities in tls, vol. 15396 LNCS, pp. 62–79 (2025). https://doi. org/10.1007/978-3-031-79007-2 4

    work page doi:10.1007/978-3-031-79007-2 2025

  32. [32]

    ASIA CCS ’24, pp

    De Vaere, P., Stoger, F., Perrig, A., Tsudik, G.: The sa4p framework: Sensing and actu- ation as a privilege. ASIA CCS ’24, pp. 873–885. Association for Computing Machin- ery, New York, NY, USA (2024). https: //doi.org/10.1145/3634737.3657006 . https://doi.org/10.1145/3634737.3657006

    work page doi:10.1145/3634737.3657006 2024

  33. [33]

    IEEE Internet of Things Journal11(24), 39323–39332 (2024) https://doi.org/10.1109/JIOT.2024.3422242

    Pradhan, M., Mohanty, S.: A blockchain- assisted multifactor authentication protocol for enhancing iomt security. IEEE Internet of Things Journal11(24), 39323–39332 (2024) https://doi.org/10.1109/JIOT.2024.3422242

    work page doi:10.1109/jiot.2024.3422242 2024

  34. [34]

    IEEE Transac- tions on Services Computing17(5), 2012– 2026 (2024) https://doi.org/10.1109/TSC.20 24.3433534

    Huang, Y., Xu, G., Song, X., Xu, Y.: An effi- cient rlwe-based privacy-preserving authenti- cation scheme based on edge computing in industrial internet of things. IEEE Transac- tions on Services Computing17(5), 2012– 2026 (2024) https://doi.org/10.1109/TSC.20 24.3433534

    work page doi:10.1109/tsc.20 2012

  35. [35]

    (eds.) Information Security and Cryptology – ICISC 2023, vol

    Ahn, T., Kwak, J., Kim, S.: mdtls: How to make middlebox-aware tls more efficient? In: Seo, H., Kim, S. (eds.) Information Security and Cryptology – ICISC 2023, vol. 14562, pp. 39–59 (2024). https://doi.org/10.1007/978-9 81-97-1238-0 3

    work page doi:10.1007/978-9 2023

  36. [36]

    Multimedia Tools and Applications83(23), 63699–63721 (2024) https://doi.org/10.100 7/s11042-024-18114-1

    Saini, K.K., Kaur, D., Kumar, D., Kumar, B.: An efficient three-factor authentication pro- tocol for wireless healthcare sensor networks. Multimedia Tools and Applications83(23), 63699–63721 (2024) https://doi.org/10.100 7/s11042-024-18114-1

    2024

  37. [37]

    Computer Communica- tions220, 81–93 (2024) https://doi.org/10.1 016/j.comcom.2024.04.011

    Zou, S., Cao, Q., Lu, R., Wang, C., Xu, G., Ma, H., Cheng, Y., Xi, J.: A robust and effective 3-factor authentication protocol for smart factory in iiot. Computer Communica- tions220, 81–93 (2024) https://doi.org/10.1 016/j.comcom.2024.04.011

    2024

  38. [38]

    Applied Sciences (Switzerland)13(7) (2023) https://doi.org/10.3390/app13074425

    Liu, K., Zhou, Z., Cao, Q., Xu, G., Wang, C., Gao, Y., Zeng, W., Xu, G.: A robust and effective two-factor authentication (2fa) protocol based on ecc for mobile computing. Applied Sciences (Switzerland)13(7) (2023) https://doi.org/10.3390/app13074425

    work page doi:10.3390/app13074425 2023

  39. [39]

    Applied Sciences (Switzerland)14(21) (2024) https: //doi.org/10.3390/app14219726

    You, I., Kim, J., Pawana, I.W.A.J., Ko, Y.: Mitigating security vulnerabilities in 6g net- works: A comprehensive analysis of the dmrn protocol using svo logic and proverif. Applied Sciences (Switzerland)14(21) (2024) https: //doi.org/10.3390/app14219726

    work page doi:10.3390/app14219726 2024

  40. [40]

    Applied Sciences (Switzerland)14(23) (2024) https://doi.org/10.3390/app142311152

    Ko, Y., Pawana, I.W.A.J., Won, T., Astillo, P.V., You, I.: Toward an era of secure 5g con- vergence applications: Formal security verifi- cation of 3gpp akma with tls 1.3 psk option. Applied Sciences (Switzerland)14(23) (2024) https://doi.org/10.3390/app142311152

    work page doi:10.3390/app142311152 2024

  41. [41]

    ACM Trans

    Ahmed, A.S., Peltonen, A., Sethi, M., Aura, T.: Security analysis of the consumer remote sim provisioning protocol. ACM Trans. Priv. Secur.27(3) (2024) https://doi.org/10.1145/ 3663761

    2024

  42. [42]

    CODASPY ’23, pp

    Duttagupta, S., Marin, E., Singelee, D., Preneel, B.: Hat: Secure and practical key establishment for implantable medi- cal devices. CODASPY ’23, pp. 213–224. Association for Computing Machinery, New York, NY, USA (2023). h t t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 5 7 7 9 2 3 . 3 5 8 3 6 4 6 . https://doi.org/10.1145/3577923.3583646

    work page doi:10.1145/3577923.3583646 2023

  43. [43]

    CMES - Computer Modeling in Engineering and Sciences134(1), 317–341 (2022) https://doi.org/10.32604/cmes.2022.0 19595

    Wu, T.-Y., Meng, Q., Yang, L., Kumari, S., Pirouz, M.: Amassing the security: An enhanced authentication and key agreement protocol for remote surgery in healthcare environment. CMES - Computer Modeling in Engineering and Sciences134(1), 317–341 (2022) https://doi.org/10.32604/cmes.2022.0 19595

    work page doi:10.32604/cmes.2022.0 2022

  44. [44]

    Journal of Systems Architecture138(2023) https: //doi.org/10.1016/j.sysarc.2023.102869

    Xie, X., Wu, B., Hou, B.: Bephap: A blockchain-based efficient privacy-preserving handover authentication protocol with key agreement for internet of vehicles. Journal of Systems Architecture138(2023) https: //doi.org/10.1016/j.sysarc.2023.102869

    work page doi:10.1016/j.sysarc.2023.102869 2023

  45. [45]

    IET Communications18(14), 21 846–859 (2024) https://doi.org/10.1049/cm u2.12794

    Zarbi, N., Zaeembashi, A., Bagheri, N., Adeli, M.: Toward designing a lightweight rfid authentication protocol for constrained environments. IET Communications18(14), 21 846–859 (2024) https://doi.org/10.1049/cm u2.12794

    work page doi:10.1049/cm 2024

  46. [46]

    Electronics (Switzerland)12(5) (2023) https: //doi.org/10.3390/electronics12051217

    Kim, K., Ryu, J., Lee, H., Lee, Y., Won, D.: Distributed and federated authentication schemes based on updatable smart contracts. Electronics (Switzerland)12(5) (2023) https: //doi.org/10.3390/electronics12051217

    work page doi:10.3390/electronics12051217 2023

  47. [47]

    Journal of Parallel and Distributed Comput- ing179, 104714 (2023) https://doi.org/10.1 016/j.jpdc.2023.104714

    Li, Y.: A secure and efficient three-factor authentication protocol for iot environments. Journal of Parallel and Distributed Comput- ing179, 104714 (2023) https://doi.org/10.1 016/j.jpdc.2023.104714

    arXiv 2023

  48. [48]

    Computers & Security126, 103072 (2023) https://doi.org/10.1016/j.cose .2022.103072

    Miculan, M., Vitacolonna, N.: Automated verification of telegram’s mtproto 2.0 in the symbolic model. Computers & Security126, 103072 (2023) https://doi.org/10.1016/j.cose .2022.103072

    work page doi:10.1016/j.cose 2023

  49. [49]

    Computers 12(1) (2023) https://doi.org/10.3390/comp uters12010002

    Akman, G., Ginzboorg, P., Damir, M.T., Niemi, V.: Privacy-enhanced akma for multi- access edge computing mobility†. Computers 12(1) (2023) https://doi.org/10.3390/comp uters12010002

    work page doi:10.3390/comp 2023

  50. [50]

    International Journal on Software Tools for Technology Transfer 26(4), 495–508 (2024) https://doi.org/10.1 007/s10009-024-00759-w

    Bodei, C., De Vincenzi, M., Matteucci, I.: Formal analysis of an autosar-based basic software module. International Journal on Software Tools for Technology Transfer 26(4), 495–508 (2024) https://doi.org/10.1 007/s10009-024-00759-w

    2024

  51. [51]

    CODASPY ’24, pp

    Wang, Y., Laing, T., Moreira, J., Ryan, M.D.: Remote registration of multiple authentica- tors. CODASPY ’24, pp. 379–390. Asso- ciation for Computing Machinery, New York, NY, USA (2024). h t t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 6 2 6 2 3 2 . 3 6 5 3 2 7 3 . https://doi.org/10.1145/3626232.3653273

    work page doi:10.1145/3626232.3653273 2024

  52. [52]

    CCS ’23, pp

    Bursuc, S., Horne, R., Mauw, S., Yurkov, S.: Provably unlinkable smart card-based payments. CCS ’23, pp. 1392–1406. Asso- ciation for Computing Machinery, New York, NY, USA (2023). h t t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 5 7 6 9 1 5 . 3 6 2 3 1 0 9 . https://doi.org/10.1145/3576915.3623109

    work page doi:10.1145/3576915.3623109 2023

  53. [53]

    Zhu, N., Xu, J., Cui, B.: Formal Analysis of 5G EAP-TLS 1.3, vol. 193, pp. 140–151 (2024). https://doi.org/10.1007/978-3-031-5 3555-0 14

    work page doi:10.1007/978-3-031-5 2024

  54. [54]

    FPGA ’25, pp

    Feng, Y., Wang, Z., Bobda, C.: Civic- fpga: A trusted fpga design validation by multi-tenant cloud providers. FPGA ’25, pp. 139–145. Association for Comput- ing Machinery, ??? (2025). ht t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 7 0 6 6 2 8 . 3 7 0 8 8 2 6 . https://doi.org/10.1145/3706628.3708826

    work page doi:10.1145/3706628.3708826 2025

  55. [55]

    In: 2023 IEEE International Conference on Cyber Security and Resilience (CSR), pp

    Bussa, S., Sisto, R., Valenza, F.: Formal ver- ification of a v2x privacy preserving scheme using proverif. In: 2023 IEEE International Conference on Cyber Security and Resilience (CSR), pp. 341–346 (2023). https://doi. org/10.1109/CSR57506.2023.10224908 . journalAbbreviation: 2023 IEEE Interna- tional Conference on Cyber Security and Resilience (CSR)

    work page doi:10.1109/csr57506.2023.10224908 2023

  56. [56]

    14896 LNCS, pp

    Watanabe, K., Yoneyama, K.: Formal veri- fication of challenge flow in emv 3-d secure, vol. 14896 LNCS, pp. 290–310 (2024). https: //doi.org/10.1007/978-981-97-5028-3 15

    work page doi:10.1007/978-981-97-5028-3 2024

  57. [57]

    APKC ’24, pp

    Fujita, K., Yoneyama, K.: Formal verifica- tion of wireless charging standard qi. APKC ’24, pp. 23–31. Association for Computing Machinery, New York, NY, USA (2024). ht tps://doi.org/10.1145/3659467.3659904 . https://doi.org/10.1145/3659467.3659904

    work page doi:10.1145/3659467.3659904 2024

  58. [58]

    Mathematics13(7) (2025) https://doi.org/10.3390/math130711 18

    Wang, S., Wu, Y., Wen, K., Zhou, X., Hu, B., Xie, Q.: An improved blockchain- based lightweight vehicle-to-infrastructure handover authentication protocol for vehic- ular ad hoc networks. Mathematics13(7) (2025) https://doi.org/10.3390/math130711 18

    work page doi:10.3390/math130711 2025

  59. [59]

    Seo, K.-M., Kim, J., Lee, S., Kwon, J.-W., Seo, S.-H.: Efficient remote identification for drone swarms, vol. 76, pp. 2937–2958 (2023). https://doi.org/10.32604/cmc.2023.039459

    work page doi:10.32604/cmc.2023.039459 2023

  60. [60]

    Arabian Journal for Science and Engineering 48(2), 1947–1971 (2023) https://doi.org/10 .1007/s13369-022-07055-2 22

    Rangwani, D., Om, H.: A robust four-factor authentication protocol for resource mining. Arabian Journal for Science and Engineering 48(2), 1947–1971 (2023) https://doi.org/10 .1007/s13369-022-07055-2 22

    1947

  61. [61]

    Cremers, C., Jacomme, C., Naska, A.: For- mal analysis of session-handling in secure messaging: Lifting security from sessions to conversations, vol. 2, pp. 1235–1252 (2023)

    2023

  62. [62]

    Journal of Healthcare Engi- neering2023(2023) https://doi.org/10.115 5/2023/4845850

    Xie, Q., Liu, D., Ding, Z., Tan, X., Han, L.: Provably secure and lightweight patient monitoring protocol for wireless body area network in ioht. Journal of Healthcare Engi- neering2023(2023) https://doi.org/10.115 5/2023/4845850

    2023

  63. [63]

    Ad Hoc Networks154, 103349 (2024) https://doi.org/10.1016/j.adhoc.2023 .103349

    Shahrouz, J.K., Analoui, M.: An anony- mous authentication scheme with conditional privacy-preserving for vehicular ad hoc net- works based on zero-knowledge proof and blockchain. Ad Hoc Networks154, 103349 (2024) https://doi.org/10.1016/j.adhoc.2023 .103349

    work page doi:10.1016/j.adhoc.2023 2024

  64. [64]

    Journal of Computer Virology and Hacking Techniques19(1), 17– 32 (2023) https://doi.org/10.1007/s11416-0 22-00444-z

    Raimondo, M., Bernardi, S., Marrone, S., Merseguer, J.: An approach for the auto- matic verification of blockchain protocols: the tweetchain case study. Journal of Computer Virology and Hacking Techniques19(1), 17– 32 (2023) https://doi.org/10.1007/s11416-0 22-00444-z

    work page doi:10.1007/s11416-0 2023

  65. [65]

    ACSAC ’22, pp

    Sabry, M., Samavi, R.: Archivesafe lt: Secure long-term archiving system. ACSAC ’22, pp. 936–948. Association for Comput- ing Machinery, ??? (2022). ht t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 5 6 4 6 2 5 . 3 5 6 4 6 3 5 . https://doi.org/10.1145/3564625.3564635

    work page doi:10.1145/3564625.3564635 2022

  66. [66]

    ARES ’24

    Wagner, P.G., Birnstill, P., Beyerer, J.: Dds security+: Enhancing the data distri- bution service with tpm-based remote attes- tation. ARES ’24. Association for Com- puting Machinery, ??? (2024). ht t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 6 6 4 4 7 6 . 3 6 7 0 4 4 2 . https://doi.org/10.1145/3664476.3670442

    work page doi:10.1145/3664476.3670442 2024

  67. [67]

    ASIA CCS ’24, pp

    Baloglu, S., Bursuc, S., Mauw, S., Pang, J.: Formal verification and solutions for estonian e-voting. ASIA CCS ’24, pp. 728–741. Asso- ciation for Computing Machinery, ??? (2024). https://doi.org/10.1145/3634737.3657009 . https://doi.org/10.1145/3634737.3657009

    work page doi:10.1145/3634737.3657009 2024

  68. [68]

    ASIA CCS ’22, pp

    Hu, S., Zhang, Q., Weimerskirch, A., Mao, Z.M.: Gatekeeper: A gateway-based broad- cast authentication protocol for the in- vehicle ethernet. ASIA CCS ’22, pp. 494–

  69. [69]

    ht t p s : / / d o i

    Association for Computing Machinery, New York, NY, USA (2022). ht t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 4 8 8 9 3 2 . 3 5 1 7 3 9 6 . https://doi.org/10.1145/3488932.3517396

    work page doi:10.1145/3488932.3517396 2022

  70. [70]

    ACSAC ’23, pp

    Pietro, T., Savio, S., Roberto, D.P.: Lightweight privacy-preserving proximity discovery for remotely-controlled drones. ACSAC ’23, pp. 178–189. Association for Computing Machinery, ??? (2023). https://doi.org/10.1145/3627106.3627174 . https://doi.org/10.1145/3627106.3627174

    work page doi:10.1145/3627106.3627174 2023

  71. [71]

    In: 2023 IEEE Smart World Congress (SWC), pp

    Song, Y., Jiang, F., Shah, S.W.A., Doss, R.: Multi-factor continuous authentication of drivers leveraging smartphone. In: 2023 IEEE Smart World Congress (SWC), pp. 1–9 (2023). https://doi.org/10.1109/SWC57546 .2023.10449311 . journalAbbreviation: 2023 IEEE Smart World Congress (SWC)

    work page doi:10.1109/swc57546 2023

  72. [72]

    In: 2024 IEEE 37th Computer Security Founda- tions Symposium (CSF), pp

    Fila, B., Radomirovi´ c, S.: Nothing is out- of-band: Formal modeling of ceremonies. In: 2024 IEEE 37th Computer Security Founda- tions Symposium (CSF), pp. 464–478 (2024). https://doi.org/10.1109/CSF61375.2024.00 049 . journalAbbreviation: 2024 IEEE 37th Computer Security Foundations Symposium (CSF)

    work page doi:10.1109/csf61375.2024.00 2024

  73. [73]

    IEEE Transactions on Computational Social Sys- tems10(3), 1039–1056 (2023) https://doi.or g/10.1109/TCSS.2022.3162869

    Lu, S., Li, Z., Miao, X., Han, Q., Zheng, J.: Piws: Private intersection weighted sum protocol for privacy-preserving score-based voting with perfect ballot secrecy. IEEE Transactions on Computational Social Sys- tems10(3), 1039–1056 (2023) https://doi.or g/10.1109/TCSS.2022.3162869

    work page doi:10.1109/tcss.2022.3162869 2023

  74. [74]

    ASIA CCS ’24, pp

    Lafourcade, P., Mahmoud, D., Marcadet, G., Olivier-Anclin, C.: Transferable, auditable and anonymous ticketing protocol. ASIA CCS ’24, pp. 1911–1927. Association for Computing Machinery, ??? (2024). https: //doi.org/10.1145/3634737.3645008 . https://doi.org/10.1145/3634737.3645008

    work page doi:10.1145/3634737.3645008 1911

  75. [75]

    ASPLOS ’25, pp

    Giantsidi, D., Pritzi, J., Gust, F., Katsarakis, A., Koshiba, A., Bhatotia, P.: Tnic: A trusted 23 nic architecture: A hardware-network sub- strate for building high-performance trust- worthy distributed systems. ASPLOS ’25, pp. 1282–1301. Association for Comput- ing Machinery, ??? (2025). ht t p s : / / d o i . o r g / 1 0 . 1 1 4 5 / 3 6 7 6 6 4 1 . 3 7...

    work page doi:10.1145/3676641.3716277 2025

  76. [76]

    CCS ’24, pp

    Li, Y., Jin, J., Levchenko, K.: Capsid: A private session id system for small uavs. CCS ’24, pp. 1791–1805. Association for Computing Machinery, ??? (2024). https: //doi.org/10.1145/3658644.3690324 . https://doi.org/10.1145/3658644.3690324

    work page doi:10.1145/3658644.3690324 2024

  77. [77]

    13619 LNCS, pp

    Rakeei, M., Giustolisi, R., Lenzini, G.: Secure internet exams despite coercion, vol. 13619 LNCS, pp. 85–100 (2023). https://doi.org/10 .1007/978-3-031-25734-6 6

    2023

  78. [78]

    In: Proceedings 10th Com- puter Security Foundations Workshop, pp

    Lowe, G.: A hierarchy of authentication specifications. In: Proceedings 10th Com- puter Security Foundations Workshop, pp. 31–43. IEEE Comput. Soc. Press, Rock- port, MA, USA (1997). h t t p s : / / d o i . o r g / 1 0 . 1 1 0 9 / C S F W . 1 9 9 7 . 5 9 6 7 82 . http://ieeexplore.ieee.org/document/596782/

    1997

  79. [79]

    The Tamarin Team: Tamarin Prover Manual: Security Protocol Analysis in the Symbolic Model. (2024). https://tamarin-prover.com/ manual/master/tex/tamarin-manual.pdf

    2024

  80. [80]

    Biba, K.J.: Integrity considerations for secure computer systems (522) (1977)

    1977

Showing first 80 references.