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)

ProVerif support for VSCode

UKano: UnlinKability and ANOnymity verifier

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

Compare robustness of protocols under attack capability combinations using ProVerif

Claude Skill: extract cryptographic protocol message flow from code, RFCs, ProVerif or Tamarin models into Mermaid + ASCII sequence diagrams

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.

Post-quantum secure messaging protocol — specifications, conformance vectors, and the Rust reference implementation. ML-KEM-768 + ML-DSA-65 hybrid. Research-stage; not production-ready.

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