ProVerif-ATP - Combining ProVerif and Automated Theorem Provers for Security Protocol Verification

Formal Verification of Telegram's MTProto 2.0

ProVerif proof of concept of the Rollback attack on car keyfob (CVE-2022-37418, CVE-2022-36945 and CVE-2022-37305)

UKano: UnlinKability and ANOnymity verifier

ProVerif support for VSCode

PPCA is a lightweight, distributed, and privacy-preserving privacy-preserving collision avoidance scheme for autonomous UAVs.

Esperimenti e progetti realizzati durante il corso di Computer Security 2021/2021

Formal Verification and Requirements Traceability for the Public Key Directory Specification

Basic proverif support for VIM files.

CESA: A Chebyshev Polynomials based Efficient and Secure Access Authentication Scheme for both UE and mMTC Devices over 5G Networks

This work delves into the privacy of vehicles and their drivers. Starting from a formal model of a proposed scheme aimed at safeguarding privacy in V2X communication, it has been extended and subjected to thorough analysis of its security properties through formal verification methods. Proverif has been used for this work.

Compare robustness of protocols under attack capability combinations using ProVerif

WebAuthn API theoretical analysis using italian language and formal analysis of the library through Proverif software tool