A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols

Abstract

In order to develop trustworthy distributed systems, verification techniques and formal methods, including lightweight and practical approaches, have been employed to certify the design or implementation of security protocols. Lightweight formal methods offer a more accessible alternative to traditional fully formalised techniques by focusing on simplified models and tool support, making them more applicable in practical settings. The technical advantages of formal verification over manual testing are increasingly recognised in the cybersecurity community. However, applying formal methods, even in their more practical forms, outside highly specialised research settings remains challenging. For practitioners, formal modelling and verification are often too complex and unfamiliar to be used routinely. In this paper, we present an Eclipse Integrated Development Environment for the design, verification, and implementation of security protocols and evaluate its effectiveness, including feedback from users in educational settings. It offers user-friendly assistance in the formalisation process as part of a Model-Driven Development approach. This IDE centres around the Alice & Bob (AnB) notation, the AnBx Compiler and Code Generator, the OFMC model checker, and the ProVerif cryptographic protocol verifier. For the evaluation, we identify the six most prominent limiting factors for formal method adoption, based on relevant literature in this field, and we consider the IDE’s effectiveness against those criteria. Additionally, we conducted a structured survey to collect feedback from university students who have used the toolkit for their projects. The findings demonstrate that this contribution is valuable as a workflow aid and helps users grasp essential cybersecurity concepts, even for those with limited knowledge of formal methods or cryptography. Crucially, users reported that the IDE has been an important component to complete their projects and that they would use again in the future, given the opportunity.

1. Introduction

The importance of formal methods in the development of security protocols has become increasingly evident in recent years, as formal verification provides a high degree of confidence in a protocol’s security, ensuring that critical flaws are identified early in the protocol design phase, thereby reducing the risk of exploitation in real-world deployments.

Serious vulnerabilities have been uncovered in several protocols that constitute the backbone of the digital infrastructure allowing individuals and organisations to perform their online activities.

For example, a critical design-level vulnerability such as the KRACK attack [1] on the WPA2 Wi-Fi standard allowed for decryption, packet replay, TCP connection hijacking, and HTTP content injection on nearly all devices using the standard. TLS, one of the most ubiquitous protocols, has also exposed serious vulnerabilities, leading to various attacks, including Heartbleed [2], Freak [3], and downgrade attacks [4].

This situation has driven the research and development community to place a greater emphasis on rigorous verification methods. Several authors have now formally verified TLS 1.3 [5,6,7], and similar notable work has been undertaken for other protocols, including Signal [8].

These efforts include the use of automated verifiers such as ProVerif [9], Tamarin [10], and OFMC [11], among others. The application of these tools has enabled security specialists to design robust protocols during the early stages of development rather than relying on the reactive approach of addressing vulnerabilities post-deployment.

Despite these advances, attacks continue to exploit vulnerabilities in software implementations [12]. Those include buffer overflows in OpenSSL, with the HeartBleed bug [2] leaking sensitive information and data confusion exploits on GnuTLS [13], where a server can be tricked into using wrong data as an encryption key. Those attacks are immediately applicable to a wide range of targets, as they leverage vulnerabilities in security libraries. In such cases, missing defensive run-time checks at the implementation level enabled those attacks, even though such checks were implied, even implicitly, in the design phase, but failed to materialise or work in the concrete code. To alleviate these issues, there is now ample consensus among experts that the application of formal methods for security should be more widespread [14,15]. Formal-backed code generation in a convenient environment would bridge the gap between formal design and implementation. It would also show examples of necessary implementation checks that reflect the design intent and prevent misconceptions or oversights.

Prior to the implementation of a protocol, its design requires considerable effort, involving extensive expertise and verification.

First of all, a fundamental security paradigm that must be taken into account is the Dolev–Yao attacker model [16], which defines the assumptions about the attacker’s capabilities. Specifically, it assumes that the adversary has total control over the network, can intercept and modify data in transit, and can perform composition and decomposition operations using the same rules as honest agents. This paradigm has practical applications in the development of the aforementioned verification tools.

Having a suite of tools for the formal modelling and analysis of security protocols to support software engineers is essential. However, when multiple tools need to be used in coordination, this creates a significant complexity barrier for users due to their complexity, unfamiliar interfaces, and difficulties in the interpretation of results [15].

Our research aims to make this initial design step more accessible for non-experts and more convenient for experts, so we can encourage the use of formal methods for security protocols and avoid the high costs associated with late vulnerability detection [17] or the potentially catastrophic consequences of deploying vulnerable protocols on a large scale. In general, a lack of control over the specification and verification process could, at best, lead to misunderstandings. A beginner would benefit from being guided by warnings, error messages, and a simple push-button solution, while an expert could leverage more advanced features for quality control, all while enjoying increased productivity. Thus, once a design is established, it could be thoroughly verified without the need to manage the complexity of command-line interactions.

This design effort must also be supported beyond dedicated tools for a specific modelling language. When outlining the skeleton of a protocol, one should be able to reason about it without having to rely on a lower-level language, which would be time-consuming. Therefore, we advocate for a very high-level specification language, accompanied by a suite of tools built around it.

The research community [18,19] supports the notion of high-level abstractions, and the 2020 Expert Survey on Formal Methods [14] highlights that the most reported limiting factors for the adoption of formal methods are the lack of training, tool limitations and insufficient maintenance, and the lack of integration of formal methods into the industrial design life cycle.

The educational barrier to adopting formal methods is mentioned in one comment: “Education in formal methods frightens off students and puts them off for life rather than showing potential benefits”. Furthermore, the integration of formal methods tools in general, and in IDEs specifically, has been recommended by many experts [14,15] and identified as one of the most important measures to overcome the barriers for industry adoption [20].

Tool integration can be an important way to enable education and training, as this is the other major barrier identified in relevant studies [14,15,20]. Therefore, our approach to tool integration also aims to facilitate training, thereby lowering the barriers and yielding positive outcomes for learners, in terms of both reducing error rates and increasing confidence, as identified by Skevoulis et al. [21]. This study suggests that a lack of integrated tools constitutes a significant challenge to the adoption of formal methods, highlighting the need for more intuitive educational approaches.

Other studies [22,23] also recognise the pedagogic value of integrated formal methods tools to improve comprehension and engagement.

1.1. Research Contribution

The main objectives of our work focus on the verification of symbolic models for cryptographic abstractions [9,10,11], alongside the automatic generation of security protocols at both the specification and implementation levels [24,25,26]. This approach not only reduces the complexity of the tasks but also promotes the broader adoption of formal methods in the development of secure protocols.

In order to encourage users to leverage formal methods, we propose an approach based on the following key components:

• A simple and intuitive language for the lightweight [27,28] formal specification of security protocols. This addresses the problem of complexity in formal methods by helping users familiarise themselves with system design from a high-level perspective, before delving into verification. The expected benefit is that users, especially non-experts, can engage with formal methods more easily and develop a better understanding of protocol design without being overwhelmed by technical details [29].

• A Model-Driven Development (MDD) strategy for the automatic generation of programs from formally verified abstract models. This eliminates the need for users to prototype at multiple abstraction levels, ensuring consistent and rigorous translation from model to implementation. The benefit is a reduction in development time and errors, as the MDD approach streamlines the workflow, allowing users to focus on design correctness rather than manual coding at each layer [30,31].

• An Integrated Development Environment (IDE) with the push-button integration of existing tools and real-time modelling/verification feedback. This addresses the issue of tool complexity and integration. By providing a seamless environment for developers, it automates significant parts of the workflow and offers real-time feedback, thus improving both the clarity of the specification process and control over the verification stage.

In this paper, we focus on the latter element, the environment, which is supporting the overall approach, leveraging the two other components.

The AnBx IDE (available at https://www.dais.unive.it/~modesti/anbx/ide/, accessed 20 November 2024) is an Integrated Development Environment for the design, verification, and implementation of security protocols. It has been actively maintained and enhanced since its first prototype was released in 2017 [32] and aims to build on this by offering a workflow that benefits both novices and experts alike.

It is developed as a plug-in using XText [33,34], a framework for creating software languages, including modelling languages, and leverages existing tools for specification, code generation, and the verification of security protocols.

The purpose of the AnBx IDE is to provide an all-in-one solution for users, offering support for high-level protocol specification, automatic code generation, and seamless integration with verification tools. Specifically, it facilitates:

• Specification: The IDE allows users to specify protocols in the simple Alice & Bob (AnB) notation [35] or its extension AnBx [36], a high-level abstraction for defining cryptographic protocols.

• Code generation: The AnBx Compiler and Code Generator [25] automatically generates ProVerif specifications and Java implementations, among other targets, from the AnB and AnBx models.

• Verification: The IDE integrates the symbolic model checker OFMC [11] and the cryptographic protocol verifier ProVerif [9] to allow for automated formal verification of protocols. This integration provides users with a smooth compilation and verification workflow.

At the time of writing, the IDE supports the AnB notation of OFMC [35], the applied-pi calculus utilised by ProVerif [37], and the AnBx language used to specify security protocols [36]. The integration of these verification tools within the IDE facilitates a streamlined design and verification process. This aligns with observations made by Kulik et al. [15], who highlight that incorporating verification tools directly into development environments promotes the adoption of formal methods in industry, as evidenced by the growing use of static code analysers [38].

The IDE, along with the interaction with the back-end tools, includes many features meant to help programmers increase their productivity, like syntax highlighting, code completion, code navigation, and quick fixes. After verification, the IDE offers a visual interpretation of the results for clear and immediate user understanding. We put a particular emphasis on the workflow aspects of formal verification. This IDE automates many intermediate steps and key aspects of this effort, such as scheduling, task management, and result visualisation. These aspects combine usability and productivity advantages for users at all levels. This contribution represents a complete overhaul of the preliminary version of the tool introduced in 2017 [32]. The earlier version only supported AnB-style specifications, with minimal workflow automation and no mechanisms for handling verification results or managing tasks effectively. In this revised version, we have added numerous features, observing students’ work and feedback to enhance usability, along with a survey to assess the usefulness of the tooling suite.

In general, incorporating formal methods into a computer science curriculum is beneficial not only for producing robust software and hardware but also for fostering a deeper understanding of the underlying logical principles [21,39]. For example, Broy et al. [40] argue for the teaching of formal methods, emphasising that it provides a foundation for rigorous reasoning about specifications. In line with their argument that basic formalism should be taught to all students, while specialised formal methods are reserved for specific fields, we think, supported by feedback from our students, that our IDE could serve as a valuable tool to facilitate the integration of formal methods into computer science courses.

1.2. Outline of the Paper

We begin by detailing the motivation behind this approach in Section 2. Next, in Section 3, we introduce the specification languages and the back-end tools, and in Section 4, we present our methodology. Section 5 presents the IDE’s construction and features, and Section 6 and Section 7 provide our evaluation and discuss related work. Finally, Section 8 concludes the paper and outlines potential future work related to our approach.

2. Motivation

In this section, we discuss the challenges in the usability and adoption of formal methods, the need for lightweight and practical formal methods, as well as the necessity for Integrated Development Environments that can support the utilisation of associated tools. Moreover, we consider the cryptographic misconceptions observed in a population of cybersecurity students, which further reinforces the need to provide supportive development tools that can help overcome such misconceptions.

2.1. Challenges in the Usability and Adoption of Formal Methods

Formal methods, while technically successful, have not become a universally adopted solution. Similar to programming languages, specialised methods have emerged for specific fields to avoid the complexities associated with a “one size fits all” approach. A study on the barriers to the industrial adoption of formal methods [20] suggests that education and tooling are the two most important factors, with highly specialised experts being needed to operate tools that are often neither integrated nor compatible with development tools. The timeline issue is also raised, with formal analysis being perceived as too long a process to be applicable. Demonstrating the practicality of such methods, both for potential and current professional users, could bring formalisation to the foreground, as discussed in [15,41].

To aid in this matter, lightweight formal methods [27,28] are commonly endorsed in the literature and are limited in terms of the languages that can be automatically analysed, contrasting with earlier approaches such as Z [42]. These methods are abstract enough to remain practical while focusing on the essential aspects that need to be formalised. In this context, our interest lies specifically in security protocols rather than the underlying machines on which they operate.

The lightweight approach is employed in this paper, starting from the observation that many developers are largely unfamiliar with formalisation concepts. For formal methods to be effectively implemented, a fundamental understanding is essential. For instance, the constructivist learning theory [43,44] suggests that new knowledge is constructed through a combination of prior knowledge and current experience. Surveys on the practicality and deployment of formal methods [14,15] state that this integration should come to software-built toolchains and not for the purposes of formalism only. This cross-integration approach is also advocated by Davis et al. [20].

To facilitate the learning process, our objective is to eliminate obstacles to experimentation. Users should not struggle with setup procedures before they can begin specifying and verifying protocols. By enabling users to achieve results with minimal time and effort, we aim to prevent discouragement and promote continued engagement in the formalisation process.

To address these complexity challenges, an intuitive language in the Alice & Bob style is essential to enable learners to understand fundamental concepts in formal methods and security protocols [29], and the relevance of AnBx has been emphasised by an external study in [45], particularly to support model-driven security analysis. Brucker et al. [29] mention the differences in teaching experience between AnB with OFMC, which successfully enabled undergraduates to grasp Dolev–Yao formalism, as well as more specialised languages and frameworks such as Isabelle/HOL [46], which proved to be too complex even for postgraduate students. However, despite being considerably simpler than other languages (e.g., the applied-pi calculus used by ProVerif), AnBx/AnB can still present technical challenges for beginners. For instance, the distinction between symmetric and asymmetric encryption is not always immediately clear. Furthermore, in the context of asymmetric encryption, the correct usage of keys for different purposes (i.e., encryption versus signature) is crucial, and it is essential that key material is not confused [47]. In AnBx, this distinction is reinforced by providing distinct predefined functions: pk(.) for keys used for asymmetric encryption and sk(.) for keys used for digital signatures.

By combining an intuitive notation with supportive tooling, the amount of experience one can gain with cybersecurity concepts can be significantly increased, with much less difficulty than would be observed without such support. Lowering the adoption barrier for formal verification not only enables users to become proficient in the formal aspects of security but also helps them develop a deeper understanding of more general security-related concepts. In fact, sketching ideas in a high-level notation and receiving immediate feedback from formal verification creates a rapid learning loop that encourages experimentation. This approach ensures at least a high-level understanding of how the underlying primitives operate.

The core usability challenges and limits in the widespread adoption of formal methods for security, in light of the 2020 Expert Survey on Formal Methods [14], the study on the barriers to the industrial adoption of formal methods [20], and other work on formal methods usability issues and practical challenges [15,48], can be summarised as follows:

1. Complexity: The inherent complexity of these methods often requires users to possess a good understanding of mathematical concepts and logic, resulting in a high learning curve that can be deterring for practitioners without a formal background or knowledge of a specific verification framework.

2. Limited Tool Integration: The limited availability of well-integrated tools can create inefficiencies in workflow, hindering the effective utilisation of formal methods. In particular, a majority of criticisms pointed out that research is not oriented enough towards the consolidation of existing results to make them available to a wider audience.

3. Unfamiliar Interfaces: Specialised, unusual, and inconsistent user interfaces across different tools may lead to confusion, making it challenging for users to navigate various applications.

4. Interpretability of Results: The interpretability of results is often compromised due to complex output formats and cryptic error messages, making it difficult for users to derive actionable insights.

5. Scalability Issues: Many formal verification tools struggle to handle complex systems efficiently, resulting in long processing times and significant resource consumption.

6. Limited Documentation: Limited or hard-to-find documentation and community support exacerbate these challenges, leaving users without sufficient guidance.

2.2. The Benefits of Integrated Development Environments

Before implementing an IDE for AnBx, we conducted tutorial sessions in which students used command-line tools for modelling, verification, and code generation, alongside simple text editors. However, the setup of these tools and managing the complexity of the toolchain proved to be a deterrent and a distraction for some students, particularly those with lower skills or motivation. We also considered a simpler syntax-highlighting solution in Notepad++, but this lacked critical features, such as real-time validation feedback from the editor and a flexible, user-friendly tool parameter selection.

Although a script-based approach could have been applied to security protocols, we chose a different direction in this case. This decision was motivated not only by some users’ preference for graphical user interfaces (GUIs) over command-line tools [49] but also by the complexity of integrating a toolchain with multiple heterogeneous tools, which requires a level of scrutiny beyond that of a standard, well-tested programming language compilation chain. While scripts can be highly effective for experts, they tend to be less accessible for beginners.

Given these considerations, we opted to support users with an IDE, as Integrated Development Environments not only enhance productivity but also lower the adoption barrier for new methodologies and technologies.

To leverage languages and back-end tools effectively, an integration effort can foster openness and interest among developers in adopting such tools. An IDE can greatly simplify the setup and configuration of the environment. We align with the perspective of Tabassum et al. [50], believing that an IDE can facilitate secure coding by providing instant security warnings, detailed explanations, and more. The Kulik et al. [15] and the Davis et al. [20] surveys report that there is a general consensus on advocating for the improvement of automated formal verification tools to ease the entry into the world of formal methods. The direct integration into an existing IDE is mentioned as a step in this direction, and we aim to participate in this effort. There is also significant empirical evidence supporting this claim; widely used IDEs such as Eclipse, Visual Studio, and the IntelliJ suite demonstrate that developers appreciate the functionality they provide. The choice of Eclipse here is motivated by its extensive and continued support for XText.

On a broader scale, Kuusinen [51] conducted a survey involving 45 developers from 21 countries to determine their ideal features in an IDE. In addition to being efficient and flexible, developers expressed a desire for the IDE to be informative and intuitive to use. They indicated that it should support a cohesive development workflow, offering control and clear visibility of both the code and the overall development situation. This is precisely what we aim to provide through features such as editing, visualisation, and task management.

2.3. Identification of Potential Cryptographic Misconceptions

Initially, we sought to assess students’ knowledge of applied cryptography to better tailor teaching and learning strategies in our university courses. Understanding students’ misconceptions and their baseline knowledge is vital for designing effective educational interventions, particularly in a specialised field like cybersecurity. The results also enabled us to understand how an IDE for security protocols could support users in avoiding the misuse of cryptography.

To achieve this, we developed a survey consisting of 24 multiple-choice questions. For each question, there were four options, one of which was correct, with the exception of a few questions that offered only three options, as the nature of these questions allowed for just three plausible choices. The survey includes some questions about general cybersecurity knowledge but focuses on applied cryptography. It covers concepts like authentication, confidentiality, types of communication channels, symmetric and asymmetric encryption, message authentication codes, and hashing functions.

The questionnaire was administered between 2021 and 2024 to four groups of students enrolled in the MSc Cybersecurity course at Teesside University in the United Kingdom, during lab activities, and they were not allowed to consult any sources of information while answering the questions, which were presented in random order.

In total, we surveyed 59 students, 48 male and 11 female. The backgrounds of the participants were diverse, though none had an undergraduate degree specifically in Cybersecurity. Most of the participants had studied computing-related degrees (Computer Science, Networking and Information Technology), and a few individuals had Engineering degrees in fields unrelated to computing. With a few exceptions, the students completed their undergraduate studies abroad, with Nigeria and India being the most represented countries. Twenty-five participants took the survey at the beginning of their postgraduate studies, while the rest completed it after a year.

To further understand the technical competencies of the students and identify areas requiring further development, an initial self-assessment of skills was also conducted. This enquiry considered proficiency in key areas, including networking, system administration, cybersecurity fundamentals, and programming.

Overall, for the purpose of this research, the sample is representative of a population of different educational backgrounds and levels of expertise. A significant number of students (71%) rated their networking skills as Strong, while 57% felt the same about their Windows system administration capabilities. In contrast, only 21% of students considered themselves Strong in Linux system administration, highlighting a major area of concern, where 50% reported feeling Weak. Ethical hacking skills showed mixed results, with 14% rating themselves as Very Strong, 36% as Strong, 43% as Average, and 7% as Weak. Finally, in scripting and programming, only 14% of students felt Strong, while 64% rated their skills as Weak, indicating a significant need for improvement in this area. Their limited mastery of programming and security subjects makes them ideal candidates for this study: without a strong foundational understanding, they are more prone to misconceptions in cryptography and would likely face increased confusion and disengagement without adequate supporting tools.

The results of the applied cryptography survey allowed us to identify the most prominent cryptography misconceptions, as a strong understanding of applied cryptography at the symbolic level, used by the verification tools in this study, is crucial for modelling protocols and interpreting the results of verification tools. The identified misconceptions are reported below:

Symmetric vs. Asymmetric Encryption Over a third (39%) did not know that the same key is used for both encryption and decryption in symmetric cryptosystems, and 22% confused it with other systems, stating that different independently generated keys are used.

Twenty-two per cent of the respondents incorrectly claimed that the main disadvantage of symmetric encryption is algorithm complexity, while 31% believed it is less secure. The core issue lies in securely sharing the secret key, which only 48% understood.

The distinction between symmetric and asymmetric cryptography is often unclear; 29% mistakenly believed that public key cryptography is symmetric, and 22% that it is both symmetric and asymmetric.

Usage of Encryption Consequently, less than half (44%) correctly identified that asymmetric cryptography can be used for encryption, digital signatures, and integrity verification. Misunderstandings persist, with 39% unaware of who should use the private key for decryption and 25% mistakenly thinking it should be used by both sender and receiver.

Only 17% correctly identified that the recipient’s public key should be used to establish a confidential channel, while 40% thought it should be the recipient’s private key. This indicates that over 80% are unfamiliar with basic encryption practices.

Further misunderstandings arise regarding signature keys; more than half suggested transmitting a private key, either encrypting with the private key (27%) or a public key (25%). Many did not realise this would compromise the secrecy of the private key. The correct option, using the private key without sending it directly, was chosen by only 29%.

Hash and Message Authentication Codes (MACs) Definitions of concepts like hash functions and MACs are often misunderstood. A staggering 78% incorrectly believed that a hash function’s output is non-deterministic. Only 40% recognised that hash functions compress input values, work on arbitrary-length input, and produce fixed-length output.

Regarding HMAC, 54% provided the correct definition, while 22% incorrectly associated it with the Diffie–Hellman key derivation. Other misconceptions included defining HMAC as a high-integrity medium access control (17%) or as a self-healing algorithm for stream ciphers (7%).

Awareness of potential collisions is also low; 36% stated that hash functions are unrelated to collision resistance, and only 29% knew that a MAC could correspond to multiple messages. Meanwhile, 44% assumed a one-to-one relationship, while 19% mistakenly thought multiple MACs could correspond to a single message.

Authentication and Confidentiality The cryptographic concept of authentication is widely misunderstood. While some respondents recognised that it can be achieved through something known (24%), inherent (15%), or possessed (8%), only 53% identified all options as valid. Regarding its purpose, 36% mistakenly thought it did not involve agreeing on message content, and 76% viewed it as an access control mechanism.

Many (32%) were unaware that faulty authentication could lead to Man-in-the-Middle attacks. Similarly, only 39% correctly answered that mutual authentication could prevent all three of Man-in-the-Middle, spoofing, and replay attacks. For scenarios benefiting from unilateral authentication, only 24% recognised its relevance with pseudonyms.

Best practices for security are poorly understood; only 27% acknowledged that switching off a device when unused does not adequately maintain confidentiality. Students must learn that confidentiality relies on tailored security measures and network security under Dolev–Yao assumptions.

General Knowledge We also posed general questions about existing technologies. A substantial 84% correctly indicated that a secure channel must be both authentic and confidential, and 76% identified “an internet scam convincing users to provide confidential information” as phishing.

However, the proportion of correct answers diminishes with more specific topics. Only 58% knew that PKI stands for Public Key Infrastructure, while 57% recognised that a certificate from a Certificate Authority guarantees a public key’s ownership. A mere 37% could identify Diffie–Hellman as a method for generating a one-time session key, and just 31% knew that TLS secures HTTP connections, often confused with SSH (34%).

Although the diverse educational backgrounds of participants may explain some incorrect responses, significant misconceptions still emerged. The lack of formal training in cybersecurity in their undergraduate studies and the different levels of expertise, particularly among students at the beginning of their postgraduate studies, likely contributed to these misunderstandings. Those results align with other studies presented by Lindmeier et al. [52] or Geels [53], where fundamental beginner mistakes on definitions, cryptography usage, and network assumptions happen regularly. Cryptography misuse has also been observed in [54] browsing programming forums.

Overall, the survey results highlighted several misconceptions among participants that have significant implications for the development of an IDE for security protocols using symbolic models in the Dolev–Yao style, such as the Alice & Bob notation.

A notable number of students struggled to differentiate between symmetric and asymmetric encryption, with many unaware that the same key is used for both encryption and decryption in symmetric systems. This lack of understanding can hinder their ability to model protocols accurately.

Moreover, misconceptions about the correct applications of asymmetric cryptography, where participants failed to recognise agents’ roles in encryption, digital signatures, and integrity verification, along with confusion surrounding private keys, with many incorrectly believing they should be shared, suggest a need for the IDE to incorporate elements that address the misuse of such concepts.

Given these identified misconceptions, it is clear that there is considerable potential for progress in an appropriate environment. The 2020 expert survey [14] supports this sentiment: they largely consider that while formal methods bring success on a technical level, there remains considerable unexploited potential for these methods to become more widespread among practitioners. In particular, these experts point out that both education and software tools are lacking to support the broader adoption of formal methods.

3. Background

In this section, we describe the XText framework, which serves as the foundation for our Integrated Development Environment. We outline the input languages and back-end tools currently supported by the IDE, highlighting its integration of the AnBx Compiler and Code Generator, the model checker OFMC, and the cryptographic protocol verifier ProVerif. This integration enables users to effectively specify, verify, and implement security protocols, streamlining the development process.

3.1. XText

XText [33,34] is a popular workbench for the development of Domain-Specific Languages (DSLs), which is part of the Eclipse ecosystem. It facilitates the automatic generation of essential components such as parsers, validators, formatters, and highlighters, supporting the customisation effort for any given language by providing a robust existing architecture. In Xtext, grammars are expressed in Extended Backus–Naur Form (EBNF), while other components are specified using XTend, a language based on Java that aims to be more concise, readable, and expressive. Additionally, a Model Workflow Engine (MWE) file orchestrates the generation of concrete artefacts from these specifications, allowing them to be utilised as plug-in components. The use of the XText framework for Domain-Specific Languages, such as AnBx, presents a significant opportunity for integrated formal methods, as discussed in [55]. This framework has been effectively applied in various works [56,57,58], including for common equipment like Arduino, with Asm2C++ [59], translating formal Abstract State Machines to targeted C++.

3.2. AnBx Language

The AnBx language is an extension of AnB [35] and is formally defined in [36]. On top of type signatures, AnBx introduces flexible channel notations as abstractions for communication. These can provide different authenticity and confidentiality guarantees for message transmission, including the novel notion of forwarding channels, enforcing security guarantees from the message originator to the final recipient along a chain of intermediate agents.

Figure 1 shows an example protocol in which two agents want to securely exchange a message Msg using a freshly generated symmetric key K, i.e., a key that is different for each protocol run. If K is compromised, neither previous nor subsequent exchanges will be compromised, but only the current one. This is similar to what happens in TLS, where a symmetric session key is established (using asymmetric encryption) at the beginning of the protocol. It should also be noted that this setting is also more efficient, as symmetric encryption is notoriously faster than asymmetric encryption.

The Types section includes declarations of identifiers of different types and function declarations, while the section Knowledge denotes the initial knowledge of each agent. Optional sections, Definitions and Equations, can be used, respectively, to specify macros with parameters or equational theories. In the Actions section, the action A -> B,@(A|B|B):K means that the key K is generated by A and sent on a secure channel to B. The notation @(A|B|B)denotes the properties of the channel: the message originates from A, it is freshly generated (@), verifiable by B, and secret for B. How the channel is implemented is delegated to the compiler. The designer can select between different options or simply use the default one, without having to take charge of low-level implementation details. A translation to AnB is shown in Figure 2: in this case, the channel is implemented using a challenge–response technique, where B freshly generates a Nonce (the challenge), encrypted with pk(A), the public key of A along with the sender name ({.} denotes the asymmetric encryption). This guarantees that only A would be able to decrypt the incoming message.

The response, along with the challenge, includes the symmetric key K. The response is digitally signed with inv(sk(A)), the private key of A, and then encrypted with pk(B), the public key of B. This allows B to verify the origin of the message and that K is known only by A and B.

It should be noted that in AnBx, we abstract from these cryptographic details, and we simply denote the capacity of A and B to encrypt and digitally sign using a Public Key Infrastructure (PKI) with the keyword Certified. This reflects the customary practice of a Certification Authority to endorse the public keys of agents, usually issuing X.509 certificates, allowing every agent to verify the identity associated with a specific public key. Moreover, in AnBx, keys for encryption and for signature are distinguished by using two different symbolic functions, pk and sk respectively.

Once the symmetric key K is shared securely between A and B, then B can secretly send the payload Msg ({|.|} denotes the symmetric encryption). Finally, A acknowledges receipt by replying with a digest of Msg computed with the predefined AnBx hash function, and with a value computed with the log function.

The section Goals denotes the security properties that the protocol is meant to convey. They can also be translated into low-level goals suitable for verification with various tools. Supported goals are as follows: (1) Weak Authentication goals have the form B weakly authenticates A on Msg and are defined in terms of non-injective agreement [60]; (2) Authentication goals have the form B authenticates A on Msg and are defined in terms of injective agreement on the runs of the protocol, assessing the freshness of the exchange; (3) Secrecy goals have the form Msg secret between A1,..., An and are intended to specify which agents are entitled to learn the message Msg at the end of a protocol run.

In the example protocol (Figure 1), the desirable goals are the secrecy of the symmetric key K and of the payload Msg that should be known only by A and B. There are also authentication goals: B should be able to verify that K originates from A and the key is freshly generated. Finally, two goals express the mutual authentication between A and B regarding Msg, including the freshness of the message. In summary, this protocol allows two agents to securely exchange a message, with guarantees about the origin and the freshness of the message.

3.3. AnBx Compiler and Code Generator

We briefly present the AnBx Compiler and Code Generator by illustrating the main steps involved in the automatic Java code generation for security protocols. A more detailed description can be found in [25].

The AnBx input protocol undergoes lexing and parsing before being compiled into AnB, a format that enables automated verification with the OFMC model checker. If the verification process is successful, the AnB specification can be translated into an executable narration (ExecNarr), which operationally encodes the sequence of actions that agents are expected to perform during the protocol. This step specifically involves computing checks on receptions, i.e., actions that agents must execute on incoming messages to ensure that the protocol adheres to the specification. For instance, this includes the verification of digital signatures, decryption of incoming messages, and equality tests to confirm that incoming messages match prior knowledge.

Following this, the sequence of actions can be reordered into an optimised executable narration (Opt-ExecNarr) using optimisation techniques such as common sub-expression elimination (CSE). This optimisation minimises the number of cryptographic operations and reduces the overall execution time.

The Java code generation requires an additional step, as illustrated in Figure 3. We model the protocol logic using a language-independent Intermediate Format called Typed-Opt-ExecNarr. This format serves as a typed representation of the Opt-ExecNarr, allowing for parametrised translation and simplifying code emission in the target programming language.

The type system of Typed-Opt-ExecNarr infers the types of expressions and variables, ensuring that the generated code is well typed. To that end, the AnBx compiler utilises, along the entire compilation chain, the function signature typing and other language extension information peculiar to AnBx, which are not available in AnB. It also provides the advantage of runtime checks to verify whether the structure of incoming messages matches the expected format as specified by the protocol.

Java code emission is accomplished by instantiating protocol templates (referred to as application logic), which serve as the skeleton of the application. It is important to note that only at this final stage do language-specific features and API calls bind to the protocol logic.

The verification of the protocol logic can be conducted using ProVerif, which translates from Typed-Opt-ExecNarr to the applied-pi calculus [9].

In summary, ProVerif verifies the symbolic implementation from which the Java code is emitted, while OFMC verifies the abstract model created by the designer.

3.4. Security Protocol Verifiers

Utilising several verification tools is often beneficial for cross-checking the validity of security properties under different assumptions. Galeotti et al. [61] demonstrate an integration of multiple tools into a single framework that addresses the limitations of individual tools. Some differences between verification tools are detailed in [62], with updates reflecting the most recent developments in ProVerif.

OFMC [11] utilises the AVISPA Intermediate Format (IF) [63] as its native input language. IF enables the description of security protocols as infinite-state transition systems using set rewriting. Additionally, OFMC supports the AnB language. The tool performs both protocol falsification and bounded session verification by exploring the transition system in a demand-driven manner. The major techniques employed by OFMC include the lazy intruder, a symbolic representation of the intruder, and constraint differentiation, a search-reduction technique that combines the lazy intruder with concepts from partial-order reduction. This integration effectively reduces the search space without excluding potential attacks or introducing new ones.

ProVerif [9] is an automated verifier for cryptographic protocols that models both the protocol and the attacker using the Dolev–Yao [16] symbolic approach. This approach represents data and ideal cryptographic operations symbolically, assuming the attacker has complete control over public communication channels. Unlike model checkers, ProVerif can model and analyse an unbounded number of parallel sessions of the protocol. However, similar to model checkers, ProVerif can reconstruct a possible attack trace when it detects a violation of the intended security properties. While ProVerif may report false attacks, if a security property is reported as satisfied, it is guaranteed to hold in all cases. Therefore, careful analysis of the results is crucial when attacks are reported.

In our context, it is important to note that OFMC is sound and complete, which, in practical terms, implies that if there is any attack on the protocol, the tool will detect it, and no false attacks can be reported. In contrast, ProVerif is only sound, meaning that potentially false attacks can be reported, for example, due to over-approximation. While it is remarkable that this tool can verify protocols for an unbounded number of sessions, non-termination or undecidability may occur in some cases. Unlike OFMC, ProVerif can check diff-equivalence properties [64], determining if protocols share the same structure while differing only in the messages they exchange. Conversely, OFMC accepts a simpler input language (i.e., AnB) and provides an attack trace that is easier to interpret. Furthermore, ProVerif may flag certain goals as satisfied even when the associated protocol steps are unreachable due to errors in the encoding of the model, which can lead to confusion regarding the protocol’s security.

4. Methodology

The methodology that our IDE intends to support follows the classical Model-Driven Development (MDD) philosophy.

The process involves specifying an abstract model of a security protocol, reasoning about its correctness and soundness with the aid of verification tools, and ultimately generating a concrete executable implementation. The MDD methodology, applied in the context of our IDE, is detailed in Figure 4, and our contribution focuses on reducing friction between each step of the process to make it user-friendly. Achieving this requires automating the design and development workflow, as well as supporting users with early warnings, error messages, and suggestions to identify, correct, and prevent mistakes.

While every step in this process would typically have to be performed manually, or at best using scripts, the IDE can automatically launch a chain of compilation, verification, implementation, and execution steps with just a couple of keystrokes. This makes the process flexible and approachable for beginners.

The integration advantages and features offered by the IDE are summarised in Figure 5. The editor enables the modelling of protocols with features like autocomplete, formatting, validation, and scoping. Then, compilation, verification, and execution procedures are supported with task management, logging, and console output separation. After verification or execution, the IDE provides clear visualisation, with console output colouring and a dedicated Eclipse view window.

5. AnBx IDE Features and Components

In this section, we detail how we cover the entire process of writing, verifying, generating, and running code within the same environment, with supporting features and components. Our approach integrates language and interface for a complete Model-Driven Development (MDD) workflow that remains user-friendly.

5.1. Editing Security Protocol Models in Different Specification Languages

Several grammars are defined in the AnBx IDE to encode security protocols in different specification languages: Alice & Bob notation (AnB and AnBx), applied-pi calculus (PV) and AVISPA/OFMC Intermediate Format (IF).

As we advocate for a Model-Driven Development (MDD) approach, the AnB notation and its extension AnBx are fully supported, along with common IDE features that we detail later in this section.

This support extends not only to AnB-like notations but also to the additional languages of the verification tools, namely applied-pi for ProVerif, and specifications in the OFMC Intermediate Format (IF) and Theory (thy) formats. This enables users to comfortably edit more fine-grained specifications than allowed in AnB style, thereby becoming better acquainted with the tools’ inner workings.

5.1.1. Getting Started with Wizards

To get started before writing a specification, the user can utilise appropriate wizards. The IDE features wizards for AnBx and ProVerif projects, which can be accessed with just a few clicks through the File→New menu commands. A stub is generated, akin to the “Hello world” code in other programming languages. Similar wizards also allow for the creation of single AnBx or ProVerif files without generating an entire project structure.

5.1.2. Syntax Highlighting and Outline

For easier visualisation, syntax highlighting is applied to the specifications. This feature aids in locating sections and keywords, and it can be customised thanks to XText’s internal DefaultSemanticHighlightingCalculator, which can be extended at will. Specifically, we have chosen a red colour for section names, while keywords receive the default purple highlighting. All supported languages benefit from this highlighting.

Additionally, for all languages in the AnBx IDE, we provide an outline of the specification for visualisation at a glance. This outline summarises the structure and core aspects of the currently edited file in a dedicated collapsible tree view within Eclipse.

5.1.3. Formatting

To maintain a clear structure and continue with the visualisation features, the IDE can auto-format AnB/AnBx files. Spaces between tokens, line breaks, and indentations are enforced, ensuring that the readability benefits of using a high-level notation are not diminished after long editing sessions. This formatting can be triggered through the defined Eclipse keyboard shortcuts, resulting in a structure similar to that shown in Figure 1 and Figure 2.

5.1.4. Autocomplete and Scoping

When writing any specification, autocomplete is one of the most essential features. In our supported languages, declared entities and keywords are suggested to the developer, along with other symbols that conform to the language grammar at a specific point.

To determine what can legitimately be used at a given time in the specification, a notion of scoping needs to be introduced in most languages. For example, in AnBx, one can use macros, and their parameters must be local to the macro. Similar requirements exist in ProVerif, albeit in a more complex manner, where bound variables and multiple processes can be used. Scoping for both languages is fully supported in our plug-in.

An appropriate use of scoping is particularly beneficial for specifications that might be confusing at first glance. We take an example from the ProVerif manual [65] in Figure 6 to illustrate our point.

The query in line 4 refers to previously declared names such as event e and the free name A. However, new a, x, y, and new B are forward references. Pointing to one of them would take us to their declaration locations, specifically line 6 for a and line 7 for B. ProVerif also employs bindings for variables that exist within a certain scope. In this context, the square brackets for new a constrain the values of x and y to equal A and new B, respectively, within the scope accessible by new a. Without a solid understanding of ProVerif applied-pi, this specification could appear obscure. Therefore, declaration tracking through scoping serves to clarify these relationships.

5.1.5. Validation: Type, Arity, and Semantics Checking with Quickfixes

As with many other standard IDEs, we provide type and arity checking. Functions and other language features can exhibit a signature, which must be enforced without the need to run the verification tools. In addition to what the user explicitly defines, a set of predefined symbols and signatures is taken into account. For example, AnB protocols rely on primitives such as inv, exp, and xor to denote a private key, exponentiation, and exclusive-or. Meanwhile, AnBx protocols also rely on public key functions pk and sk, as well as a symbolic hash function. ProVerif includes predefined types such as bitstring, bool, and nat. These signatures and symbols are hard-coded as libraries that a specification can use as if they were defined in the current file.

The IDE enforces many sanity checks and signals any violations to the user through the XText Validator component. Moreover, the validation feature notably handles the arity of function calls and type-checking. Taking the protocol defined in Figure 7 as an example, a function signature like $\mathtt{log}:\mathtt{Agent},\mathtt{Number}\to \mathtt{Number}$ will be compared to its calls, accepting only Agent or a function returning an agent as the first parameter. Similarly, a call to log cannot be used as a parameter unless the called function’s signature expects a Number.

The protocol in Figure 7 contains two errors. The first error arises because a channel mode only accepts parameters of type Agent. The type checker returns the cause of the error and provides two suggestions on how to resolve it. The second error occurs due to the use of illegal cryptographic notations. In fact, a challenge for a developer is determining which encryption to use in specific situations. The validation system guarantees the correctness of types according to the cryptographic specifications. The user is attempting to use a public key in a symmetric cipher scheme. To fix this error, the user has two possibilities: changing the type of K to SymmetricKey or changing the encryption scheme from symmetric to asymmetric. However, the protocol is safe only in the first case, while the second case introduces a potential attack. This can be determined by verifying the protocol.

These examples demonstrate how the IDE can assist users with limited knowledge of cryptography in avoiding design mistakes. The use of the most basic primitives, such as pk, might seem clear to someone familiar with the language. However, even understanding that this symbol represents the key of a particular agent, and that only this agent is entitled to it, may not be evident when described as a public value. During our practical activities with students, some attempted to model a shared symmetric key as pk(A,B), confusing symmetric and asymmetric schemes, and still under the impression that one key must be used and shared by both the sender and the receiver with public-key cryptography. Instead, pk is a function that is used for asymmetric encryption and expects a single parameter of type Agent. The feedback in the editor is immediate, eliminating the need to run the compiler and track line and column numbers, resulting in a short-lived misconception.

The editor can also help to avoid possible mistakes with the AnBx channel’s syntax, which consists of a triple (auth∣vers∣dest). For example, the auth parameter (the agent authenticating a message, e.g., with a signature) and the vers parameter (a set of agents that the auth intends to enable to verify the authenticity of the message) can only occur together in a single channel mode but not individually (see Figure 8).

5.2. Running the Verification Tasks and Generating Code

Once the user has specified the protocol according to their vision, benefiting from editor feedback, a combination of UI components and workflow helpers can be employed. These features provide flexible and convenient control over the upcoming compilation and verification tasks.

5.2.1. Configuration Dialogs with Options and Help

The integration of design and verification tools begins with dedicated UI windows that allow users to set command-line parameters and execute common tasks with just a few clicks.

For example, these dialogs feature dropdown lists, spinners, and checkboxes for the most common options and facilitate interaction across tools. An AnBxC additional args textbox is provided for each tool, enabling users to specify any command-line parameters without cluttering the interface.

Next to this textbox, we include a help button that opens the manual for the relevant tool. The window that appears contains a link to the complete official documentation, along with a scrollable, selectable text area detailing the options, presented as the tool, would display them in a terminal when requesting help. An example of tool dialog is given in Figure 9, featuring the one for AnBxC.

The Launch-associated validator option triggers automatic verification with OFMC or ProVerif, depending on the chosen output format. It is important to note that enabling a real-time modelling and verification feedback cycle is crucial for increasing productivity when dealing with complex protocols. Adjacent to this option, a settings button opens the dialog for the associated verification tool, namely OFMC or ProVerif, allowing users to configure verification options for the next run without unnecessary back-and-forth.

As the AnBx Compiler enables users to generate a Java implementation for the specified protocol, the same option triggers the building and execution of the generated code. This process is orchestrated by an Ant file, a standard build file for the Eclipse platform and other IDEs. Alternatively, the associated Java project can be opened in Eclipse, where users can manually run its Ant build file. Observing the execution trace at a concrete level after working in AnBx is essential, as it allows users to understand how abstract concepts are translated into the real world. This understanding is crucial for grasping the nuances of cryptographic operations and their practical applications.

5.2.2. Supporting Users in Their Workflow

Opting for an Integrated Development Environment is beneficial for automating intermediate steps and saving considerable time, avoiding unnecessary back-and-forth.

Typically, the running time of OFMC increases drastically with the number of sessions. For fast prototyping, it is important to first verify that our specification satisfies the security goals in a single session and then verifies it again with multiple concurrent sessions. The IDE features an option for this in the OFMC dialog. The Run with one session first option attempts verification according to the options specified in the dialog, with the session number set to 1. If an attack is found, the process stops here, and verification with concurrent sessions only occurs if no attack is identified.

Intermediate steps with OFMC may also arise when we want to generate an IF representation of the AnB protocol and then verify it. By using a simple Run on an on-the-fly generated IF file option, the generation and verification commands are executed sequentially.

Another important aspect of OFMC verification is the use of equational theories. These are specified in .thy files, but we can automatically generate these files using the AnBx Compiler along with appropriate AnBx notations. From an AnBx file, the compiler can output a theory file that encodes the relations in the Equations section, allowing non-experts to reason with custom functions while saving considerable time for more advanced users. Understanding the internals of OFMC and how to encode equational theories for this particular tool is not necessary. Users can then concentrate on the core aspects of the logic and avoid wasting time that could be better spent on understanding the reasoning behind such relations. Appropriate output formats and options are available in the AnBx Compiler and OFMC dialogs to generate and include these theory files.

5.2.3. Verifying Single or Multiple Security Goals in Parallel

The Single-goal generation option (Figure 9) generates files in the target format as if we had a separate copy of the protocol for each goal. The verification tools can then run on every generated protocol and test a single property. Compared to checking all goals within a single process, our experience shows that the overhead of spawning multiple processes is more reasonable and well worth it when aiming to obtain precise information on each goal as quickly as possible. Moreover, this approach takes advantage of multicore CPUs, offering significant time savings through parallelisation.

With OFMC, it is particularly useful to quickly identify which goals have failed, as it typically reports the first attack trace it finds. Although the output generated by OFMC clearly indicates the type of goal that has been violated (e.g., authentication, secrecy), it can be much more challenging to determine the exact vulnerable goal in cases where multiple goals of the same category fail.

This solution with single goals helps to maintain a readable and concise verification output. Moreover, OFMC operates with a bounded number of sessions. If we obtain a result for one session and subsequently wish to check whether all goals can be satisfied with multiple sessions, this parallel approach can yield results considerably faster than waiting for all the goals of a complex protocol to be checked sequentially. We observe a particular parallelisation advantage in this regard in the case of ProVerif.

It should be noted that in ProVerif, some goals can be deemed satisfied when the associated protocol steps are unreachable, as the goals are specified as implication queries. Indeed, not reaching the point where we could have A makes the expression $A\Rightarrow B$ be evaluated as true. This can lead to confusion for the user, who might write a specification considered correct but that is not executable by design. Ensuring that all agents can properly terminate their respective processes requires the presence of events in the ProVerif specification. The AnBx dialog offers an option to do this automatically when generating a ProVerif file. Consequently, a user would be more likely to recognise the benefits of these events instead of being potentially misled by ProVerif results.

We benchmark the overhead of the single goals feature, and we report results in Table 1. The benchmarking was conducted on an Intel(R) Xeon(R) W-2145 CPU running at 3.70 GHz, equipped with 128 GB of RAM and operating on Windows 10 64-bit. We tested OFMC 2022 with two sessions and ProVerif 2.05 for an unbounded number of sessions. We used half of the CPU cores to ensure smooth task progression and maintain a good balance in overall machine performance, and at least six cores were available to perform the single goal verification tasks in parallel. Tasks were repeated at least 20 times, and then we computed the average verification times.

With these benchmarks, one may immediately note that single-goal parallel verification is always advantageous for ProVerif’s performance. Moreover, this approach may help to detect reachability issues more easily. In all tested cases, the verification time is reduced by at least 50%.

As expected, given the verification technique used by OFMC, there is an overhead in almost all cases. While the most evident convenience lies in clearly indicating in the results which goal is failing, the advantage of parallel single-goal verification is that all goals can be checked instead of halting at the first failing one. In percentage terms, the large discrepancies between parallel single and all-goal verification times are usually due to OFMC stopping at the first failing goal in the all-goals verification scenario.

As a reference, performing single-goal verification manually would introduce significant overhead, requiring the user to launch each task individually. In the worst-case scenario, tasks would run sequentially; at best, extra time would be needed to enter each command and execute them as background processes. This manual approach, when employing the command line, also results in reduced visualisation of verification results and less control over running tasks, as it relies on the operating system’s task manager rather than the IDE’s dedicated task manager.

5.2.4. Java Code Generation and Run of Dockerised Applications

The AnBx Compiler can generate Java code from an AnBx specification, and the IDE can coordinate the execution of the distributed application using an automatically generated Ant file. In the most basic setting, the application will run using the localhost interface; however, recent developments in the compiler have extended its features to allow for the generation of Dockerised distributed Java code. Docker is a platform that enables developers to automate the deployment of applications inside lightweight, portable containers. Each agent’s code can now run on different machines, which allows for greater flexibility and scalability. Furthermore, the IDE can execute this Dockerised Java in just a few steps, streamlining the process for users.

When the export to Java (Docker) option is selected, the call to the compiler is followed by several Docker commands that manage the lifecycle of the application containers. These commands are as follows:

• docker compose lastBuildFile down: This command stops and removes the containers defined in the specified Docker Compose file, which represents the last built project. This ensures that any previously running instances of the application are halted before starting a new one.

• docker container prune: This command removes all stopped containers, helping to free up system resources and reduce clutter in the Docker environment.

• docker network prune: This command cleans up unused networks, ensuring that only necessary connections are maintained within the Docker ecosystem.

• docker compose currentBuildFile up: This command starts the containers defined in the current Docker Compose file, effectively launching the application in its new environment.

Here, lastBuildFile and currentBuildFile refer to YAML Docker Compose files that are tied to the last and currently built Docker projects, respectively.

Essentially, this sequence of commands stops previous containers, deletes unused containers and networks from the disk, and runs the container of interest. This approach ensures that no other AnBx-related container interferes with the workflow.

5.2.5. Console Output and Logging

At the bottom of any tool dialog (e.g., Figure 9), users can choose to run the next process in a new console. This feature helps to separate the outputs of different tasks, providing a clearer view of the unfolding results. This option leverages standard Eclipse consoles, which can be selected like any other through the console view’s toolbar menu. The consoles are numbered and have their own stream processing, ensuring that the output from one console does not interfere with that of another.

To interpret console output at a glance, we colour it according to pre-defined regular expressions. For example, a detected attack is coloured red, while the absence of an attack on a given protocol or goal is represented in green, and undecidability is indicated with an orange output. The policy applies to all tools printing to an AnBx IDE console and can be deactivated in the configuration window.

To facilitate output analysis, we can go beyond merely compartmentalising it into several consoles by saving it in dedicated log files with another option. These log files are named after the protocol, a runtime timestamp, and export options when relevant. Each log file is located in a folder named after the tool that generated the output, making retrieval straightforward. Users can then launch an entire suite of tasks and later perform statistical analyses on the logs.

From a research perspective, these two options are invaluable when comparing multiple prototypes for runtime, correctness, etc. They also help in building a database of case studies for protocols verified as secure or subject to interesting attacks.

5.2.6. Displaying Verification Results in an Eclipse View

With multiple tasks running and reaching conclusions concurrently, we help the user by providing a clear and concise summary of these results. To achieve this, we use a dedicated Eclipse view of the verification results, which details, in a collapsible tree view, for each protocol by file name, which goals succeeded in green, which goalsfailed in red, and which goals are deemed undecidable in orange.

The targeted goals are colour-coded, session-annotated, and sorted with the failing ones first. The user also has the option to sort the list of protocols alphabetically, enable a scroll lock (similarly to a console), or clear the list. An example is shown in Figure 10.

With this integrated view, there is no need to look in detail at the console output or scroll through long blocks of information to understand the current status. For ProVerif, the view displays precise extracts of the output, making it easily searchable when more detail is required.

5.2.7. Scheduling with Priorities and Task Manager

As users launch many tasks, the order of execution needs to be considered for productivity. The tasks are organised in a queue, and we implement a priority policy for the waiting tasks.

A user may want to experiment with some light verification or generation while a more time-consuming task is running. Our approach is to move lighter tasks up the queue, thereby avoiding the need to wait for the heavier ones to complete. We have implemented a priority queue as detailed in Algorithm 1: the compiling tasks are executed first, followed by OFMC verification with one session, then ProVerif, and finally OFMC with multiple sessions. Tasks with the same priority are executed in a First-In, First-Out (FIFO) fashion.

Algorithm 1: Task Scheduling with Priority Queue

To provide better control and visualisation of the running and enqueued tasks, we have also included a task manager. A button for this feature is added to the console’s toolbar menu and becomes active when tasks are running. This provides a view for each task, displaying which console it has been running in, how long it has been running, whether it is waiting to start, and what its exact command line is, as presented in Figure 11. Users can also select any or all of the tasks and terminate them via a dedicated button.

If a task is killed, this fact is reported in the console next to its running time. This feature can be particularly useful, for example, when console outputs are logged.

The maximum number of concurrent tasks can be set in the configuration window of the AnBx IDE plug-in. If this number increases, new concurrent tasks can start if any are enqueued; however, no running tasks will be interrupted if it decreases. By default, it is set to a minimum of four and the number of available logical CPU cores.

Setting a maximum number of concurrent threads is particularly useful when verifying protocols goal by goal, typically with the -singlegoals option. Launching parallel processes to quickly obtain intermediate results for each goal can be very resource-intensive. Thus, one can verify several goals in parallel without consuming all resources by trying to verify all of them at once.

In the same spirit of saving resources, a global timeout in minutes can be set for the running tasks. After this time elapses, a given task will be terminated in the same manner as it would be via the task manager. The default value is 0, which disables the timeout. This feature brings convenience when launching large tasks on a cluster to avoid hogging shared resources.

5.2.8. Attack Trace Reconstruction

We also enabled in the IDE the AnBx Compiler feature, which allows one to reconstruct OFMC attack traces back into AnB and to generate a Java implementation of a given trace. The IDE automates the intermediate steps necessary for the reconstruction. When Reconstruct OFMC Attack Trace is checked, the following steps ensue:

• The AnBx protocol is exported to AnB.

• OFMC is executed on the generated AnB.

• If an attack is found, the compiler is called again on the AnBx protocol, using the trace for interpretation.

After this last step, the reconstructed AnB narration of the attack is created, and a Java implementation will also be generated if the export is set to Java. The attack narration can also be printed as ExecNarr, which serves as an Intermediate Format for the concrete implementation of the attack.

With this, in addition to a UI for existing protocols, the user can see concrete results in Java emerging from an abstract attack trace, as well as a trace reconstruction expressed in AnB. This all happens without the user having to worry about intermediate steps, thereby providing both abstract and concrete attack artefacts within the same window with just a few clicks. This is the second visualisation option the IDE offers to complement the Eclipse view previously mentioned in Section 5.2.6.

5.3. Environment Customisation and Other Functionalities

There are several options for the customisation of the environment that can improve the user experience. Configuration options are available in the AnBx IDE, accessible via the AnBx Tools→Configuration menu in Eclipse. The configuration window allows users to specify paths for tool executables, configuration files, and working directories, with an automatic checking process to ensure these paths are valid and accessible. The IDE also checks file system permissions to prevent issues during operation, which can be disabled if users encounter false positives. Additionally, the window provides links for downloading tools and accessing documentation, facilitating a smooth user experience.

Finally, the IDE tracks the versions of AnBxC, OFMC, and ProVerif, offering automatic update checks and links for manual updates to ensure users have the latest software versions. In the same dialog, the user can set the maximum number of parallel threads, the timeout value, and colouring options for the console output, as already discussed in Section 5.2.5 and Section 5.2.7.

Finally, to complement and support the global user experience, we include access to documentation and help. It points to the respective tools’ webpages and tutorials, including our own step-by-step learning tasks, with instructions (https://paolo.science/anbxtutorial/, accessed on 20 November 2024) both for IDE and command line uses, and the IDE update site (https://www.dais.unive.it/~modesti/anbx/ide/, accessed on 20 November 2024).

6. Evaluation

In our evaluation strategy, we firstly focus on overcoming core challenges and barriers to the adoption of formal methods, such as complexity, accessibility, and usability, in light of how the IDE simplifies the use of verification tools. Secondly, we conduct user evaluations to assess the tool’s effectiveness and user satisfaction, gathering feedback from users in an educational setting. Those reviews added to usage statistics provide empirical evidence of the IDE’s adoption, supporting claims of its practical impact made in Section 6.1.

In Section 5, we already considered performance metrics, particularly regarding single-goal versus all-goal verification times (Section 5.2.3), to demonstrate the IDE’s efficiency improvements in cryptographic protocol verification tasks. Additionally, we have shown how our IDE helps users avoid common cryptographic misconceptions, such as those related to key usage and encryption mechanisms, by offering intelligent editing features that provide immediate feedback and guidance (Section 5.1).

6.1. Addressing Core Challenges for Formal Methods Adoption

We detail here how the AnBx IDE addresses core concerns presented in Section 2.1 to make formal method tools more accessible, as advocated in [14,15,20,48].

1. Complexity: The IDE simplifies the use of complex tools that can be employed to formalise models through high-level and standard languages. The user experience (UX) of the IDE is designed to allow the manipulation of tools without requiring an in-depth understanding of the underlying theories or the precise workings of each tool. Overall, the IDE reduces the usability barrier and facilitates the work of novice users who are unfamiliar with formal method tools and techniques, with general editing support (Section 5.1).

2. Limited Tool Integration: We identify and integrate relevant state-of-the-art tools, providing the user with the option to run all of them from a single protocol standpoint, achieving an end-to-end workflow. This aligns with the demand for the consolidation of existing tools and methods [14].

3. Unfamiliar Interfaces: We integrate several tools that have different and very specific command-line interfaces. The IDE offers a uniform access point to these tools in a common Eclipse environment for consistency, limiting back-and-forth actions and making them more accessible to the public without hindering more specialised usage.

4. Interpretability of Results: Several features of the IDE are designed to improve the way tool results are presented to the user, making them easier to interpret: console colouring (Section 5.2.5), verification result views (Section 5.2.6), single-goal handling (Section 5.2.3), and attack trace reconstruction (Section 5.2.8).

5. Scalability Issues: By supporting two verification tools, we can overcome some individual limitations and provide comparative results for a finer understanding of verification. The task manager, scheduler, concurrent threads cap, and timeout (Section 5.2.7) help to prevent resource exhaustion and confusion with numerous running tasks.

6. Limited Documentation: We provide immediate access to documentation about the tools, reducing the need to search for it (Figure 9). Overall, the UX of the IDE minimises the need to consult documentation in order to perform tasks.

In summary, by incorporating user-friendly features such as editing support, automated error reporting, and intuitive workflows, the AnBx IDE addresses core concerns raised in [14] (Section 2.1) to make formal method tools more accessible, enabling a broader user base in the field of the design and analysis of security protocols and their implementation.

6.2. User Evaluation

To assess the potential benefits of our IDE in monitoring the effectiveness of our teaching activities, we surveyed a group of Cybersecurity students at Teesside University between 2023 and 2024 about their experience using the environment and associated tools. We invited 51 students that we identified as having potentially used the toolkit at some point in their studies at our university and received responses from 35 of them (response rate: 68.8%): 30 postgraduate and 5 undergraduate students, comprising 8 female and 27 male participants. It should be noted that almost all individuals in this sample differ from those who participated in the assessment of cryptographic misconceptions (Section 2.3). However, the postgraduate students’ backgrounds are similar to those previously discussed, while the undergraduate participants included a mix of home and international students.

The survey was structured into sections to capture participants’ experiences with the AnBx tools and their technical backgrounds. It employed a five-point Likert scale [78,79] for most questions, allowing participants to rate the usefulness of different functionalities and their own technical proficiency. The following areas were covered:

• Operating system usage;

• Types of projects where the tools were used;

• Usefulness of specific IDE functionalities;

• Overall ratings of the IDE (functionality, stability, performance, usability);

• Importance of the tools in completing their projects;

• Frequency of usage;

• Technical background in computing, programming, cybersecurity, cryptography, and formal/mathematical methods for security.

In addition to these structured questions, we asked about participants’ interest in using specific tools in the future. We also provided open-ended questions that allowed them to give more detailed feedback on their experiences and suggestions for improvement.

We used LimeSurvey [80] to collect the responses, and in all cases, the survey was administered at least one month after they had received their grades, allowing for a more objective evaluation of the IDE’s usefulness.

Here is an overview of the results. While reading the results, it should be considered that the option Never used this function has not been discounted from the calculation of how useful the participants found the features.

• Operating System Usage Multiple responses were allowed. The majority of participants used Windows (94.29%), with a small proportion using Linux (14.29%) or MacOS (8.57%).

• Project Types Most participants used the IDE and supported tools for their MSc projects (60%), while 31.43% used it for advanced practice activities, a project-based module taken by MSc students. The remaining participants employed it for other university work (e.g., lab activities and other projects).

• IDE Functionality Participants rated several functionalities, with the following response options: Very useful, Somewhat useful, Not useful, Not useful at all, and Never used this function. The results show that:

  • 68.57% found the visualisation and editing of AnBx/AnB files Very useful, 17.14% Somewhat useful, 11.43% Never used this function.

  • 54.29% found the same functionality Very useful for ProVerif files, 17.14% Somewhat useful, with 25.71% reporting never using it.

  • The generation of Java code with the AnBx Compiler was highly appreciated, with 88.57% finding it Very useful, with just 2.86% having never used it.

  • The generation of AnB and ProVerif files also had high utility, with 82.86% and 60% of participants respectively, rating it Very useful. Again, the Never used this function was higher for ProVerif (22.86%) than AnB (5.71%).

  • 77.14% found Very useful the IDE support for running the generated Java code, with just 8.57% not having used the feature.

• Verification Tasks Verification tasks were among the most common features utilised by the sampled population.

  • 62.86% found OFMC verification of AnB files Very useful, and 22.86% found it Somewhat useful. 5.71% Never used this function.

  • 40% found ProVerif verification Very useful, with 31.43% finding it Somewhat useful. 22.86% Never used this function.

  • Single goal generation for ProVerif and AnB files has been described as useful for those who used the functionality, though it had lower usage compared to other features: 40% Very useful for ProVerif, 51.43% for AnB. 22.86% Never used this function for AnB, 37.14% for ProVerif.

• Logging, Task Monitoring, and Configuration These features attracted high interests and they were considered overall very useful.

  • Tool output logging was considered Very useful by 71.43% of respondents, as it allows to archive results for further analysis. 8.57% Never used this function.

  • Monitoring task progress (verification, code generation) was rated Very useful by 74.29%, with only 5.71% never using this functionality.

  • Configuring code generation parameters and concurrent task numbers was also appreciated, with 71.43% finding configuration Very useful. 8.57% Never used this function.

• General Tool Rating Overall, participants rated the AnBx IDE highly in terms of user experience. The options for the responses were: Very good, Good, Acceptable, Poor, and Very poor.

  • Functionality: 57.14% rated it Very good, 37.14% Good.

  • Stability: 40% rated it Very good, and 48.57% Good.

  • Performance: 57.14% found the performance Very good, and 34.29% rated it Good.

  • Usability: 45.71% rated usability Very good, and 40% Good.

• Importance of Tools in participants’ activities We also asked how important the tools were in order to complete the technical part of their projects or activities. The options offered for the responses were:

  • 65.71% of students considered the tools Very important for completing their projects, and 20% rated them Important.

  • Regarding usage frequency, 57.14% used the tools Most of the time, and 22.86% used them Often during their projects.

• Technical Background For the self-assessment of technical skills, we offered the following options: High, Moderately high, Average, Low, and None. The results showed that:

  • 48.57% rated themselves Moderately high in computing, 28.57% Average and 22.86% High.

  • 40% rated themselves Average in programming, with 25.71% having low programming skills. Only 8.57% rated themselves High.

  • 51.43% rated themselves Moderately high in cybersecurity, with 31.43% having High proficiency.

  • Cryptography knowledge was more varied: 14.29% High, 31.43% Moderately high, and 42.86% Average.

  • Formal/mathematical methods for security were less familiar, with only 17.14% having High proficiency, 28.57% Moderately high, 37.14% Average and 11.43% reporting no experience.

The survey results demonstrate that the AnBx tools and IDE are regarded as highly useful, especially for Java code generation and AnBx file manipulation. Participants appreciated the ability to monitor tasks and configure verification processes, highlighting the importance of these features for security protocol development. Windows was the dominant operating system used, and the tools were primarily employed for MSc projects and advanced practice.

The average general feedback on functionality, performance, and usability was largely positive (90%), but the fact that the Very Good and Good ratings are evenly split indicates that some improvements may be considered to enhance further the user experience.

Some results were surprising, particularly from the self-assessment survey. More than a quarter of the students described their programming skills as low at the master’s level, and few claimed high proficiency. In contrast, they reported having more knowledge of cryptography and formal methods than of programming. The self-assessment for general cybersecurity was also very favourable, with more than 80% indicating they had High or Moderately high mastery. Being enrolled in a security-related course likely contributed to their feeling of familiarity with security and verification concepts.

Although obtained by inquiring similar student populations, there are discrepancies between the self-assessment and the results from the knowledge survey detailed in Section 2.3. These discrepancies highlight a lack of concrete experience with subtle security issues, which student projects are designed to begin addressing. Given these misconceptions, user assistance was crucial, explaining why a large majority rated the IDE as an essential tool for completing their activities.

Notably, all the students surveyed in this evaluation who used the toolkit in individual master’s projects successfully completed their assessment with an average mark of 67/100, which is substantially in line with the results achieved by their peers undertaking other master’s projects. However, it is not possible to perform a quantitative evaluation, as projects are very different in nature, and we cannot directly compare our findings with similar activities conducted using different methodologies. Moreover, for pedagogical reasons, we could not enforce the use of particular tools on students, as their selection was part of the project proposal. The students played a leading role in choosing a particular technology, akin to real-world scenarios. We provided guidance but allowed them the freedom to reflect on alternative solutions.

All other students included in the sample also successfully completed their assessments, but their results were either pass/fail, or the specific mark was not significantly affected by the use of the tools.

The diverse technical backgrounds and varying levels of proficiency in cryptography and formal methods suggest that the IDE could support users with different levels of expertise, possibly through more guided tutorials or enhanced error messages. By addressing these aspects, the IDE can continue to effectively support both novice and advanced users in security protocol development.

Moreover, considering comments and discussions with the students, we understand that there is room to enhance usability, and based on this feedback, we fixed some bugs and improved the overall user experience.

Looking ahead, more than two-thirds of the participants stated that they would definitely use the toolkit if applicable to their future projects. None responded that they would probably not or definitely not use it in such settings.

6.3. Usage Statistics

To look beyond the individuals we surveyed, we also examined the Eclipse Marketplace statistics, synthesised in Figure 12. The first preliminary version of the tool was published in November 2017, so the data range from 2018 to October 2024. We observe a significant installation rate, around 100 installations per year. This demonstrates that this IDE has generated interest for years, attracting a broader community than just our group and the survey participants. It should be noted that the Eclipse Marketplace is not the only place where the installation process can begin, as it is also possible to install the plug-in directly from the distribution/update website run by the authors.

We also have information about the downloads of platform-specific back-end tools used by the IDE for the period from June 2021 to October 2024, broken down by operating system: Windows (509 downloads, 72%), Linux (103 downloads, 14.5%), and macOS (97 downloads, 13.5%). Anecdotally, we have evidence of downloads from different countries such as Germany, Poland, the United Kingdom, the United States, China, Italy, France, Spain, Russia, India, Bulgaria, and Denmark, among others.

6.4. Assumptions and Limitations

The analysis and evaluation of the IDE for security protocol development were based on the following assumptions. First, we assumed that users, primarily postgraduate cybersecurity students, would have a basic knowledge of applied cryptography and, more generally, of security concepts, enabling them to engage with simple formal verification methods. This was tested through the initial knowledge survey (Section 2.3) and user evaluation (Section 6.2, technical background). We also assumed that users’ cryptographic misconceptions, identified in Section 2.3, could be addressed through hands-on interaction with the IDE’s verification and error-handling features. This, indirectly, relies on the accuracy of self-assessment surveys in capturing users’ perceptions of the IDE’s usability and educational impact (Section 6.2).

In terms of generalising the results, we assumed that these findings could extend to professional contexts where formal methods are applied. Finally, our analysis was limited to specific tools, namely OFMC and ProVerif, as representative examples of automated symbolic verification for security protocols.

7. Related Work

The development of fully fledged Integrated Development Environments tailored for formal methods is not a new concept. Our contribution focuses on practicality for lowering the adoption barrier of formal methods, as promoted by Kulik et al. [15]. This is exemplified by works like Leino et al., who present an IDE [48] for the Dafny [81] language, verifier, and proof assistant. The authors find, as we do, that feedback on the specification and verification results is particularly valuable.

Other examples of IDEs for formal methods tools include the Eclipse plug-in SpinRCP [82] for the Spin model checker [83], which, on top of editing support, allows users to run verification and simulation tasks, with graphical visualisation and textual exportation of simulation output. A VSCode IDE [84] exists for the Prototype Verification System [85] used in avionics, with support for the evaluation of executable specifications and the visualisation of proof trees.

However, when it comes to security protocols, such comprehensive environments are much rarer, and keeping them up to date is challenging. While some existing tools offer partial support, particularly at the level of editing security protocol notations like AnB and ProVerif, the availability of IDEs that fully integrate verification and make results more user-friendly and interpretable is limited. As per the criteria we derived from [14,15,20] in Section 2.1, we summarise some contributions below.

Regarding complexity, simple AnB-like notations receive support from extensions or standalone editors. For example, syntax highlighting is provided for Emacs, Notepad++, Sublime Text, and TextMate via the OFMC distribution. ProVerif and Tamarin also have modes for Emacs and Vim, shipped with their respective distributions. Another project, MetaCP [86], allows for the graphical editing of protocols in an AnB style on a dedicated website and offers export options to Tamarin, ProVerif, LaTeX, or C++. The Kant specification language [87], which uses an AnB notation, has a dedicated extension for VSCode, supporting parsing, highlighting, and semantic validation. Moreover, SPAN [88,89] is a security protocol animator tool for AVISPA [90] supporting HLPSL and CAS+ specifications. CAS+ is a light evolution of CASRUL [91], a language in the AnB style.

On tool integration limitations, some editors offer the option to run the underlying tool directly from them, such as a Vim mode for ProVerif [92], which supports ProVerif editing, as well as launching and stopping tasks. It includes similar features for other formal languages, though the ProVerif part has not been updated since 2021. A Sublime Text plug-in [93] can also run tasks for Tamarin as a workflow aid, last updated in 2020.

To leverage simple, popular, and widely used interfaces, Malladi and Blanchet supplied a minimal web interface [94] to load protocols and launch verification tasks, and Nicolas and Cheval developed a ProVerif extension for VS Code [95]. This extension is in sync with the current grammar of ProVerif as of 2024 and only provides syntax highlighting. Kant [87], being integrated into a VSCode environment, is also in a position to reach a wide audience. A different approach is taken by SPAN [88] which uses a custom GUI and provides a virtual machine with all the required back-end tools pre-installed.

For the interpretability of results, a dedicated editor with highlighting named OFMC-GUI [96] exists, which can launch OFMC and display an attack trace as an easily readable sequence chart, but it has been unmaintained since 2020. A standalone ProVerif editor [97] has also been implemented in Python, providing highlighting, error reporting, an outline, and a verification summary. However, it has not seen releases since 2013. On a similar level of abstraction as ProVerif, Tamarin [98] can express its attack traces in the form of a graph of states violating security constraints.

As these tools usually focus on one language only, choosing different formalisms and levels of abstraction to better suit a broad range of problems is more complicated and requires multiple toolsets.

Access to documentation is also limited, often requiring users to read terminal output or visit the tool’s webpage. While necessary for detailed work requiring comprehensive tutorials and examples, quick GUI-assisted documentation retrieval is usually absent from these contributions.

It appears that other tools in the literature often stop short of offering comprehensive support for tasks from editing to verification and interpretation of results, in a popular Eclipse environment for security protocols. The AnBx IDE integrates the entire process of modelling, verification, and implementation of security protocols in a way that makes the tools’ output more accessible and understandable. This includes advanced features such as console output colouring, task management, and result visualisation, which help users better interpret complex verification outcomes. This interpretation is a common challenge among users unfamiliar with the underlying formal models.

To our knowledge, the AnBx IDE is currently the only editor that supports the entire workflow of editing, verification, implementation, and code generation for AnBx, OFMC AnB, and ProVerif notations. We support two main back-end tools and formalisms, and the IDE parses and logs their outputs for user visualisation and analysis. Additionally, documentation is immediately available, and the latest supported versions are advertised to users to allow them to benefit from the most recent tool features. A detailed user evaluation is also rare for security protocol handling in IDEs, an aspect that we cover in this paper.

8. Conclusions and Future Work

In this paper, we introduce an Integrated Development Environment (IDE) specifically designed to support the formal development, verification, and implementation of security protocols. This research provides significant outcomes for both practical and educational applications.

First, the IDE’s intuitive interface integrates formal verification tools with features like error-checking and visual feedback, making formal methods more accessible. It reduces the traditionally steep learning curve associated with formal verification [14,15], enabling even non-expert users to engage in secure and effective protocol design.

Second, by incorporating the AnB notation, AnBx Compiler, OFMC, and ProVerif tools within a single environment, the IDE streamlines the workflow. This automation reduces the complexity and time needed for protocol verification, allowing both developers and students to focus on design accuracy without dealing with low-level configuration tasks.

For students and early-career professionals, the AnBx IDE and its support documentation can also be a valuable educational support tool. It simplifies the formalisation of security protocols and promotes a deeper understanding of cybersecurity principles. By clarifying common cryptographic misconceptions, the IDE helps learners develop secure protocol design skills.

Additionally, with its built-in support at each stage of development, the IDE promotes a proactive approach to cybersecurity, potentially reducing the risks associated with the deployment of vulnerable protocols. Practitioners who aim to incorporate formal verification into the software lifecycle may streamline the process in practical contexts.

In summary, this research outcome bridges the gap between theoretical formal methods and practical, accessible tools, addressing challenges highlighted in the literature, such as complexity, limited tool integration, unfamiliar interfaces, interpretability of results, scalability issues, and sparse documentation. The IDE’s effectiveness demonstrates that these barriers to formal verification can be lowered.

Although the IDE currently integrates tools like OFMC and ProVerif, its flexible approach makes it adaptable to other formal languages, verifiers, and IDEs. This adaptability means that core features like task automation, result interpretation, and error handling could be implemented across a broader spectrum of formal methods applications, enhancing the IDE’s relevance.

The IDE was developed using the popular Eclipse developer platform, supporting a wide range of programming languages, both mainstream and domain-specific. This approach enhances the tool’s applicability beyond our educational community, and the IDE has been distributed through the Eclipse Marketplace to maximise accessibility.

Adding new languages and tools to the IDE, Tamarin [10,98] for example, would be an interesting way forward. As time and reviews go on, we plan to continue adding quality-of-life features and extend our toolset’s reach.

Other future work may include evaluating how effectively various languages for security protocol specification capture and support the designer’s mental models. This assessment could help identify more precise ways to reduce errors and misconceptions.

Author Contributions

Conceptualisation, R.G. and P.M.; Data curation, R.G. and P.M.; Formal analysis, R.G. and P.M.; Investigation, R.G. and P.M.; Methodology, R.G. and P.M.; Project administration, R.G. and P.M.; Software, R.G. and P.M.; Supervision, P.M.; Validation, R.G. and P.M.; Visualisation, R.G. and P.M.; Writing—original draft, R.G. and P.M.; Writing—review & editing, R.G. and P.M. All authors have read and agreed to the published version of the manuscript.

Data Availability Statement

The AnBx IDE is available at https://www.dais.unive.it/~modesti/anbx/ide/ (accessed on 20 November 2024). The original contributions presented in this study are included in the article. Further inquiries can be directed to the corresponding authors.

Acknowledgments

The authors express their gratitude to Leo Freitas for engaging in constructive discussions, Sebastian Mödersheim for his support with OFMC, and Bruno Blanchet and Vincent Cheval for their support with ProVerif. They also thank the users, particularly the students of Teesside University, for their feedback and suggestions regarding the AnBx IDE and related tools.

Conflicts of Interest

The authors declare no conflicts of interest.

Footnotes

Disclaimer/Publisher’s Note: The statements, opinions and data contained in all publications are solely those of the individual author(s) and contributor(s) and not of MDPI and/or the editor(s). MDPI and/or the editor(s) disclaim responsibility for any injury to people or property resulting from any ideas, methods, instructions or products referred to in the content.

Figures and Table

Figure 1. AnBx Protocol example.

Figure 2. AnB Protocol example.

Figure 3. AnBx compiler back-end (adapted from [25]).

Figure 4. Model driven development with the AnBx IDE (---- manual ― automatic).

Figure 5. Control and visualisation over the modelling and verification process with the AnBx IDE (---- IDE features ― workflow).

Figure 6. Tracking declarations with ProVerif scoping.

Figure 7. Error message and quick fix.

Figure 8. Auth and Verifiers checking.

Figure 9. AnBxC dialog.

Figure 10. View of verification results.

Figure 11. Task manager window.

Figure 12. Eclipse Marketplace statistics for the AnBx IDE (January 2018–October 2024).

Table 1

Comparison of verification times (for typed models) in seconds and variation between single-goal and all-goal verification for OFMC and ProVerif.

Protocol	Goals/Attacks	OFMC (2 Sessions)			ProVerif (Unlimited S.)
		all	sgl	Δ%	all	sgl	Δ%
Carlsen [66,67]	3/0	5.64	6.07	7.62	0.090	0.032	−64.44
H530 [67,68]	2/2	16.05	19.14	19.25	0.257	0.081	−68.48
IKEv2DS [67,69]	4/0	32.86	34.78	5.84	2.774	0.980	−64.67
ISO5Pass [67,70]	3/2	1.22	23.25	1805.74	0.337	0.093	−72.40
ISOCCF3PassMutual [67,71]	2/0	3.47	4.19	20.75	0.042	0.021	−50.00
NSL [67,72]	2/0	0.78	0.81	3.85	0.062	0.028	−54.84
NSPK [67,73]	4/4	0.32	0.88	175.00	0.077	0.027	−64.94
Otway-Rees [67,74]	3/0	16.78	17.38	3.58	0.116	0.038	−64.24
TLS [67,75]	3/0	70.24	68.69	−2.21	0.504	0.068	−85.51
Woo-Lam 92 [67,76]	3/1	266.57	325.21	22.00	8.329	2.401	−71.17
Yahalom [67,77]	6/1	2.38	4.28	79.83	0.131	0.030	−77.10

all—All-goal verification time; sgl—Parallel single-goal verification time; Δ%—Difference in verification time (%): $100\ast (sgl-all)/all$.

References

1. Vanhoef, M.; Piessens, F. Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017; Dallas, TX, USA, 30 October–3 November 2017; Thuraisingham, B.; Evans, D.; Malkin, T.; Xu, D. ACM: New York, NY, USA, 2017; pp. 1313-1328. [DOI: https://dx.doi.org/10.1145/3133956.3134027]

2. Cassidy, S. Diagnosis of the OpenSSL Heartbleed Bug. 2014; Available online: https://www.seancassidy.me/diagnosis-of-the-openssl-heartbleed-bug.html (accessed on 20 November 2024).

3. Fogel, B.; Farmer, S.; Alkofahi, H.; Skjellum, A.; Hafiz, M. POODLEs, More POODLEs, FREAK Attacks Too: How Server Administrators Responded to Three Serious Web Vulnerabilities. Engineering Secure Software and Systems; Springer International Publishing: Berlin/Heidelberg, Germany, 2016; pp. 122-137. [DOI: https://dx.doi.org/10.1007/978-3-319-30806-7_8]

4. Alashwali, E.S.; Rasmussen, K. What’s in a Downgrade? A Taxonomy of Downgrade Attacks in the TLS Protocol and Application Protocols Using TLS. Security and Privacy in Communication Networks; Springer International Publishing: Berlin/Heidelberg, Germany, 2018; pp. 468-487. [DOI: https://dx.doi.org/10.1007/978-3-030-01704-0_27]

5. Cremers, C.; Horvat, M.; Scott, S.; van der Merwe, T. Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication. Proceedings of the 2016 IEEE Symposium on Security and Privacy (SP); San Jose, CA, USA, 22–26 May 2016; IEEE: Piscataway, NJ, USA, 2016; [DOI: https://dx.doi.org/10.1109/sp.2016.35]

6. Bhargavan, K.; Blanchet, B.; Kobeissi, N. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. Proceedings of the 2017 IEEE Symposium on Security and Privacy, SP 2017; San Jose, CA, USA, 22–26 May 2017; IEEE Computer Society: Washington, DC, USA, 2017; pp. 483-502. [DOI: https://dx.doi.org/10.1109/SP.2017.26]

7. Blanchet, B. Composition theorems for cryptoverif and application to TLS 1.3. Proceedings of the 2018 IEEE 31st Computer Security Foundations Symposium (CSF); Oxford, UK, 9–12 July 2018; pp. 16-30. [DOI: https://dx.doi.org/10.1109/csf.2018.00009]

8. Cohn-Gordon, K.; Cremers, C.; Dowling, B.; Garratt, L.; Stebila, D. A Formal Security Analysis of the Signal Messaging Protocol. J. Cryptol.; 2020; 33, pp. 1914-1983. [DOI: https://dx.doi.org/10.1007/s00145-020-09360-1]

9. Blanchet, B. An efficient cryptographic protocol verifier based on Prolog rules. Proceedings of the Computer Security Foundations Workshop; Cape Breton, NS, Canada, 11–13 June 2001; IEEE: Piscataway, NJ, USA, IEEE Computer Society: Washington, DC, USA, 2001; 0082.

10. Meier, S.; Schmidt, B.; Cremers, C.; Basin, D.A. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. Proceedings of the Computer Aided Verification—25th International Conference, CAV 2013; Saint Petersburg, Russia, 13–19 July 2013; Proceedings; Lecture Notes in Computer Science Sharygina, N.; Veith, H. Springer: Berlin/Heidelberg, Germany, 2013; Volume 8044, pp. 696-701. [DOI: https://dx.doi.org/10.1007/978-3-642-39799-8_48]

11. Basin, D.; Mödersheim, S.; Viganò, L. OFMC: A symbolic model checker for security protocols. Int. J. Inf. Secur.; 2005; 4, pp. 181-208. [DOI: https://dx.doi.org/10.1007/s10207-004-0055-7]

12. Dark, M.; Belcher, S.; Bishop, M.; Ngambeki, I. Practice, Practice, Practice.. Secure Programmer!. Proceedings of the 19th Colloquium for Information System Security Education; Las Vegas, NV, USA, 15–17 June 2015.

13. NIST. CVE-2020-13777; NIST: Gaithersburg, MD, USA, 2020; Available online: https://nvd.nist.gov/vuln/detail/CVE-2020-13777/ (accessed on 20 November 2024).

14. Garavel, H.; ter Beek, M.H.; van de Pol, J. The 2020 Expert Survey on Formal Methods. Proceedings of the Formal Methods for Industrial Critical Systems—25th International Conference, FMICS 2020; Vienna, Austria, 2–3 September 2020; Proceedings; Lecture Notes in Computer Science ter Beek, M.H.; Nickovic, D. Springer: Berlin/Heidelberg, Germany, 2020; Volume 12327, pp. 3-69. [DOI: https://dx.doi.org/10.1007/978-3-030-58298-2_1]

15. Kulik, T.; Dongol, B.; Larsen, P.G.; Macedo, H.D.; Schneider, S.; Tran-Jørgensen, P.W.V.; Woodcock, J. A Survey of Practical Formal Methods for Security. Form. Asp. Comput.; 2022; 34, pp. 1-39. [DOI: https://dx.doi.org/10.1145/3522582]

16. Dolev, D.; Yao, A. On the Security of Public-Key Protocols. IEEE Trans. Inf. Theory; 1983; 2, pp. 198-208. [DOI: https://dx.doi.org/10.1109/TIT.1983.1056650]

17. Sommerville, I. Software Engineering; 9th ed. Addison-Wesley: San Francisco, CA, USA, 2010.

18. Bugliesi, M.; Focardi, R. Language Based Secure Communication. Proceedings of the Computer Security Foundations Symposium, 2008, CSF’08, IEEE 21st; Pittsburgh, PA, USA, 23–25 June 2008; pp. 3-16. [DOI: https://dx.doi.org/10.1109/csf.2008.17]

19. Avalle, M.; Pironti, A.; Sisto, R. Formal verification of security protocol implementations: A survey. Form. Asp. Comput.; 2014; 26, pp. 99-123. [DOI: https://dx.doi.org/10.1007/s00165-012-0269-9]

20. Davis, J.A.; Clark, M.; Cofer, D.; Fifarek, A.; Hinchman, J.; Hoffman, J.; Hulbert, B.; Miller, S.P.; Wagner, L. Study on the Barriers to the Industrial Adoption of Formal Methods. Formal Methods for Industrial Critical Systems; Springer: Berlin/Heidelberg, Germany, 2013; pp. 63-77. [DOI: https://dx.doi.org/10.1007/978-3-642-41010-9_5]

21. Skevoulis, S.; Makarov, V. Integrating Formal Methods Tools Into Undergraduate Computer Science Curriculum. Proceedings of the Frontiers in Education, 36th Annual Conference; Aarhus, Denmark, 24–8 June 2002; IEEE: Piscataway, NJ, USA, 2006; pp. 1-6. [DOI: https://dx.doi.org/10.1109/fie.2006.322570]

22. Scheurer, T. Formal Methods: The Problem Is Education. Computer Safety, Reliability and Security; Springer: Berlin/Heidelberg, Germany, 2000; pp. 198-210. [DOI: https://dx.doi.org/10.1007/3-540-40891-6_18]

23. Pomorova, O.; Lysenko, S. Formal and Intelligent Methods for Security and Resilience: Education and Training Issues. Inf. Secur. Int. J.; 2016; 35, pp. 133-150. [DOI: https://dx.doi.org/10.11610/isij.3507]

24. Avalle, M.; Pironti, A.; Pozza, D.; Sisto, R. JavaSPI: A Framework for Security Protocol Implementation. Int. J. Secur. Softw. Eng.; 2011; 2, pp. 34-48. [DOI: https://dx.doi.org/10.4018/jsse.2011100103]

25. Modesti, P. AnBx: Automatic Generation and Verification of Security Protocols Implementations. Proceedings of the 8th International Symposium on Foundations & Practice of Security; Clermont-Ferrand, France, 26–28 October 2015; LNCS Springer: Berlin/Heidelberg, Germany, 2015; Volume 9482, pp. 156-173. [DOI: https://dx.doi.org/10.1007/978-3-319-30303-1_10]

26. Almousa, O.; Mödersheim, S.; Viganò, L. Alice and Bob: Reconciling Formal Models and Implementation. Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday; Lecture Notes in Computer Science Bodei, C.; Ferrari, G.L.; Priami, C. Springer International Publishing: Berlin/Heidelberg, Germany, 2015; Volume 9465, pp. 66-85. [DOI: https://dx.doi.org/10.1007/978-3-319-25527-9_7]

27. Wing, D.J.J. Lightweight formal methods. An Invitation to Formal Methods; Saiedian, H. IEEE Computer: Washington, DC, USA, 1996; [DOI: https://dx.doi.org/10.1007/3-540-45251-6_1]

28. Zamansky, A.; Spichkova, M.; Rodríguez-Navas, G.; Herrmann, P.; Blech, J.O. Towards Classification of Lightweight Formal Methods. Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2018; Funchal, Portugal, 23–24 March 2018; Damiani, E.; Spanoudakis, G.; Maciaszek, L.A. SciTePress: Setúbal, Portugal, 2018; pp. 305-313. [DOI: https://dx.doi.org/10.5220/0006770803050313]

29. Brucker, A.D.; Marmsoler, D. Teaching Formal Methods in Application Domains: A Case Study in Computer and Network Security. Formal Methods Teaching; Springer Nature: Cham, Switzerland, 2024; pp. 124-140. [DOI: https://dx.doi.org/10.1007/978-3-031-71379-8_8]

30. Brambilla, M.; Cabot, J.; Wimmer, M. Model-Driven Software Engineering in Practice; 2nd ed. Synthesis Lectures on Software Engineering Morgan & Claypool Publishers: San Rafael, CA, USA, 2017; [DOI: https://dx.doi.org/10.2200/S00751ED2V01Y201701SWE004]

31. Nguyen, P.H.; Kramer, M.E.; Klein, J.; Traon, Y.L. An extensive systematic review on the Model-Driven Development of secure systems. Inf. Softw. Technol.; 2015; 68, pp. 62-81. [DOI: https://dx.doi.org/10.1016/j.infsof.2015.08.006]

32. Garcia, R.; and Modesti, P. An IDE for the Design, Verification and Implementation of Security Protocols. Proceedings of the International Symposium on Software Reliability Engineering Workshops, ISSRE; Toulouse, France, 23–26 October 2017; pp. 157-163. [DOI: https://dx.doi.org/10.1109/ISSREW.2017.69]

33. Bettini, L. Implementing Domain-Specific Languages with Xtext and Xtend; Packt Publishing Ltd.: Birmingham, UK, 2016.

34. Eclipse Community. XText Documentation; Eclipse Community: Ottawa, ON, Canada, Available online: http://eclipse.org/Xtext/documentation/ (accessed on 20 November 2024).

35. Mödersheim, S. Algebraic Properties in Alice & Bob Notation. Proceedings of the Forth International Conference on Availability, Reliability and Security, ARES 2009; Fukuoka, Japan, 16–19 March 2009; IEEE Computer Society: Washington, DC, USA, 2009; pp. 433-440. [DOI: https://dx.doi.org/10.1109/ARES.2009.95]

36. Bugliesi, M.; Calzavara, S.; Mödersheim, S.; Modesti, P. Security protocol specification and verification with AnBx. J. Inf. Secur. Appl.; 2016; 30, pp. 46-63. [DOI: https://dx.doi.org/10.1016/j.jisa.2016.05.004]

37. Blanchet, B.; Cheval, V.; Cortier, V. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. Proceedings of the 43RD IEEE Symposium on Security and Privacy (S&P’22); San Francisco, CA, USA, 22–26 May 2022; [DOI: https://dx.doi.org/10.1109/sp46214.2022.9833653]

38. Shaukat, R.; Shahoor, A.; Urooj, A. Probing into code analysis tools: A comparison of C# supporting static code analyzers. Proceedings of the 2018 15th International Bhurban Conference on Applied Sciences and Technology (IBCAST); Islamabad, Pakistan, 9–13 January 2018; pp. 455-464. [DOI: https://dx.doi.org/10.1109/IBCAST.2018.8312264]

39. Fetaji, M.; Loskovska, S.; Fetaji, B.; Ebibi, M. Combining Virtual Learning Environment and Integrated Development Environment to Enhance e-Learning. Proceedings of the 2007 29th International Conference on Information Technology Interfaces; Dubrovnik, Croatia, 25–28 June 2007; pp. 319-324. [DOI: https://dx.doi.org/10.1109/ITI.2007.4283790]

40. Broy, M.; Brucker, A.; Fantechi, A.; Gleirscher, M.; Havelund, K.; Kuppe, M.A.; Mendes, A.; Platzer, A.; Ringert, J.; Sullivan, A. Does Every Computer Scientist Need to Know Formal Methods?. Form. Asp. Comput.; 2024; accepted [DOI: https://dx.doi.org/10.1145/3670795]

41. Gleirscher, M.; Marmsoler, D. Formal methods in dependable systems engineering: A survey of professionals from Europe and North America. Empir. Softw. Eng.; 2020; 25, pp. 4473-4546. [DOI: https://dx.doi.org/10.1007/s10664-020-09836-5]

42. Spivey, J.M. Z Notation—A Reference Manual; 2nd ed. Prentice Hall International Series in Computer Science Prentice Hall: Hoboken, NJ, USA, 1992.

43. Wadsworth, B.J. Piaget’s Theory of Cognitive and Affective Development: Foundations of Constructivism; Longman Publishing: Harlow, UK, 1996.

44. Bruner, J.S. The Process of Education; Harvard University Press: Cambridge, MA, USA, 2009; [DOI: https://dx.doi.org/10.2307/j.ctvk12qst]

45. Raimondo, M.; Marrone, S.; Bernardi, S.; Palladino, A. Demonstrating the Necessity of Model Generation in Security Protocol Verification. Proceedings of the 28th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2023; Sinaia, Romania, 12–15 September 2023; IEEE: Piscataway, NJ, USA, 2023; pp. 1-8. [DOI: https://dx.doi.org/10.1109/ETFA54631.2023.10275424]

46. Paulson, L.C.; Nipkow, T.; Wenzel, M. From LCF to Isabelle/HOL. Form. Asp. Comput.; 2019; 31, pp. 675-698. [DOI: https://dx.doi.org/10.1007/s00165-019-00492-1]

47. Abadi, M.; Needham, R. Prudent engineering practice for cryptographic protocols. Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, 1994 Proceedings; Oakland, CA, USA, 16–18 May 1994; pp. 122-136. [DOI: https://dx.doi.org/10.1109/32.481513]

48. Leino, K.R.M.; Wüstholz, V. The Dafny Integrated Development Environment. Proceedings of the 1st Workshop on Formal Integrated Development Environment, F-IDE 2014; Grenoble, France, 6 April 2014; EPTCS Dubois, C.; Giannakopoulou, D.; Méry, D. Open Publishing Association: The Hague, The Netherlands, 2014; Volume 149, pp. 3-15. [DOI: https://dx.doi.org/10.4204/EPTCS.149.2]

49. Unwin, A.; Hofmann, H. GUI and Command-line—Conflict or Synergy?. Proceedings of the 31st Symposium on the Interface: Models, Predictions, and Computing; Schaumburg, IL, USA, 9–12 June 1999; Computing Science and Statistics Berk, K.; Pourahmadi, M. Interface Foundation of North America: Fairfax Station, VA, USA, 1999; pp. 246-253.

50. Tabassum, M.; Watson, S.; Lipford, H.R. Comparing Educational Approaches to Secure programming: Tool vs. TA. Proceedings of the Thirteenth Symposium on Usable Privacy and Security, SOUPS 2017; Santa Clara, CA, USA, 12–14 July 2017; USENIX Association: Berkeley, CA, USA, 2017.

51. Kuusinen, K. Software Developers as Users: Developer Experience of a Cross-Platform Integrated Development Environment. Proceedings of the Product-Focused Software Process Improvement—16th International Conference, PROFES 2015; Bolzano, Italy, 2–4 December 2015; Proceedings; Lecture Notes in Computer Science Abrahamsson, P.; Corral, L.; Oivo, M.; Russo, B. Springer: Berlin/Heidelberg, Germany, 2015; Volume 9459, pp. 546-552. [DOI: https://dx.doi.org/10.1007/978-3-319-26844-6_40]

52. Lindmeier, A.; Mühling, A. Keeping secrets: K-12 students’ understanding of cryptography. Proceedings of the WiPSCE ’20: Workshop in Primary and Secondary Computing Education; Essen, Germany, 28–30 October 2020; Brinda, T.; Armoni, M. ACM: New York, NY, USA, 2020; pp. 14:1-14:10. [DOI: https://dx.doi.org/10.1145/3421590.3421630]

53. Geels, J. Ordinary Users Do Not Understand Digital Signatures. Proceedings of the 13th Nordic Conference on Human-Computer Interaction, NordiCHI 2024; Uppsala, Sweden, 13–16 October 2024; ACM: New York, NY, USA, 2024; pp. 66:1-66:15. [DOI: https://dx.doi.org/10.1145/3679318.3685402]

54. Braga, A.M.; Dahab, R.; Antunes, N.; Laranjeiro, N.; Vieira, M. Understanding How to Use Static Analysis Tools for Detecting Cryptography Misuse in Software. IEEE Trans. Reliab.; 2019; 68, pp. 1384-1403. [DOI: https://dx.doi.org/10.1109/TR.2019.2937214]

55. Gleirscher, M.; Foster, S.; Woodcock, J. New Opportunities for Integrated Formal Methods. ACM Comput. Surv.; 2020; 52, pp. 117:1-117:36. [DOI: https://dx.doi.org/10.1145/3357231]

56. van Glabbeek, R.J.; Höfner, P.; van der Wal, D. Analysing AWN-Specifications Using mCRL2 (Extended Abstract). Proceedings of the Integrated Formal Methods—14th International Conference, IFM 2018; Maynooth, Ireland, 5–7 September 2018; Proceedings; Lecture Notes in Computer Science Furia, C.A.; Winter, K. Springer: Berlin/Heidelberg, Germany, 2018; Volume 11023, pp. 398-418. [DOI: https://dx.doi.org/10.1007/978-3-319-98938-9_23]

57. Runge, T.; Schaefer, I.; Cleophas, L.; Thüm, T.; Kourie, D.G.; Watson, B.W. Tool Support for Correctness-by-Construction. Proceedings of the Software Engineering 2021, Fachtagung des GI-Fachbereichs Softwaretechnik; Braunschweig, Germany, 22–26 February 2021; LNI Koziolek, A.; Schaefer, I.; Seidl, C. Gesellschaft für Informatik e.V.: Bonn, Germany, 2021; Volume P-310, pp. 93-94. [DOI: https://dx.doi.org/10.18420/SE2021_34]

58. Fares, E.; Bodeveix, J.; Filali, M. Correct Pattern-Based Development Through Refinements and Weakest Preconditions Calculus. Proceedings of the Formal Aspects of Component Software—20th International Conference, FACS 2024; Milan, Italy, 9–10 September 2024; Proceedings; Lecture Notes in Computer Science Marmsoler, D.; Sun, M. Springer: Berlin/Heidelberg, Germany, 2024; Volume 15189, pp. 59-78. [DOI: https://dx.doi.org/10.1007/978-3-031-71261-6_4]

59. Bonfanti, S.; Carissoni, M.; Gargantini, A.; Mashkoor, A. Asm2C++: A Tool for Code Generation from Abstract State Machines to Arduino. Proceedings of the NASA Formal Methods—9th International Symposium, NFM 2017; Moffett Field, CA, USA, 16–18 May 2017; Proceedings; Lecture Notes in Computer Science Barrett, C.W.; Davies, M.D.; Kahsai, T. Springer: Berlin/Heidelberg, Germany, 2017; Volume 10227, pp. 295-301. [DOI: https://dx.doi.org/10.1007/978-3-319-57288-8_21]

60. Lowe, G. A Hierarchy of Authentication Specifications. Proceedings of the CSFW’97; Rockport, MA, USA, 10–12 June 1997; IEEE Computer Society Press: Washington, DC, USA, 1997; pp. 31-43.

61. Galeotti, J.P.; Furia, C.A.; May, E.; Fraser, G.; Zeller, A. Automating Full Functional Verification of Programs with Loops. arXiv; 2014; [DOI: https://dx.doi.org/10.48550/arxiv.1407.5286] arXiv: 1407.5286

62. Barbosa, M.; Barthe, G.; Bhargavan, K.; Blanchet, B.; Cremers, C.; Liao, K.; Parno, B. SoK: Computer-Aided Cryptography. Proceedings of the 42nd IEEE Symposium on Security and Privacy, SP 2021; San Francisco, CA, USA, 24–27 May 2021; IEEE: Piscataway, NJ, USA, 2021; pp. 777-795. [DOI: https://dx.doi.org/10.1109/SP40001.2021.00008]

63. AVISPA Team. AVISPA v1.0 User Manual. Available online: https://people.rennes.inria.fr/Thomas.Genet/Crypt/AVISPA_manual.pdf (accessed on 20 November 2024).

64. Delaune, S.; Hirschi, L. A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. J. Log. Algebr. Methods Program.; 2017; 87, pp. 127-144. [DOI: https://dx.doi.org/10.1016/j.jlamp.2016.10.005]

65. Blanchet, B.; Smyth, B.; Cheval, V. ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial; Inria: Paris, France, 2023.

66. Carlsen, U. Optimal Privacy and Authentication on a Portable Communications System. ACM SIGOPS Oper. Syst. Rev.; 1994; 28, pp. 16-23. [DOI: https://dx.doi.org/10.1145/182110.182112]

67. Mödersheim, S. OFMC Distribution and Tutorials. Available online: https://www2.compute.dtu.dk/~samo/ (accessed on 20 November 2024).

68. ITU-T Recommendation H.530: Symmetric Security Procedures for H.510 (Mobility for H.323 Multimedia Systems and Services); H.323 Forum: San Ramon, CA, USA, 2002.

69. Kaufman, C. Internet Key Exchange (IKEv2) Protocol; Technical Report Internet Engineering Task Force (IETF): Fremont, CA, USA, 2005.

70. ISO/IEC 9798-2:2008 Information Technology—Security Techniques—Entity Authentication—Part 2: Mechanisms Using Symmetric Encipherment Algorithms; 3rd ed. International Organization for Standardization: Geneva, Switzerland, 2008.

71. ISO/IEC 9798-4:1999 Information Technology—Security Techniques—Entity Authentication—Part 3: Mechanisms Using a Cryptographic Check Function; 2nd ed. International Organization for Standardization: Geneva, Switzerland, 1999.

72. Lowe, G. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. Softw. Concepts Tools; 1996; 17, pp. 93-102. [DOI: https://dx.doi.org/10.1007/3-540-61042-1_43]

73. Needham, R.M.; Schroeder, M.D. Using Encryption for Authentication in Large Networks of Computers. Commun. ACM; 1978; 21, pp. 993-999. [DOI: https://dx.doi.org/10.1145/359657.359659]

74. Otway, D.J.; Rees, O. Efficient and Timely Mutual Authentication. ACM SIGOPS Oper. Syst. Rev.; 1987; 21, pp. 8-10. [DOI: https://dx.doi.org/10.1145/24592.24594]

75. Paulson, L.C. Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur.; 1999; 2, pp. 332-351. [DOI: https://dx.doi.org/10.1145/322510.322530]

76. Woo, T.Y.; Lam, S.S. Authentication for distributed systems. Computer; 1992; 25, pp. 39-52. [DOI: https://dx.doi.org/10.1109/2.108052]

77. Paulson, L.C. The Yahalom Protocol. Proceedings of the Security Protocols: 7th International Workshop; Cambridge, UK, 19–21 April 1999; Proceedings 7 Springer: Berlin/Heidelberg, Germany, 2000; pp. 78-84. [DOI: https://dx.doi.org/10.1007/10720107_11]

78. Likert, R. A technique for the measurement of attitudes. Arch. Psychol.; 1932; 140, pp. 5-55.

79. Clark, L.A.; Watson, D. Constructing validity: New developments in creating objective measuring instruments. Psychol. Assess.; 2019; 31, 1412. [DOI: https://dx.doi.org/10.1037/pas0000626]

80. LimeSurvey Team. LimeSurvey: An Open Source Survey Tool. 2024; Available online: https://www.limesurvey.org (accessed on 14 October 2024).

81. Leino, K.R.M. Dafny: An Automatic Program Verifier for Functional Correctness. Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning—16th International Conference, LPAR-16; Dakar, Senegal, 25 April–1 May 2010; Revised Selected Papers; Lecture Notes in Computer Science Clarke, E.M.; Voronkov, A. Springer: Berlin/Heidelberg, Germany, 2010; Volume 6355, pp. 348-370. [DOI: https://dx.doi.org/10.1007/978-3-642-17511-4_20]

82. Brezocnik, Z.; Vlaovic, B.; Vreze, A. SpinRCP: The eclipse rich client platform integrated development environment for the spin model checker. Proceedings of the 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings; San Jose, CA, USA, 21–23 July 2014; Rungta, N.; Tkachuk, O. ACM: New York, NY, USA, 2014; pp. 125-128. [DOI: https://dx.doi.org/10.1145/2632362.2632380]

83. Holzmann, G.J. The SPIN Model Checker—Primer and Reference Manual; Addison-Wesley: Boston, MA, USA, 2004.

84. Masci, P.; Muñoz, C.A. An Integrated Development Environment for the Prototype Verification System. Proceedings of the Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019; Porto, Portugal, 7 October 2019; EPTCS Monahan, R.; Prevosto, V.; Proença, J. Open Publishing Association: The Hague, The Netherlands, 2019; Volume 310, pp. 35-49. [DOI: https://dx.doi.org/10.4204/EPTCS.310.5]

85. Owre, S.; Rushby, J.M.; Shankar, N. PVS: A Prototype Verification System. Proceedings of the Automated Deduction—CADE-11, 11th International Conference on Automated Deduction; Saratoga Springs, NY, USA, 15–18 June 1992; Proceedings; Lecture Notes in Computer Science Kapur, D. Springer: Berlin/Heidelberg, Germany, 1992; Volume 607, pp. 748-752. [DOI: https://dx.doi.org/10.1007/3-540-55602-8_217]

86. Metere, R.; Arnaboldi, L. MetaCP: Cryptographic Protocol Design Tool for Formal Verification. arXiv; 2021; [DOI: https://dx.doi.org/10.48550/arxiv.2105.09150] arXiv: 2105.09150

87. Braghin, C.; Lilli, M.; Riccobene, E.; Baba, M. Kant: A Domain-Specific Language for Modeling Security Protocols. Proceedings of the 12th International Conference on Model-Based Software and Systems Engineering, MODELSWARD 2024; Rome, Italy, 21–23 February 2024; Mayo, F.J.D.; Pires, L.F.; Seidewitz, E. SciTePress: Setúbal, Portugal, 2024; pp. 62-73. [DOI: https://dx.doi.org/10.5220/0012386400003645]

88. Glouche, Y.; Genet, T.; Heen, O.; Courtay, O. A security protocol animator tool for AVISPA. Proceedings of the ARTIST2 Workshop on Security Specification and Verification of Embedded Systems; Pisa, Italy, 18 May 2006; pp. 1-7.

89. Boichut, Y.; Genet, T.; Glouche, Y.; Heen, O. Using animation to improve formal specifications of security protocols. Proceedings of the 2nd Conference on Security in Network Architectures and Information Systems (SARSSI 2007); Annecy, France, 12–15 June 2007; pp. 169-182.

90. Armando, A.; Basin, D.; Boichut, Y.; Chevalier, Y.; Compagna, L.; Cuéllar, J.; Drielsma, P.H.; Héam, P.C.; Kouchnarenko, O.; Mantovani, J. et al. The AVISPA tool for the automated validation of internet security protocols and applications. Proceedings of the Computer Aided Verification; Edinburgh, UK, 6–10 July 2005; Springer: Berlin/Heidelberg, Germany, 2005; pp. 281-285. [DOI: https://dx.doi.org/10.1007/11513988_27]

91. Rusinowitch, M. Automated analysis of security protocols. Proceedings of the 12th International Workshop on Functional and Constraint Logic Programming, WFLP 2003, in Connection with RDP’03, Federated Conference on Rewriting, Deduction and Programming; Boulder, CO, USA, 14 July 2003; Electronic Notes in Theoretical Computer Science Brim, L.; Grumberg, O. Elsevier: Amsterdam, The Netherlands, 2003; Volume 86, pp. 12-15. [DOI: https://dx.doi.org/10.1016/S1571-0661(04)80690-X]

92. Lifepillar. Vim Mode for Formal Languages; GitHub: San Francisco, CA, USA, 2024; Available online: https://github.com/lifepillar/vim-formal-package (accessed on 20 November 2024).

93. Whitefield, J.; Ralf Sasse, B.F. Sublime Text 3 plug-in for Tamarin. Available online: https://github.com/tamarin-prover/editor-sublime (accessed on 20 November 2024).

94. Malladi, S.; Blanchet, B. ProVerif Web Interface; Inria: Paris, France, 2024; Available online: http://proverif20.paris.inria.fr/index.php (accessed on 20 November 2024).

95. Nicolas, G.; Cheval, V. ProVerif Syntax Highlighting for VS Code; Inria: Paris, France, 2024; Available online: https://marketplace.visualstudio.com/items?itemName=georgio.proverif-vscode (accessed on 20 November 2024).

96. Edvardsson, Ú.J.; Hoffmann, V.J.L. OFMC-GUI; GitHub: San Francisco, CA, USA, 2024; Available online: https://github.com/ulfur88/OFMC-GUI (accessed on 20 November 2024).

97. de Ruiter, J. ProVerif Editor; Inria: Paris, France, 2024; Available online: https://proverifeditor.sourceforge.net/ (accessed on 20 November 2024).

98. Schmidt, B.; Meier, S.; Cremers, C.; Basin, D. Automated analysis of Diffie–Hellman protocols and advanced security properties. Proceedings of the Computer Security Foundations Symposium (CSF), 2012 IEEE 25th; Cambridge, MA, USA, 25–27 June 2012; IEEE: Piscataway, NJ, USA, 2012; pp. 78-94. [DOI: https://dx.doi.org/10.1109/csf.2012.25]