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.

APROVER: A FRAMEWORK FOR THE DEVELOPMENT OF SECURITY PROTOCOLS / M. Lilli ; tutor: E. Riccobene ; co-supervisore: C. Braghin ; coordinatore: R. Sassi. Dipartimento di Informatica Giovanni Degli Antoni, 2024 Apr. 36. ciclo

APROVER: A FRAMEWORK FOR THE DEVELOPMENT OF SECURITY PROTOCOLS

M. Lilli
2024

Abstract

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.
17-apr-2024
Settore INF/01 - Informatica
RICCOBENE, ELVINIA MARIA
BRAGHIN, CHIARA
SASSI, ROBERTO
Doctoral Thesis
APROVER: A FRAMEWORK FOR THE DEVELOPMENT OF SECURITY PROTOCOLS / M. Lilli ; tutor: E. Riccobene ; co-supervisore: C. Braghin ; coordinatore: R. Sassi. Dipartimento di Informatica Giovanni Degli Antoni, 2024 Apr. 36. ciclo
File in questo prodotto:
File Dimensione Formato  
phd_unimi_R13088.pdf

accesso aperto

Tipologia: Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione 3.24 MB
Formato Adobe PDF
3.24 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/1039590
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact