Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin Leonard Tudorache1*, Ivan Kurtev1 and Mark van den Brand1 1*
arXiv:2605.29465v1 [cs.CR] 28 May 2026
Department of Mathematics and Computer Science, Eindhoven University of Technology, Groene Loper 3, Eindhoven, 5612 AE, North Brabant, The Netherlands.
*Corresponding author(s). E-mail(s): [email protected]; 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. Keywords: Formal Verification, Taxonomy, Security Properties, Modeling Patterns
1 Introduction
Formal verification techniques offer a structured approach to identifying flaws in security protocols, making them a crucial component in the design process. Numerous automated tools have been developed for this purpose, including ProVerif [1], Tamarin [2], Scyther [3], AVISPA [4], and Verifpal [5], among others. These tools allow their users to model their security protocols and specify the security properties to be checked. Then they perform a verification process where all the
Security protocols are used to define the way interconnected systems interact. They include a step-by-step description, usually accompanied by a sequence diagram that aims to guide the implementation. Furthermore, security properties are defined as requirements for such protocols, which can be verified by hand or in an automated manner before the actual implementation.
1
possible paths are verified, providing step-by-step traces that highlight if a property does not hold. Automated verification tools for security protocols often require domain-specific and toolspecific expertise to be used effectively, and each tool has different capabilities and limitations. As a result, users must acquire in-depth knowledge of multiple tools to thoroughly and formally verify the security of their protocols. Moreover, developers of the automated verification tools usually have a formal verification background and might have a different approach than protocol designers, who often have a security background. This mismatch in expertise often results in a steep learning curve, as protocol designers must gain additional formal verification knowledge to model and analyze their systems accurately. For instance, to verify a simple authentication property in Tamarin, a protocol designer must learn to express it as multiset rewriting rules over a global state, while the same property in ProVerif requires expressing it in terms of processes and events in ProVerif’s applied pi calculus-based input language. These are two fundamentally different formalisms that demand significant background knowledge before any protocol-specific work can begin. Developers of automated verification tools need to invest in transferring observations back to the protocol world, ensuring that formal analysis results are meaningful and actionable for security engineers. Thus, there is a clear need for a user-friendly approach that abstracts the complexity involved in formally verifying security protocols. As we highlighted in our previous work [6], there is a lack of efficient and robust security protocols [7], and the complexity of security testing is high. The next step after defining a security protocol is to verify it. There are various approaches available to verify protocols, ranging from mathematical proofs to automated verification via specialized tools. Nevertheless, all require a deep understanding of the security properties targeted by a protocol. There are various classifications of security properties in the literature [8–10], but these do not include all security properties that are verified nowadays and often use a lower level of abstraction, by using rigorous formal specification to define the properties, making it more difficult for security protocol designers to understand them. Furthermore, they do not provide examples
of how to model them and integrate them into security protocols. The lack of a systematic classification creates a gap in understanding how security properties are used in security protocols by practitioners and how these can be modeled and verified using automated verification tools. Therefore, there is a need for a structured taxonomy that defines security properties that are currently verified by protocol designers. To the best of our knowledge, there is no classification of security properties that provides a common and formal understanding of all security properties identified in the current literature. Therefore, a taxonomy, which is a structured system for classifying and organizing concepts into groups (often hierarchical) [11], would provide a foundation for security protocol verification, to help protocol designers understand how to model fundamental security protocols and verify them using automated verification tools. Furthermore, this taxonomy, paired with modeling patterns, gives users a clear path from property selection to executable verification, cutting through the varying definitions and tool-specific syntax that currently make the process unnecessarily difficult. We propose a taxonomy by systematically extracting and categorizing security properties verified with ProVerif and Tamarin over the past three years from the tool-based property verification literature. We aim to provide both formal and informal definitions and create a repository containing example models for ProVerif and Tamarin that represent how each property of the taxonomy can be specified and verified. This aims to aid protocol designers in starting their verification process using these tools. First, the taxonomy provides both an informal and a formal definition of the security property. Then, the users can employ the modeling patterns presented in the ProVerif and Tamarin models for each security property, following a simple guide on how to apply the verification queries to their protocols, or use the example models as a starting skeleton for a protocol. In this paper, we focus on the automated verification tools ProVerif and Tamarin, two prominent automated approaches dedicated to analyzing security protocols. Both use an unbounded number of sessions and the Dolev-Yao model [12]. The Dolev-Yao model is an abstract adversarial framework employed in the formal verification 2
2 Related Work
of security protocols, which simplifies analysis by assuming that cryptographic primitives are perfect while modeling an adversary with comprehensive control over all network communication channels. ProVerif operates by translating the models of security protocols into Horn clauses to analyze violations of the specified properties [1]. Conversely, Tamarin employs a state-based approach utilizing multiset rewriting rules [2]. The protocol is modeled as a set of rewrite rules that modify a global multiset of facts, which represents the system’s current state and event history. This approach enables stateful reasoning and the application of temporal logic (such as LTL) to specify and verify complex security properties Tamarin provides native support for complex algebraic properties such as Diffie-Hellman exponentiation [13], full support for mutual global state, and stateful reasoning with temporal logic, enabling verification of properties such as postcompromise security. However, these capabilities come at the cost of undecidable verification problems [14]. ProVerif, by contrast, offers more limited support for equational reasoning [15] and global state, but provides built-in biprocesses for modeling and verifying indistinguishability, and generally benefits from more automated and decidable verification. The remainder of the article is structured into six sections. Section 2 provides a critical review of existing classifications and literature pertaining to security property formalization and verification techniques. Section 3 describes the goal, research questions, and defines the search protocol employed to identify and select relevant primary studies from the literature. Subsequently, Section 4 answers the research questions by describing a taxonomy of security properties, a comprehensive quantitative analysis of the selected papers, and a description of the modeling patterns. Section 5 aims to validate the applicability of the taxonomy and modeling patterns. Section 6 offers an interpretation and critical analysis of these findings, discussing the advancements over prior work and addressing threats to validity. Finally, Section 7 summarizes the main contributions and addresses future work.
Although there is a common agreement on the definitions of security properties for security protocols, they are still open to interpretation since some of the formal definitions have not been widely agreed upon [9]. Focardi et al. [9] claim that a formal model is required to define the problem, and then the formal definition of the security property needs to be presented concerning the model. In this regard, they propose a classification of security properties by formulating it through a general scheme, Generalized Non Deducibility Composition (GNCD), to allow for an easier formal comparison of formal security properties. They use CryptoSPA [16] to specify security properties, but this does not allow for automated formal verification. Rouland et al. [17] specify security properties of a system using a technology-independent specification language: first-order logic. In the next phase, they specify the designed system using Alloy [18], a specific computational model of the system used for model checking and verification. The security properties specified are: confidentiality, integrity, and availability. On top of these security properties, Sayar et al. [10] also include authorization, authenticity, and accountability as being known as properties that a system should preserve. They propose a System Development Life Cycle (SDLC) taxonomy that allows experts to identify threats and propose defenses by synchronizing security properties with attacks, defenses, and system assets. Event-B [19] language was used to define the taxonomy, evaluate it, and update it as it evolves. Aldini [8] proposes a classification of security properties using process algebra based on Lindalike coordination primitives [20] (a shared, associative memory where data items can be added), where they used relaxed notions of behavioral equivalences that include the external observer’s abilities. The results highlight the positive influence of Linda coordination model on the expressivity. Hermann et al. [21] propose a taxonomy of functional implementation-level security features. This taxonomy is achieved by conducting a systematic literature review, then mapping the results to security standards and producing a relation to famous security frameworks. This aims
3
secrecy, authentication, unlinkability) are priorto help developers select appropriate security feaitized by researchers, and how often they appear tures to achieve certain standards. across case studies and domains. In contrast to prior taxonomies or classifications, which have either remained at a conceptual RQ2 How are security properties formally and informally defined? This question addresses the level [9, 10] or targeted functional security feadual nature of defining security properties: (i) tures [21], our work advances the state of the informal definitions, often presented in natuart in three ways. First, we systematically extract ral language to convey intuitive understanding, and categorize security properties verified with and (ii) formal definitions, expressed in logiProVerif and Tamarin over the past three years, cal formalisms (e.g., first-order logic) to support providing an up-to-date and evidence-based view. rigorous verification. The objective is to assess Second, we propose informal and formal definithe clarity, precision, and consistency of these tions, expressed in first-order logic, to ensure clardefinitions across studies. ity and consistency. Third, we make the taxonomy executable by mapping each property to represen- RQ3 What patterns and best practices can be identified for modeling and verifying common secutative models in both ProVerif and Tamarin, colrity properties of protocols using ProVerif and lected in an open repository. This combination of Tamarin? This question aims to uncover recurrigor, reproducibility, and practical applicability ring modeling structures, abstraction choices, distinguishes our work from earlier classifications. and verification strategies used across different studies that employ ProVerif and Tamarin for 3 Methodology protocol analysis. The focus is on identifying methodological patterns and tool-specific best This paper aims to provide a taxonomy of the curpractices that enhance the correctness, scalarent security properties verified using automated bility, and interpretability of security property verification tools such as ProVerif and Tamarin verification. over the past three years. To find relevant papers, we have defined a methodology in Section 3.1 based on established guidelines for systematic 3.2 Protocol literature reviews (SLRs) presented by KitchenWe define a protocol that includes the search ham et al. [22]. This facilitates the identification string, strategy, inclusion/exclusion criteria, and and analysis of resources used to address specific data extraction to enhance the reproducibility of research questions in a manner that is both reproour study. We performed a literature search on the ducible and unbiased. This section aims to present following digital libraries: ACM Digital Library, the research questions and the protocol used to IEEE Xplore, ScienceDirect, Scopus, and WebOfextract relevant studies from the literature. Science. The search string, comprising (”security” OR ”cryptographic”) AND ”protocol” AND ”ver3.1 Goal and Research Questions ification” AND (”tamarin” OR ”proverif”), was The primary objective of this study is to advance executed on the title, abstract, and keyword fields. the understanding of how security properties are Furthermore, we applied a filter on the years the modeled and verified in formal protocol analypapers were published, from January 2022 to April sis using ProVerif and Tamarin, two of the most 2025. By focusing on this period, this work aims widely adopted tools in the field. To achieve this, to provide a contemporary perspective on the we define the following research questions: security properties currently verified by protocol designers, also including properties from previRQ1 What security properties are verified using ous security property classification papers. This ProVerif and Tamarin? This question seeks to resulted in 454 papers (after removing duplicates). compile and categorize the most frequently verTable 1 defines a search protocol that includes ified security properties in protocol verification the search string, inclusion/exclusion criteria, and literature that utilizes ProVerif and Tamarin. the data extraction form. The inclusion/exclusion The goal is to understand which properties (e.g., criteria state that the selected papers must provide a ProVerif or Tamarin model, a description 4
of the security properties, and be published in the past three years. After applying the protocol, we selected a total of 53 papers that met the requirements. Next, data extraction is performed to extract the ProVerif or Tamarin models along with the definition of the security properties from the selected papers. The next step is to extract a relevant security protocol model for each security property in both ProVerif and Tamarin. The models are obtained by either extracting a specific model from previous studies, tools’ manuals, or by deriving it from the selected papers. These models aim to be used as a starting point for modeling protocols that aim to maintain these security properties.
4 Results This section presents the results of our study by addressing each research question. First, we provide an overview of the security properties identified in the literature by proposing a taxonomy. Second, we provide informal and formal definitions in first-order logic for each property. Finally, we describe some of the modeling patterns identified from the extracted models.
Fig. 1: Taxonomy of Security Properties
self-contained security requirement that cannot be decomposed into simpler ones, serving as a building block from which more complex security mechanisms can be constructed. Therefore, the scope of our taxonomy is primitive security properties. Figure 1 presents the taxonomy of security properties extracted from the selected papers. We define five main categories: authentication, integrity, confidentiality, privacy, and accountability. Each category represents a high-level security property that can be further extended to achieve a stricter security level. For instance, for confidentiality, ensuring key secrecy provides a certain level of confidentiality, but checking for forward secrecy ensures that if an attacker obtains a key, they cannot decrypt messages sent previously. To further investigate RQ1, a quantitative analysis was conducted to systematically examine the occurrence, distribution, and relationships of security properties. The analysis aims to enable an evidence-based understanding of how ProVerif and Tamarin are applied in practice. Data was extracted into a structured dataset, normalized for consistency, and analyzed. Figure 2 illustrates the distribution of the verified security properties by each group defined in our taxonomy. The most verified property is
4.1 RQ1 - What security properties are verified using ProVerif and Tamarin? The initial extraction of security properties from the selected papers yielded a total of 64 distinct terms. However, several of these overlapped semantically or represented the same concept expressed differently across studies. We performed a normalization process to ensure terminological consistency, grounding our classification in the functional goal of each property. By focusing on these functional outcomes, hierarchical or protocol-specific terms were consolidated under a common representative (see Table 2). For instance, conditional privacy-preserving and ticket privacy were both grouped under Privacy, and authenticity and message integrity were both unified under the Integrity group. Furthermore, we have identified protocol-specific properties (such as fairness, eligibility, or verification of intent) that, based on our analysis, are mechanisms that involve multiple properties already identified. We define a primitive security property as an atomic, 5
Table 1: Protocol overview Search string
(”security” OR ”cryptographic”) AND ”protocol” AND ”verification” AND (”tamarin” OR ”proverif”)
Search strategy
Database search: Scopus, IEEE Xplore, Web of Science, ACM Digital Library, SpringerLink. Forward and backward snowballing using Google Scholar.
Inclusion and exclusion criteria
Inclusion: Articles, conference papers, book chapters, and workshop papers. Studies where the title, abstract, or keywords suggest that their main topic of study is security protocol verification using ProVerif or Tamarin. Studies published between January 2022 and April 2025. Articles that are electronically accessible. Exclusion: Articles not in English. Studies such as slides, websites, or conference reviews. Articles that do not include a model. Articles that are not electronically accessible.
Data extraction
Title, year, security properties (formal/informal definitions), tool used (ProVerif or Tamarin), model
authentication (38 occurrences), but confidentiality (35), privacy (31), and integrity (23) are not far from it. This shows that the current verification tools provide the necessary means to verify these properties. Nevertheless, accountability (7 occurrences) is the least verified property from the selected papers. The reason behind this might be that to verify accountability, the users need to model more than the message flows, they need to model evidence generation and evaluation by a judge or a third party. Most protocol verification focuses on preventing attacks (such as ensuring confidentiality and integrity) rather than on proving responsibility after an incident. Additionally, many case studies that have been identified in the literature are based on well-known protocols (TLS, Signal), where accountability is not a primary design goal. The distribution of the sub-categories shows that core, broadly applicable security properties, such as integrity, forward secrecy, confidentiality, and anonymity dominate security protocol verification studies. This suggests that automated verification efforts predominantly focus on widely applicable and wellsupported properties, such as secrecy, privacy, and
authentication, while more specialized or complex properties remain underexplored. This might indicate that properties that require more effort to be modeled and verified are less likely to be verified. Table 3 maps each selected paper to the security properties defined by our taxonomy, where each property is grouped by its high-level category. Figure 4 presents the distribution of security properties per each taxonomy group by the verification tool used. This highlights the verification tool that is predominantly used to verify certain properties. Taking into consideration that only 26.9% of the selected papers use Tamarin (see Figure 3), the proportion for which both Tamarin and ProVerif are used for authentication, confidentiality, and integrity is broadly similar. However, for accountability and privacy, Tamarin tends to be used less compared to ProVerif. ProVerif’s higher automation, long-standing support for equivalence-based privacy, and extensive documentation explain why it is used more often in practice, while Tamarin is favored when one needs more expressive trace-based reasoning at the cost of higher modeling and proof effort. Thus, protocol designers have a lower learning barrier
6
Table 2: Normalization of extracted security properties into the final taxonomy Original Property (extracted from selected Mapped / Final Category papers) explicit key confirmation, strong secrecy Confidentiality – Secrecy perfect forward security Confidentiality – Forward secrecy data confidentiality Confidentiality anonymous, identity anonymity, user anonymity, Privacy – Anonymity identity protection, identity privacy conditional privacy-preserving, ticket privacy Privacy – Privacy indistinguishability, single-blindness, long-term Privacy – Unlinkability and untraceability unlinkable message integrity, authenticity Integrity – Integrity non-equivocation, unforgeability Integrity – Subproperties trace, traceable, traceability Accountability – Traceability non-repudiation Accountability – Non-repudiation transferable authentication, strong user authenti- Authentication – Authentication cation fairness, eligibility, verification of intent, cor- Protocol-specific (excluded) rectness, profile binding, receipt-freeness, nodouble-spending, vote verifiability, offline verifiable, remote attestation
4.2 RQ2 - How are security properties formally and informally defined?
when selecting ProVerif to model and verify their protocol. Both ProVerif and Tamarin are used to verify most of the security properties, although each tool may be more straightforward when it comes to modeling certain properties. Tamarin is used to verify post-compromise security properties, while ProVerif is used to check traceability. For instance, Tamarin is used for post-compromise security because it can explicitly model mutable state, temporal reasoning, and compromise events. In contrast, traceability, which belongs to the accountability class of properties, is often expressed as a reachability condition. This is more straightforwardly verified in ProVerif using its event-based correspondence queries. In general, the properties defined in our taxonomy can be verified by both Tamarin and ProVerif, but they may differ in the level of detail with which the protocols are modeled. Furthermore, the modeling approach might differ per tool since each tool offers different capabilities.
This section aims to present a taxonomy of primitive security properties that are verified using automated formal verification tools such as ProVerif and Tamarin. These properties have been identified from the literature, mostly based on the papers published in the past three years. Security has been studied for decades, evolving from early concerns over physical and communication security to the rigorous study of information security in the digital era. We define a taxonomy of security properties (see Section 4.1) for automated formal verification and in this section, we provide the formal definitions expressed in first-order logic. In first-order logic, predicate symbols are the building blocks used to express properties and relationships between entities. A predicate symbol takes one or more terms as arguments and evaluates to either true or false, essentially making a statement about those terms. For example, a predicate like Honest(A) asserts that agent A is honest, while a binary predicate like Knows(A, k) asserts that agent A knows key k. In the context of security protocol verification, predicates are used to capture protocol-specific concepts such as whether 7
Category Authentication
Authentication Authentication Authentication Authentication Confidentiality Confidentiality Confidentiality Integrity Integrity Integrity Accountability Accountability Privacy Privacy Privacy
Table 3: Mapping of selected papers to security properties verified Property Papers Authentication / Mutual Auth. [23], [24], [25], [26], [27], [28], [29], [30], [31], [32], [33], [34], [35], [36], [37], [38], [39], [40], [41], [42], [43], [44], [45], [46], [47] aliveness [48] weak agreement [48], [24] non-injective agreement [48], [24], [49], [50] injective agreement [48], [24], [49], [51], [52] [40], [24], [25], [43], [53], [28], [52], [54], [55], [29], [56], [34], [39], [57], [58], [27] forward secrecy [48], [47], [36], [37], [59], [46], [26], [42], [33], [57], [60], [38], [44], [61], [39], [45], [23] post-compromise security [45], [60] [40], [47], [62], [63], [33], [57], [64], [43], [53], [65], [58], [66], [55], [56], [67], [68], [34], [69], [70], [71], [39] unforgeability [72] non-equivocation [73] traceability [62], [43], [74], [41] non-repudiation [62], [28], [23] [62], [43], [28], [52], [56], [71], [50], [72] anonymity [62], [33], [35], [57], [43], [45], [54], [61], [71], [75], [72], [36], [37], [59], [46], [23] unlinkability [24], [43], [74], [28], [54], [61], [51]
Fig. 2: Frequency of Security Properties per Group
8
describe step by step the interaction between actors of the protocols. Next, we develop ProVerif and Tamarin models for each property based on the models presented in the selected papers (see Section 4.3).
4.2.1 Authentication The authentication definitions are based on the authentication levels defined by Lowe [76]: aliveness, weak agreement, non-injective agreement, and injective agreement. Particularly, for authentication, we consider two agents, A and B, taking the roles of initiator and responder, respectively. We aim to ensure that each agent can verify that it genuinely interacted with the other, that is, that the entity on the other end of the exchange is who it claims to be. The formalization of the authentication is based on Lowe’s definition and Tamarin’s manual [77], where they are described in first-order logic.
Fig. 3: Distribution of papers by verification tool.
Aliveness Informal Definition. This is the weakest form of authentication, which ensures that agent B has been running the protocol at some point in the past, but it does not guarantee that agent B interacted with agent A, or that the protocol has been running recently. Fig. 4: Frequency of properties verified per tool.
Formal Definition. • end(A, B, i) Agent A has completed a run of the protocol, apparently with agent B, at time (or trace step) i. • start(B, j ) Agent B has started (or participated in) a protocol session at time (or trace step) j.
a message was sent, whether a session key was established, or whether an adversary has learned a secret. This is aligned with the way properties are specified in ProVerif and Tamarin, where events (in the case of ProVerif) or actions (in the case of Tamarin) form a trace during the execution of the protocol. For our definitions, we first give an informal definition, then introduce the predicates, and finally, introduce the formal definition. The proposed definitions have been adapted from established formalizations in the literature to ensure consistency and to provide a robust foundational layer for modeling, enabling the practical verification of security properties through automated analysis tools. Furthermore, we provide examples on how to model and verify these security properties using both Tamarin and ProVerif. We first model the properties using sequence diagrams (as a tool-independent notation) that
∀A, B, i : end(A, B, i) =⇒ ∃j : start(B, j ) Weak Agreement Informal Definition. An initiator A has a weak agreement with another agent B, whenever A completes a run of the protocol, believing they interacted with B. Nevertheless, the fact that B was executing the protocol under the assumption of interacting with A does not necessarily imply that B assumed the role of responder. Formal Definition. • end(A, B, t, i) Agent A has completed a run of the protocol, apparently with agent B, with
9
• end(A, B, t, i) Agent A has completed a run of the protocol, apparently with agent B, with term t, at time (or trace step) i. • start(B, A, t, j ) Agent B has started (or participated in) a protocol session with agent A, with term t, at time j.
term t (data shared among the participants), at time (or trace step) i. • start(B, A, t, j ) Agent B has started (or participated in) a protocol session with agent A, with term t, at time j.
∀ A, B, t1 , i : end (A, B, t1 , i) =⇒ ∃ t2 , j : start (B, A, t2 , j )
∀ A, B, t, i : end (A, B, t, i) =⇒ ∃ j : start (B, A, t, j ) ∧ j < i ∧ ¬∃ A2 , B2 , i2 : end (A2 , B2 , t, i2 ) ∧ i2 ̸= i
Non-injective Agreement Informal Definition. An initiator A has a noninjective agreement with a responder B if A finishes the protocol believing they communicated with B, and B also has been running the protocol before, believing they were interacting with A, and both used the same data. However, A could run multiple instances of the protocol while B may not take part in all of them. Thus, it does not guarantee a one-to-one relationship.
4.2.2 Integrity The goals of integrity are defined by Biba [78] as data consistency is maintained both internally and externally, the data cannot be modified by unauthorized parties, where authorized refers to both cases where the party needs to be authorized to access a system, and it has the required levels of access to perform data modification. Furthermore, we include two more levels of integrity: unforgeability and non-equivocation.
Formal Definition. • end(A, B, t, i) Agent A has completed a run of the protocol, apparently with agent B, with term t, at time (or trace step) i. • start(B, A, t, j ) Agent B has started (or participated in) a protocol session with agent A, with term t, at time j.
Unforgeability Informal Definition. Unforgeability ensures that no adversary can produce a valid message or signature that was not generated by an honest participant, thus, an attacker cannot modify messages [34, 79]. Formal Definition.
∀ A, B, t, i : end (A, B, t, i) =⇒ ∃ j : start (B, A, t, j )
• validsig (A, m, sig ) The signature sig is valid for message m under agent A’s public key • signevent (A, m, sig, i) At time i, agent A actually signed message m, producing signature sig
Injective Agreement Informal Definition. This is the strongest level of authentication, where there is a non-injective agreement between initiator A and responder B with a strict one-to-one relationship. An initiator A has a non-injective agreement with a responder B if A finishes the protocol believing they communicated to B, and B also has been running the protocol before, believing they were interacting with A, and both used the same data. Additionally, every time agent A completes a run of the protocol, agent B has also been running the same instance of the protocol.
∀ A, m, sig : valid sig (A, m, sig ) =⇒ ∃ i : sign event (A, m, sig, i) Non-equivocation Informal Definition. Equivocation happens when an actor of the protocol sends different messages to different actors in the same instance of the protocol while the protocol instructs that the same message must be sent [80]. Therefore, non-equivocation is defined as assurance that an
Formal Definition.
10
• sessionKey (k, t) The session key k was generated or used in a protocol session at time t. • longT ermKey (ltk ) ltk is a long-term secret key, used for authentication or key agreement. • K (x) Value x is known by the attacker • leaked(k, t) Key k is leaked at time t
actor cannot use the same key to validate contradicting messages. Alternatively, non-equivocation is defined as the guarantee that a single message cannot be accepted more than once [73].
Formal Definition. • validsig (k, m) Message m is valid under public key k — i.e., m was signed with the private key corresponding to k, and the signature verification succeeded.
∀ ltk, k1 , t1 , t2 : sessionKey (k1 , t1 ) ∧ longTermKey (ltk ) ∧ leaked (ltk, t2 ) ∧ t1 < t2 =⇒ ¬K (k1 )
∀ k, m1 , m2 : valid sig (k, m1 ) ∧ valid sig (k, m2 ) =⇒ m1 = m2
Post-compromise Security (PCS) Informal Definition. Post-compromise security, also known as backward secrecy [84], is defined as the property of a protocol where actor A has a security guarantee about the communication with actor B, even if the attacker has B’s secrets [85]. It has the ability to recover after the compromise, so leaking the partner’s key does not imply that all future messages can be decrypted [60]. The recovery process is often a protocol-specific function, so it differs from protocol to protocol.
4.2.3 Confidentiality Confidentiality, also referred to as secrecy in practice, is achieved when a protocol ensures the secrecy of data M by never publishing M, or the means to compute M, even if there is an interaction with an attacker [81]. This also holds when the protocol is using public channels for communication. We include stronger versions of confidentiality, such as forward secrecy and postcompromise security. Confidentiality is one of the most verified security properties using ProVerif or Tamarin. ProVerif supports it as a primitive query to check this property, while Tamarin provides clear instructions in the manual [77]. Based on the lemma extracted from the Tamarin manual, we can express confidentiality as follows:
Formal Definition. Adapted from [60] • sent(sidA , A, B, sck, i) Agent A sends a message to B using session key sck during the session identified by sidA , at time i. • K (x, j ) Value x is known by the attacker at time j. • heal(sidA , A, B, k ) The session between A and B (session id sidA ) was healed at time k. • compromise(sidA , A, B, l) The session between A and B is compromised at time l.
• K (x) Value x is known by the attacker • secret(x) Value x is expected to remain confidential — i.e., not known to the adversary. ∀x : secret(x) =⇒ ¬K (x) Forward Secrecy Informal Definition. Forward secrecy property, also known as perfect forward secrecy [82], is a property of key exchange protocols that ensures past session keys remain secure even if longterm secret keys (used for authentication or key negotiation) are later compromised [83].
∀ A, B, sck, sidA , i, j, k : sent (sidA , A, B, sck, i) ∧ K (sck, j ) ∧ heal (sidA , A, B, k ) ∧k<i =⇒ ∃ l : compromise (sidA , A, B, l) ∧k<l
Formal Definition.
11
4.2.4 Privacy
4.2.5 Accountability
According to Westin [86], privacy is defined as ‘The claim of individuals, groups, or institutions to determine for themselves when, how and to what extent information about them is communicated to others’. We further include four subcategories of privacy in our taxonomy: anonymity and unlinkability.
Accountability is a property of a system or protocol that ensures that if a security goal is violated, the responsible parties can be identified [90]. The verification of this property usually requires a trusted third-party judge. Based on the definition introduced by Künnemann et al. [90]:
• Judged (t, c, i) – the judge received and accepted a response for certificate c carrying timestamp t, at time i • Secret (c, sk , j ) – the secret key sk is bound to certificate c, established at time j • K (sk , k ) – Value sk is known by the attacker at time k • Time (t, l) – the honest clock process emitted timestamp t at time l
Anonymity Informal Definition. Anonymity is defined as the confidentiality of the identification of agents of a protocol [87, 88]. Only authorized parties have access to relevant identification elements. Formal Definition. • actor(B, id) Agent B is a legitimate actor in the protocol with unique identifier id. • K (x) Value x is known by the attacker ∀B, id : actor(B, id) =⇒ ¬K (id)
¬∃ c, sk , t, i, j, k, l. Judged (t, c, i) ∧ Secret (c, sk , j ) ∧ K (sk , k ) ∧ Time (t, l) ∧k<l
Unlinkability Informal Definition. Unlinkability, also referred to as indistinguishability, represents the impossibility for an outside observer to distinguish two processes/systems [1, 89]. Furthermore, indistinguishability is one of the most important elements for ProVerif and Tamarin when it comes to the verification phase. If two processes are observationally equivalent, it means that no adversary, no matter how powerful, can tell which one they are interacting with. Thus, we present the following process notation, which describes that two processes are indistinguishable:
The intuition here is that if the secret sk becomes known to the attacker, the certification process must have happened before that. The formula is a negation of the opposite situation: secret sk is revealed before the time of the certification.
Traceability Informal Definition. Traceability is defined as the ability for a trusted entity to trace a message back to the sender to avoid malicious behaviors [43, 91].
Formal Definition. P (s)|P (s) ≈ P (s)|P (t)
Formal Definition. The notation expresses that two parallel compositions of process P are observationally equivalent, where on the left-hand side, both instances run with the same value s, while on the right-hand side, one instance runs with s and the other with a different value t. The equivalence relation states that no external observer can distinguish between these two configurations based on the observable outputs of the process.
• send(A, m) Agent A sends message m. • computeId(m) A function that returns the identity of the agent who actually sent message m. ∀A, m : send(A, m) =⇒ computeId(m) = A Non-repudiation Informal Definition. Non-repudiation property for protocols ensures that its agents are able to
12
provide evidence that another agent previously transmitted a message, which can be presented to a judge to prove its behavior [92].
Table 4 presents a comparison of security properties based on ProVerif and Tamarin in terms of conceptual maturity, tool support, modeling requirements, and verification difficulty. There are three levels of conceptual maturity (low, medium, and high) based on how well-defined and standardized the property is within the current literature. These are based on the patterns and definitions identified in the selected papers and the tools’ manuals. Furthermore, the tool support classification is extracted from the specific strengths and weaknesses of the two automated tools. Modeling requirements describe the specific coding structures or architectural elements a user must implement to verify the property. Verification difficulty estimates the computational costs and the likelihood of a tool to converge based on our hands-on experience. For the authentication property, we have chosen the Needham-Schroeder-Lowe Public Key protocol from the Tamarin example models [94]. This model has been modified to abstract away from traditional adversarial key-compromise scenarios to prioritize a formal deconstruction of the Lowe hierarchy of authentication. By omitting the longterm key-reveal rules, the model establishes a closed-world environment that isolates the protocol’s structural logic from the noise of forward secrecy analysis. This approach is motivated by the need to verify the incremental establishment of trust between actors, transitioning from basic aliveness to full injective agreement. Through the introduction of explicit state facts and lemmas for each authentication level, the model serves as a specialized investigative framework to demonstrate how we can verify the authentication levels using Tamarin. Although we provide ProVerif and Tamarin models along with sequence diagrams for each property from the taxonomy in our repository, we select two properties to present in detail in this section. We choose unlinkability and unforgeability, two properties that are not explicitly described in either ProVerif or Tamarin manuals. As defined in Section 4.2, unlinkability is defined as the indistinguishability of two processes/systems. This is a trivial property used for automated formal verification of security properties. In our case, we will limit the scope to the possibility of an attacker distinguishing between two processes of an actor of a protocol. Listing
Formal Definition. • obs(m) Message m is observed (an attacker or a participant of the protocol sees it on the network). • sent(m) Message m was sent by a legitimate process. ∀m : obs(m) =⇒ sent(m) These informal and formal definitions provide input for the verification queries used by both ProVerif and Tamarin. Besides giving a thorough understanding of how each security property is verified, this taxonomy explicitly identifies the specific events required for protocol instrumentation and the logical assertions necessary for tool-specific queries.
4.3 RQ3 - What patterns and best practices can be identified for modeling and verifying common security properties of protocols using ProVerif and Tamarin? To answer RQ3, we identify the best practices and patterns used to develop both ProVerif and Tamarin models for the security properties presented in our taxonomy. We analyzed the models proposed in the selected papers. Then, we proposed a model for each security property in both ProVerif and Tamarin. These are small models that capture the essential behavior of a property. In the case that some properties are not specifically modeled in the selected papers, or they were only modeled using one tool, we perform a search in the literature or check examples from ProVerif or Tamarin manuals. This allows us to extract/build example models for those security properties. This aims to help security protocol designers start the modeling and verification process for their protocol. We created a repository [93] with all the modeling patterns and security properties definitions extracted from the selected papers. Furthermore, our proposed models can be found in folders ProVerif Models and Tamarin Models in our repository.
13
Table 4: Comparative Synthesis of Security Properties Property
Conceptual Maturity
Tool Support (ProVerif vs. Tamarin)
Modeling Requirements
Verification Difficulty
Confidentiality
High Standard definitions (e.g., Secrecy, Forward Secrecy) are established.
ProVerif: Native primitive queries. Tamarin: Strong support via lemmas.
Reachability: Requires defining secret terms and checking adversary derivability.
Low to Medium Standard secrecy is efficient. PCS is difficult due to state explosion.
Authentication
High Based on Lowe’s hierarchy (Aliveness to Injective Agreement).
ProVerif: Excellent (Correspondence queries). Tamarin: Excellent (Logic formulas).
Correspondence: Requires annotating protocols with events (e.g., begin and end) to prove relationships.
Low Straightforward unless complex multi-party interactions are involved.
Integrity
High Based on Biba and standard signature validity.
Both: Supported via event matching (checking signatures/hashes).
Event Logic: Explicit modeling of signing and verification steps (e.g., signed by).
Medium Requires correct modeling of cryptographic primitives to prevent trivial violations.
Privacy
Medium Well-defined (Unlinkability) but complex implementation.
ProVerif: Uses biprocesses / choice. Tamarin: Uses Diff-equivalence.
Observational Equivalence: Modeling two distinct systems to prove they are indistinguishable to an attacker.
High Computationally heavy. Equivalence checks occur at every path, often causing nontermination.
Accountability
Low Least verified; lacks standardized patterns.
ProVerif: Good for Traceability. Tamarin: Better for Nonrepudiation.
Structural: Requires modeling Evidence generation and third-party verifiers, not just message flows.
Very High High manual modeling effort; difficult to abstract into simple queries.
1 presents the ProVerif model where we check if an attacker can observe the difference between two sessions that use different session IDs. We use the construct choice that allows for checking observational equivalence, such that an attacker cannot distinguish between two processes. Our model is just an example of how observational equivalence can be used to check unlinkability. This construct can also be used inside processes to check for the equivalence of output messages. However, if it is used inside a process, it will be computationally heavy as the check will take place at every path used for the verification, leading
to non-termination for the verification of midlevel complexity. For Tamarin, we have a similar construct (diff ) for verifying observational equivalence that was used in this case inside the Tamarin rule on line 26 in Listing 2. In this case, Tamarin seems to handle better than ProVerif the nontermination problem for observational equivalence as the verification converges (when used in the equivalent of the ProVerif process). We do not provide a sequence diagram for this model because it has one process/actor that sends only one message
14
on the public channel, so there is no interaction between multiple parties. Nevertheless, the attacker can initiate a message exchange.
functions for the signing and verification process of the signature. We use these functions to model the protocol described by the sequence diagram and introduce some events to allow us to verify the correctness of the protocol. The ProVerif model triggers a signedBy event with the secret key and the message after the Signer signs the message, then it creates an event after the verification of the signature with the message and the public key of the signer as parameters. These two events enable us to define a query verifying that for each valid signature with a public key, there has been created a signature with corresponding secret key for that message. Conversely, Listing 4 presents the Tamarin model of the same protocol, where we defined a lemma for the unforgeability check based on the formal definition from our taxonomy. The lemma states that for each valid signature, there is an event where an honest participant signed the message. In a similar manner, we have introduced SignedBy and ValidSignature events to allow us to apply the unforgeability lemma.
free c : channel . type uid . type nonce . 3 fun pid ( uid , nonce ) : bitstring . 1 2 4 5
free U , V : uid [ private ].
6
let session ( u : uid ) = new r : nonce ; 9 (* out (c , u ) . *) 10 out (c , pid (u , r ) ) . 7 8
11
(* B i p r o c e s s : left = both s e s s i o n s use U ; right = second uses V *) 13 process 14 ( session ( U ) | session ( choice [U , V ]) ) 12
Listing 1: Unlinkability Check in ProVerif 1
// tamarin - prover -- diff -- prove U n l i n k a b i l i t y . spthy
2 3 4
theory Identit y Pr iv ac y begin
5 6
builtins : hashing
7
/* 1. Setup : G e n e r a t e the private i d e n t i t i e s */ rule Setup : 10 [ Fr (~ U ) , Fr (~ V ) ] 11 - -[ OnlyOnce () ] - > 12 [ ! ID_U (~ U ) , ! ID_V (~ V ) ]
1
13
4
8 9
free c : channel .
2
14
type skey . type pkey . 5 type boolean .
15
6
/* 2. Session One : Always uses I d e n t i t y U */ rule Session_One : 16 [ ! ID_U (~ U ) , Fr (~ r1 ) ] 17 --> 18 [ Out ( h ( <~U , ~ r1 >) ) ] 19
/* 3. Session Two : The ’ Choice ’ rule Uses diff (U , V ) to check for o b s e r v a t i o n a l equivalence . 22 */ 23 rule Session_Two : 24 [ ! ID_U (~ U ) , ! ID_V (~ V ) , Fr (~ r2 ) ] 25 --> 26 [ Out ( h ( < diff (~ U , ~ V ) , ~ r2 >) ) ]
3
fun pk ( skey ) : pkey . fun sign ( bitstring , skey ) : bitstring . 9 reduc forall m : bitstring , sk : skey ; checksign ( sign (m , sk ) , pk ( sk ) ) = m . 7 8
20
10
21
11
27
event signed_by ( skey , bitstring ) . event va li d _s ig n at ur e ( bitstring , pkey ) . 13 event check () . 12 14
query m : bitstring , sk : skey ; event ( v al id _s i gn at ur e (m , pk ( sk ) ) ) == > event ( signed_by ( sk , m ) ) . 16 query event ( check () ) . 15
28
/* --- R e s t r i c t i o n s --- */ restriction OnlyOnce : 30 " All # i # j . OnlyOnce () @ i & OnlyOnce () @ j == > # i = # j "
17
29
18
31
21
32
end
Listing 2: Unlinkability Check in Tamarin Unforgeability property ensures that no adversary can produce a valid message or signature that was not generated by an honest participant (see Section 4.2). Figure 5 shows a sequence diagram of a simple protocol that achieves unforgeability [72]. In this protocol, a Signer signs a message using its secret key, sends the signed message to the Verifier. Then, Verifier verifies the signature with the public key of Signer. Listing 3 presents the ProVerif model of this protocol, where we define
free skA : skey [ private ].
19
let processA () = new m1 : bitstring ; 22 let s1 = sign ( m1 , skA ) in 23 event signed_by ( skA , m1 ) ; 24 out (c , m1 ) ; 25 out (c , s1 ) . 20
26
let processB ( pkA : pkey ) = new m2 : bitstring ; 29 in (c , si gned_me ssage : bitstring ) ; 30 let m = checksign ( signed_message , pkA ) in 27 28
31 32 33 34
event va l id _s ig n at ur e (m , pkA ) ; event check () ; 0.
35
process let pkA = pk ( skA ) in 38 out (c , pkA ) ; 36 37
15
39
(! processA () | ! processB ( pkA ) )
Listing 3: Unforgeability Check in ProVerif 1 2
theory Simpl eS i gn at ur e begin
3 4
builtins : signing
5
/* 1. Setup : G e n e r a t e keys and publish the public key */ 7 rule Setup : 8 [ Fr (~ skA ) ] 9 - -[ OnlyOnce () ] - > 10 [ ! LtkA (~ skA ) , ! PkA ( pk (~ skA ) ) , Out ( pk (~ skA ) ) ] 6
11
/* 2. Process A : Sign a fresh message */ rule ProcessA : 14 [ ! LtkA (~ skA ) , Fr (~ m1 ) ] 15 - -[ SignedBy (~ skA , ~ m1 ) ] - > 16 [ Out ( <~ m1 , sign (~ m1 , ~ skA ) >) ] 12 13
17
/* 3. Process B : Receive message and signature , then verify */ 19 rule ProcessB : 20 [ In ( <m , sig >) 21 , ! PkA ( pkA ) 22 ] 23 - -[ Eq ( verify ( sig , m , pkA ) , true ) 24 , ValidSig nature (m , pkA ) 25 , Check () 26 ]-> 27 [ ] 18
Fig. 5: Example Protocol for Unforgeability Property
5 Case Study To validate the applicability of the taxonomy and modeling patterns to cryptographic primitives that combine multiple security goals, we analyze the Signcryption scheme proposed by Zheng [95]. Signcryption is a cryptographic primitive that performs signature and encryption in a single logical step. This is often regarded as secure message transmission. However, using our taxonomy, we decompose it into two security properties that require distinct verification strategies. One property is secrecy, which is a well-established property within the automated verification domain. In this case, the message m must remain secret from the attacker. The other property is unforgeability, which is part of the integrity in our taxonomy. This ensures that a message originates from the claimed sender. In the case of ProVerif, this is verified by using event correspondence. We developed two models to demonstrate the necessity of the taxonomy’s modeling patterns (see Example folder in our repository). The initial models implement only the algebraic logic of the protocol. They define the key derivation functions (kdf1, kdf2 ) and the core algebraic reduction where the Receiver’s calculation matches the Sender’s (for the signcryption). This model includes a success event as a sanity check to
28 29
/* --- R e s t r i c t i o n s --- */
30 31 32
restriction Equality : " All x y # i . Eq (x , y ) @ i == > x = y "
33 34 35
restriction OnlyOnce : " All # i # j . OnlyOnce () @ i & OnlyOnce () @ j == > # i = # j "
36 37
/* --- Lemmas --- */
38
lemma Unforgeabi lity : all - traces 41 " All m pkA # i . Val idSigna ture (m , pkA ) @ i == > 42 ( Ex sk # j . SignedBy ( sk , m ) @ j & pk ( sk ) = pkA ) " 39 40
43
lemma Executability : exists - trace 46 " Ex # i . Check () @ i " 44 45 47 48
end
Listing 4: Unforgeability Check in Tamarin Together, the sequence diagrams, ProVerif models, and Tamarin models collected in the accompanying repository create a reusable catalogue of modeling patterns that serves as a blueprint for specifying and verifying security properties. The applicability of this catalogue to concrete security protocols is demonstrated in Section 5.
16
even for schemes involving more complex algebraic reductions compared with the initial signing function provided in the pattern.
ensure that the two actors can communicate. Nevertheless, this reachability check does not prove security, it only proves that the protocol can reach the end. To verify unforgeability and secrecy (as claimed by the signcryption protocol), we applied the pattern for unforgeability and secrecy from our repository to the initial model. Based on this example, we extract the query and the events used and identify where the events are triggered (as presented in Listing 3, lines 23 and 32). In this case, the events are triggered before the signed message is sent and after the signed message is verified. Listing 5 presents the events and queries extracted from the unforgeability pattern and introduced in the signcryption protocol to verify the secrecy of the message and the unforgeability of the signature. The results of the verification indicate that the signcryption protocol ensures secrecy of the message and unforgeability of the signature as claimed by the protocol definition.
6 Discussion The results reveal that confidentiality, authentication, and privacy are the most frequently verified properties, reflecting the maturity of tool support for these primitives. In contrast, accountability properties are rarely modeled, suggesting either an open research gap in automating their verification or that current security protocols do not prioritize this. Unlike prior conceptual classifications [9, 10, 17, 21], our taxonomy is based on empirical evidence from recent verification studies and bridges the gap between theoretical definitions and executable models. Although these classifications provide rigorous formalization, we focus on improving understandability and practical applicability. We achieve this by deriving our taxonomy from current verification trends and building a catalog to demonstrate how these properties can be used in practice. We provide definitions of the security properties and propose small protocols to showcase ProVerif and Tamarin models to verify all security properties. We first give a conceptual understanding of the properties, then we present concrete examples for each property by creating code examples. These code examples aim to help users encode the verification of these security properties in their protocols [96]. For example, in Section 4.3 we introduce an example for unforgeability. Given that the user already has a protocol encoded in ProVerif (without verification queries), the user can employ the queries that we defined for unforgeability into their model.
(* --- 4. Events and Queries --- *) event signed_by ( skey , bitstring ) . 3 event valid_sig n at ur e ( bitstring , pkey ) . (* Message m a c c e p t e d as coming from pkey *) 1 2
4
(* Sanity check *) event success () . 7 query event ( success () ) . 5 6 8 9 10
(* C o n f i d e n t i a l i t y : Can the a t t a c k e r get m_0 ? *) query attacker ( m_0 ) .
11 12 13
(* U n f o r g e a b i l i t y *) query m : bitstring , sk : skey ; event ( valid_sign at ur e (m , pk ( sk ) ) ) == > event ( signed_by ( sk , m ) ) .
Listing 5: Unforgeability ProVerif Events and Queries In this case study, we followed the modeling pattern for unforgeability provided in the companion repository. The applicability of this pattern has been demonstrated on a security protocol by introducing the verification steps to both ProVerif and Tamarin models of the protocol. Even though the unforgeability definitions are available already, missing modeling patterns for the verification significantly increase the difficulty of modeling and verifying such security protocols. Therefore, this case study confirms that the taxonomy, along with the modeling patterns, provides a necessary bridge between abstract cryptographic definitions and concrete ProVerif and Tamarin implementations,
6.1 Threats to Validity This section addresses threats to internal, external, and construct validity, as statistical conclusion validity is not applicable given the qualitative nature of our study. To mitigate the threats to validity, we employed a systematic approach where we defined a protocol that specifies the search string, inclusion/exclusion criteria, and data extraction form. Because the inclusion and
17
exclusion criteria were clearly defined and objective, selection bias was minimized. Some subjectivity may have been introduced when determining whether a study included a description of security properties and corresponding ProVerif or Tamarin models. However, this assessment was largely straightforward, as the presence or absence of these elements was usually explicit in the papers. Largely, because for any security protocol study, they include a description of the properties they aim for. This study focuses only on security properties verified using ProVerif or Tamarin, thereby excluding works employing other tools such as Scyther or AVISPA. Nevertheless, when defining and formalizing security properties for our taxonomy, we did not limit ourselves to the selected papers, but took into consideration various relevant studies from the literature that propose widely accepted definitions and formalizations. During normalization, terminology across papers (e.g., identity protection, strong user authentication) required manual consolidation, which may have introduced interpretation bias. Thus, subjective grouping decisions could have influenced the taxonomy’s structure. Since our paper only covers the studies published from 2022 to 2025, earlier works that introduced foundational security properties or alternative modeling approaches might be missed. However, this limitation was mitigated by performing targeted searches for each identified security property to extract relevant definitions and formalizations from relevant sources.
Accountability properties, which requires modeling complex concepts like evidence generation and judgment rather than simple message flows. Crucially, we provided unified informal and formal definitions (in first-order logic) for each property in the taxonomy and detailed executable modeling patterns and best practices for both tools. This combination of rigor and practicality distinguishes our work from earlier conceptual or functional classifications. The provision of an open repository containing these formal models addresses the difficulty faced by protocol designers, offering a concrete and repeatable starting point for their verification efforts. The immediate outcome of this study is the definitive foundation required for the development of our planned Domain-Specific Language (DSL). Future work will focus on: 1. DSL Development: Creating the DSL to automatically translate high-level protocol descriptions and security properties into executable models for both ProVerif and Tamarin, thereby abstracting the complexity of formal verification. 2. Taxonomy Expansion: Expanding the taxonomy to include higher-level security mechanisms, such as key exchange and multifactor authentication, that are composed of the primitive properties identified in this study.
Declarations This research has been funded by the European Union’s research and innovation programme ENTRUST, under grant agreement No. 101095634.
7 Conclusion This study establishes an evidence-based taxonomy of security properties crucial for the formal verification of security protocols using automated tools, specifically ProVerif and Tamarin. By systematically analyzing recent literature, we categorized verified properties into five core groups: Authentication, Confidentiality, Integrity, Privacy, and Accountability. The quantitative analysis provided empirical insight into current verification trends, confirming that core properties such as Confidentiality and Privacy dominate academic attention. A notable finding is the pronounced research gap in formal verification techniques for
References [1] Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: Proverif 2.00: automatic cryptographic protocol verifier, user manual and tutorial. Version from 16, 05–16 (2018) [2] Meier, S., Schmidt, B., Cremers, C., Basin, D.: The tamarin prover for the symbolic analysis of security protocols. In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 1319, 2013. Proceedings 25, pp. 696–701 (2013).
18
[9] Focardi, R., Gorrieri, R., Martinelli, F.: In: Focardi, R., Gorrieri, R. (eds.) Classification of Security Properties: (Part II: Network Security). Lecture Notes in Computer Science, vol. 2946, pp. 139–185. Springer, Berlin, Heidelberg (2004). h t 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 - 2 4 . http://link.springer.com/10.1007/978-3-54024631-2 4
Springer [3] Cremers, C.J.: The scyther tool: Verification, falsification, and analysis of security protocols: Tool paper. In: International Conference on Computer Aided Verification, pp. 414–418 (2008). Springer [4] Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The avispa tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, pp. 281–285. Springer, Berlin, Heidelberg (2005)
[10] 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] [11] Nickerson, R.C., Varshney, U., Muntermann, J.: A method for taxonomy development and its application in information systems. European Journal of Information Systems 22(3), 336–359 (2013) https://doi.org/10.1057/ejis .2012.26
[5] Kobeissi, N., Nicolas, G., Tiwari, M.: Verifpal: Cryptographic protocol analysis for the real world. In: Bhargavan, K., Oswald, E., Prabhakaran, M. (eds.) Progress in Cryptology – INDOCRYPT 2020, pp. 151–202. Springer, Cham (2020)
[12] Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983) http s://doi.org/10.1109/TIT.1983.1056650 . Conference Name: IEEE Transactions on Information Theory. Accessed 2024-06-10
[6] Tudorache, L.: Towards secure iot deployments: A dsl and digital twin-based emulation platform for security verification. In: 2025 ACM/IEEE 28th International Conference on Model Driven Engineering Languages and Systems Companion, MODELS-C 2025, pp. 71–76. Institute of Electrical and Electronics Engineers, United States (2025). http s://doi.org/10.1109/MODELS-C68889.2025 .00017 . 28th ACM/ IEEE International Conference on Model Driven Engineering Languages and Systems Companion, MODELSC 2025, MODELS-C 2025 ; Conference date: 05-10-2025 Through 10-10-2025
[13] Diffie, W., Hellman, M.E.: New directions in cryptography. In: Democratizing Cryptography: the Work of Whitfield Diffie and Martin Hellman, pp. 365–390 (2022) [14] 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
[7] 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
[15] 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– 423. ACM, Dallas Texas USA (2017). https://doi.org/10.1145/3133956.3133998 . https://dl.acm.org/doi/10.1145/3133956.3133998
[8] Aldini, A.: Classification of security properties in a linda-like process algebra. Science of Computer Programming 63(1), 16–38 (2006) https://doi.org/10.1016/j.scico.2005.07.010 19
[23] Jacomme, C., Klein, E., Kremer, S., Racouchot, M.: A comprehensive, formal and automated analysis of the edhoc protocol, vol. 8, pp. 5881–5898 (2023)
[16] Focardi, R., Martinelli, F.: A uniform approach for the definition of security properties. 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)
[24] 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 communication. IEEE Transactions on Dependable and Secure Computing, 1–15 (2024) ht tps://doi.org/10.1109/TDSC.2024.3522895
[17] 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). ht t p s : //doi.org/10.1109/ICECCS.2019.00033 . https://ieeexplore.ieee.org/document/8882749/
[25] Wang, B., Li, H., Guan, J.: A formal analysis of data distribution service security. ASIA CCS ’24, pp. 716–727. Association for Computing Machinery, New York, NY, USA (2024). h t t p s : / / d o i . org/10.1145/3634737.3656288 . https://doi.org/10.1145/3634737.3656288 [26] Chunka, C., Banerjee, S., Sachin Kumar, G.: A secure communication using multifactor authentication and key agreement techniques in internet of medical things for covid19 patients. Concurrency and Computation: Practice and Experience 35(7) (2023) https: //doi.org/10.1002/cpe.7602
[18] Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, USA (2012) [19] Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, USA (2010)
[27] Méré, 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. Software and Systems Modeling (2024) https: //doi.org/10.1007/s10270-024-01201-0
[20] Gelernter, D.: Generative communication in linda. ACM Trans. Program. Lang. Syst. 7(1), 80–112 (1985) https://doi.org/10.1145/ 2363.2433 [21] Hermann, K., Schneider, S., Tony, C., Yardim, A., Peldszus, S., Berger, T., Scandariato, R., Sasse, M.A., Naiakshina, A.: A taxonomy of functional security features and how they can be located. Empirical Software Engineering 30(5), 117 (2025) https://doi. org/10.1007/s10664-025-10649-7 . Accessed 2025-08-14
[28] Feng, H., Guan, J., Li, H., Pan, X., Zhao, Z.: Fido gets verified: A formal analysis of the universal authentication framework protocol. IEEE Transactions on Dependable and Secure Computing 20(5), 4291–4310 (2023) https://doi.org/10.1109/TDSC.2022.321725 9
[22] Kitchenham, B., Pearl Brereton, O., Budgen, D., Turner, M., Bailey, J., Linkman, S.: Systematic literature reviews in software engineering – a systematic literature review. Information and Software Technology 51(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
[29] Bussa, S., Sisto, R., Valenza, F.: Formal verification of the fdo protocol. In: 2023 IEEE Conference on Standards for Communications and Networking (CSCN), pp. 290–295 (2023). https://doi.org/10.1109/CSCN 60443.2023.10453172 . journalAbbreviation: 2023 IEEE Conference on Standards for Communications and Networking (CSCN)
20
Applied Sciences (Switzerland) 13(7) (2023) https://doi.org/10.3390/app13074425
[30] Moustafa, M., Sethi, M., Aura, T.: Misbinding 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
[38] You, I., Kim, J., Pawana, I.W.A.J., Ko, Y.: Mitigating security vulnerabilities in 6g networks: A comprehensive analysis of the dmrn protocol using svo logic and proverif. Applied Sciences (Switzerland) 14(21) (2024) https: //doi.org/10.3390/app14219726
[31] De Vaere, P., Stoger, F., Perrig, A., Tsudik, G.: The sa4p framework: Sensing and actuation as a privilege. ASIA CCS ’24, pp. 873–885. Association for Computing Machinery, New York, NY, USA (2024). ht t p s : //doi.org/10.1145/3634737.3657006 . https://doi.org/10.1145/3634737.3657006
[39] Ko, Y., Pawana, I.W.A.J., Won, T., Astillo, P.V., You, I.: Toward an era of secure 5g convergence applications: Formal security verification of 3gpp akma with tls 1.3 psk option. Applied Sciences (Switzerland) 14(23) (2024) https://doi.org/10.3390/app142311152
[32] Pradhan, M., Mohanty, S.: A blockchainassisted multifactor authentication protocol for enhancing iomt security. IEEE Internet of Things Journal 11(24), 39323–39332 (2024) https://doi.org/10.1109/JIOT.2024.3422242
[40] 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
[33] Huang, Y., Xu, G., Song, X., Xu, Y.: An efficient rlwe-based privacy-preserving authentication scheme based on edge computing in industrial internet of things. IEEE Transactions on Services Computing 17(5), 2012– 2026 (2024) https://doi.org/10.1109/TSC.20 24.3433534
[41] Duttagupta, S., Marin, E., Singelee, D., Preneel, B.: Hat: Secure and practical key establishment for implantable medical devices. CODASPY ’23, pp. 213–224. Association for Computing Machinery, New York, NY, USA (2023). h t t p s : / / d o i . org/10.1145/3577923.3583646 . https://doi.org/10.1145/3577923.3583646
[34] 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 [35] Saini, K.K., Kaur, D., Kumar, D., Kumar, B.: An efficient three-factor authentication protocol for wireless healthcare sensor networks. Multimedia Tools and Applications 83(23), 63699–63721 (2024) https://doi.org/10.100 7/s11042-024-18114-1
[42] 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 Sciences 134(1), 317–341 (2022) https://doi.org/10.32604/cmes.2022.0 19595
[36] 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 Communications 220, 81–93 (2024) https://doi.org/10.1 016/j.comcom.2024.04.011
[43] 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 Architecture 138 (2023) https: //doi.org/10.1016/j.sysarc.2023.102869
[37] 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.
[44] Zarbi, N., Zaeembashi, A., Bagheri, N., Adeli, M.: Toward designing a lightweight rfid authentication protocol for constrained environments. IET Communications 18(14), 21
846–859 (2024) https://doi.org/10.1049/cm u2.12794
(2024). https://doi.org/10.1007/978-3-031-5 3555-0 14
[45] 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
[53] Feng, Y., Wang, Z., Bobda, C.: Civicfpga: A trusted fpga design validation by multi-tenant cloud providers. FPGA ’25, pp. 139–145. Association for Computing Machinery, ??? (2025). h t t p s : / / d o i.org/10.1145/3706628.3708826 . https://doi.org/10.1145/3706628.3708826
[46] Li, Y.: A secure and efficient three-factor authentication protocol for iot environments. Journal of Parallel and Distributed Computing 179, 104714 (2023) https://doi.org/10.1 016/j.jpdc.2023.104714
[54] Bussa, S., Sisto, R., Valenza, F.: Formal verification 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 International Conference on Cyber Security and Resilience (CSR)
[47] Miculan, M., Vitacolonna, N.: Automated verification of telegram’s mtproto 2.0 in the symbolic model. Computers & Security 126, 103072 (2023) https://doi.org/10.1016/j.cose .2022.103072 [48] Akman, G., Ginzboorg, P., Damir, M.T., Niemi, V.: Privacy-enhanced akma for multiaccess edge computing mobility †. Computers 12(1) (2023) https://doi.org/10.3390/comp uters12010002
[55] Watanabe, K., Yoneyama, K.: Formal verification 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 [56] Fujita, K., Yoneyama, K.: Formal verification 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
[49] 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
[57] Wang, S., Wu, Y., Wen, K., Zhou, X., Hu, B., Xie, Q.: An improved blockchainbased lightweight vehicle-to-infrastructure handover authentication protocol for vehicular ad hoc networks. Mathematics 13(7) (2025) https://doi.org/10.3390/math130711 18
[50] Wang, Y., Laing, T., Moreira, J., Ryan, M.D.: Remote registration of multiple authenticators. CODASPY ’24, pp. 379–390. Association for Computing Machinery, New York, NY, USA (2024). h t t p s : / / d o i . org/10.1145/3626232.3653273 . https://doi.org/10.1145/3626232.3653273
[58] 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
[51] Bursuc, S., Horne, R., Mauw, S., Yurkov, S.: Provably unlinkable smart card-based payments. CCS ’23, pp. 1392–1406. Association for Computing Machinery, New York, NY, USA (2023). h t t p s : / / d o i . org/10.1145/3576915.3623109 . https://doi.org/10.1145/3576915.3623109
[59] 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
[52] Zhu, N., Xu, J., Cui, B.: Formal Analysis of 5G EAP-TLS 1.3, vol. 193, pp. 140–151
22
Z.M.: Gatekeeper: A gateway-based broadcast authentication protocol for the invehicle ethernet. ASIA CCS ’22, pp. 494– 507. Association for Computing Machinery, New York, NY, USA (2022). h t t p s : / / doi.org/10.1145/3488932.3517396 . https://doi.org/10.1145/3488932.3517396
[60] Cremers, C., Jacomme, C., Naska, A.: Formal analysis of session-handling in secure messaging: Lifting security from sessions to conversations, vol. 2, pp. 1235–1252 (2023) [61] 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 Engineering 2023 (2023) https://doi.org/10.115 5/2023/4845850
[68] 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
[62] Shahrouz, J.K., Analoui, M.: An anonymous authentication scheme with conditional privacy-preserving for vehicular ad hoc networks based on zero-knowledge proof and blockchain. Ad Hoc Networks 154, 103349 (2024) https://doi.org/10.1016/j.adhoc.2023 .103349
[69] 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)
[63] Raimondo, M., Bernardi, S., Marrone, S., Merseguer, J.: An approach for the automatic verification of blockchain protocols: the tweetchain case study. Journal of Computer Virology and Hacking Techniques 19(1), 17– 32 (2023) https://doi.org/10.1007/s11416-0 22-00444-z
[70] Fila, B., Radomirović, S.: Nothing is outof-band: Formal modeling of ceremonies. In: 2024 IEEE 37th Computer Security Foundations Symposium (CSF), pp. 464–478 (2024). https://doi.org/10.1109/CSF61375.2024.00 049 . journalAbbreviation: 2024 IEEE 37th Computer Security Foundations Symposium (CSF)
[64] Sabry, M., Samavi, R.: Archivesafe lt: Secure long-term archiving system. ACSAC ’22, pp. 936–948. Association for Computing Machinery, ??? (2022). h t t p s : / / d o i.org/10.1145/3564625.3564635 . https://doi.org/10.1145/3564625.3564635
[71] 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 Systems 10(3), 1039–1056 (2023) https://doi.or g/10.1109/TCSS.2022.3162869
[65] Wagner, P.G., Birnstill, P., Beyerer, J.: Dds security+: Enhancing the data distribution service with tpm-based remote attestation. ARES ’24. Association for Computing Machinery, ??? (2024). h t t p s : / / doi.org/10.1145/3664476.3670442 . https://doi.org/10.1145/3664476.3670442
[72] 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
[66] Baloglu, S., Bursuc, S., Mauw, S., Pang, J.: Formal verification and solutions for estonian e-voting. ASIA CCS ’24, pp. 728–741. Association for Computing Machinery, ??? (2024). https://doi.org/10.1145/3634737.3657009 . https://doi.org/10.1145/3634737.3657009
[73] Giantsidi, D., Pritzi, J., Gust, F., Katsarakis, A., Koshiba, A., Bhatotia, P.: Tnic: A trusted
[67] Hu, S., Zhang, Q., Weimerskirch, A., Mao,
23
nic architecture: A hardware-network substrate for building high-performance trustworthy distributed systems. ASPLOS ’25, pp. 1282–1301. Association for Computing Machinery, ??? (2025). h t t p s : / / d o i.org/10.1145/3676641.3716277 . https://doi.org/10.1145/3676641.3716277
[81] Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs [82] Krawczyk, H.: In: Jajodia, S., Samarati, P., Yung, M. (eds.) Perfect Forward Secrecy, pp. 1–3. Springer, Berlin, Heidelberg (2019). http s://doi.org/10.1007/978-3-642-27739-9 90-2
[74] 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
[83] Krawczyk, H.: In: Jajodia, S., Samarati, P., Yung, M. (eds.) Perfect Forward Secrecy, pp. 1–3. Springer, Berlin, Heidelberg (2021). http s://doi.org/10.1007/978-3-642-27739-9 90-2 [84] Cremers, C., Fairoze, J., Kiesl, B., Naska, A.: Clone detection in secure messaging: Improving post-compromise security in practice. In: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. CCS ’20, pp. 1481– 1495. Association for Computing Machinery, New York, NY, USA (2020). ht t p s : //doi.org/10.1145/3372297.3423354 . https://doi.org/10.1145/3372297.3423354
[75] 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 [76] Lowe, G.: A hierarchy of authentication specifications. In: Proceedings 10th Computer Security Foundations Workshop, pp. 31–43. IEEE Comput. Soc. Press, Rockport, 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/
[85] Cremers, C., Jacomme, C., Naska, A.: Cispa helmholtz center for information security [86] Westin, A.F.: Privacy and Freedom. Ig Publishing, Brooklyn, NY (2015). With a new introduction by Daniel J. Solove
[77] The Tamarin Team: Tamarin Prover Manual: Security Protocol Analysis in the Symbolic Model. (2024). https://tamarin-prover.com/ manual/master/tex/tamarin-manual.pdf
[87] Schneider, S., Sidiropoulos, A.: In: Bertino, E., Kurth, H., Martella, G., Montolivo, E. (eds.) CSP and anonymity. Lecture Notes in Computer Science, vol. 1146, pp. 198–218. Springer, Berlin, Heidelberg (1996). https: //doi.org/10.1007/3-540-61770-1 38
[78] Biba, K.J.: Integrity considerations for secure computer systems (522) (1977) [79] Katz, J., Yung, M.: Unforgeable encryption and chosen ciphertext secure modes of operation. In: Goos, G., Hartmanis, J., Leeuwen, J., Schneier, B. (eds.) Fast Software Encryption, pp. 284–299. Springer, Berlin, Heidelberg (2001)
[88] Samfat, D., Molva, R., Asokan, N.: Untraceability in mobile networks. In: Proceedings of the 1st Annual International Conference on Mobile Computing and Networking - MobiCom ’95, pp. 26–36. ACM Press, Berkeley, California, United States (1995). https://doi.org/10.1145/215530.215548 . http://portal.acm.org/citation.cfm?doid=215530.215548
[80] Clement, A., Junqueira, F., Kate, A., Rodrigues, R.: On the (limited) power of non-equivocation. In: Proceedings of the 2012 ACM Symposium on Principles of Distributed Computing, pp. 301–308. ACM, Madeira Portugal (2012). [89] Baelde, D., Delaune, S., Moreau, S.: A https://doi.org/10.1145/2332432.2332490 . method for proving unlinkability of stateful https://dl.acm.org/doi/10.1145/2332432.2332490 protocols, vol. 2020-June, pp. 169–183 (2020).
24
https://doi.org/10.1145/1062455.1062491
https://doi.org/10.1109/CSF49147.2020.00 020 [90] Künnemann, R., Esiyok, I., Backes, M.: Automated verification of accountability in security protocols. In: 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), pp. 397–39716 (2019). https://doi.org/10.1109/ CSF.2019.00034 [91] Fu, A., Qin, N., Wang, Y., Li, Q., Zhang, G.: Nframe: A privacy-preserving with nonframeability handover authentication protocol based on (t, n) secret sharing for lte/lte-a networks. Wireless Networks 23(7), 2165– 2176 (2017) https://doi.org/10.1007/s11276 -016-1277-0 [92] Schneider, S.: Formal analysis of a nonrepudiation protocol. In: Proceedings. 11th IEEE Computer Security Foundations Workshop (Cat. No.98TB100238), pp. 54–65. IEEE Comput. Soc, Rockport, MA, USA (1998). h t t p s : //doi.org/10.1109/CSFW.1998.683155 . http://ieeexplore.ieee.org/document/683155/ [93] Tudorache, L.: leonardtudorache/AnExecutable-Taxonomy-ofSecurityProperties-for-ProVerif-and-Tamarin: Initial Release. h t t p s : / / d o i . o r g / 1 0 .5281/zenodo.19352740 . https: //doi.org/10.5281/zenodo.19352740 [94] Basin, D., Cremers, C., Dreier, J., Meier, S., Sasse, R., Schmidt, B.: Tamarin Prover. http s://github.com/tamarin-prover/tamarin-pro ver [95] Zheng, Y.: Signcryption and its applications in efficient public key solutions. In: Okamoto, E., Davida, G., Mambo, M. (eds.) Information Security, pp. 291–312. Springer, Berlin, Heidelberg (1998) [96] Holmes, R., Murphy, G.C.: Using structural context to recommend source code examples. In: Proceedings of the 27th International Conference on Software Engineering. ICSE ’05, pp. 117–125. Association for Computing Machinery, New York, NY, USA (2005). https://doi.org/10.1145/1062455.1062491 . 25