APROVER: A FRAMEWORK FOR THE DEVELOPMENT OF SECURITY PROTOCOLS

In the dynamic landscape of emerging technologies such as IoT and 5G, the integration of advanced cryptographic protocols becomes essential for fostering secure and data-driven communication. The reliability of crypto- graphic protocols plays a pivotal role, enabling secure communication chan- nels, privacy preservation, real-time responses, energy-efficient operations, enhanced security measures, personalised user experiences, and optimized network performance. However, a critical concern emerges due to the lim- ited presence of formalised communication protocols, posing security risks in our interconnected daily lives. The lack of formalisation can be traced back to the mathematical intricacy of formal methods languages and their complex integration into the tight development timeframes of companies. To ensure that mathematical proofs of correctness, secrecy, authentication and integrity are guaranteed through all the developing phases of security protocols, we perfuse our effort in creating a framework to close the gap between the designers’ needs and the formal methods tools. The project in- troduces APROVER, an "Automatic Protocol Verifier" designed to simplify the formal specification, verification, and development of security protocols. The initiative focuses on two main aspects: i) bridging the usability gap by developing a web UI based on a sequence diagram for message exchange and a versatile language (KANT) for power users, helping them with syn- tactic and semantic validation of their models; ii) unifying the verification methodology by creating a multi-level approach that targets both the com- munication and the internal device logic.