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

TL;DR

This paper introduces an Eclipse IDE designed to make formal methods for security protocol verification more accessible and practical for users with limited formal methods experience, supported by user feedback and evaluation.

Contribution

It presents a user-friendly Eclipse IDE integrating formal verification tools and a Model-Driven Development approach to facilitate security protocol design and verification.

Findings

The IDE aids users in understanding cybersecurity concepts.

Users found the IDE helpful for completing projects.

Participants expressed willingness to reuse the toolkit.

Abstract

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, for practitioners, formal modelling and verification are often too complex and unfamiliar to be used routinely. In this paper, we present an Eclipse IDE 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.