ProVerif est un outil dédié à la vérification automatique de propriétés de sécurité des protocoles cryptographiques. Il permet de modéliser et d'analyser des protocoles pour détecter des vulnérabilités potentielles, garantissant ainsi leur robustesse face aux attaques. Utilisé dans la recherche académique et industrielle, il aide à sécuriser les communications et les échanges de données.

Cette bibliothèque fournit des outils mathématiques formalisés pour aider à la vérification d'implémentations cryptographiques. Elle permet aux développeurs et chercheurs de s'assurer que les algorithmes cryptographiques respectent des propriétés de sécurité strictes, réduisant ainsi les risques de vulnérabilités dans les systèmes critiques comme les protocoles de communication ou les infrastructures sécurisées.

Ce projet est une preuve de concept (PoC) dédiée à l'implémentation et à la comparaison de méthodes de multiplication scalaire sur des courbes de Kummer. Il inclut des scripts pour évaluer les performances de l'échelle de Montgomery et de l'échelle hybride, ainsi que des outils de vérification pour confirmer la justesse des formules mathématiques utilisées. L'objectif est d'améliorer l'efficacité des protocoles cryptographiques basés sur les isogénies.

Ce projet développe un protocole de billetterie électronique innovant permettant la création, le transfert et la vérification de billets anonymes tout en garantissant leur traçabilité et leur sécurité. Il s'appuie sur des mécanismes cryptographiques avancés pour assurer l'anonymat des utilisateurs et l'intégrité des transactions, tout en permettant des audits indépendants. Le système est conçu pour des applications nécessitant une gestion de billets sécurisée et respectueuse de la vie privée.

Le projet cv2fstar-material est un dépôt de code source contenant une extension pour l'outil CryptoVerif, qui permet de vérifier la correction et la sécurité des protocoles cryptographiques. Cette extension, développée dans le cadre d'une thèse de doctorat, permet de générer automatiquement du code sécurisé à partir de spécifications formelles, améliorant ainsi l'efficacité et la fiabilité du processus de développement de protocoles cryptographiques.

Ce projet contient des programmes permettant d'analyser et de vérifier des protocoles de cryptographie modulaire, développés dans le cadre de la rédaction de l'article [Lattice-Based Cryptanalysis of Modular Exponentiation Outsourcing Protocols](https://hal.archives-ouvertes.fr/hal-03209303). Il a été testé avec la version 9.2 de SageMath.