Des développeurs de Blockstream Research ont publié libshrincs, une bibliothèque de preuve de concept en langage C implémentant WOTS+C, un composant de signature à usage unique d’un schéma Resistant aux ordinateurs quantiques conçu pour Bitcoin. La bibliothèque intègre des preuves de correction fonctionnelle vérifiées par machine et des preuves de sécurité utilisant l’outil SSProve dans Rocq, totalisant environ 19 600 lignes de code formel. L’intelligence artificielle, notamment ChatGPT et Fable, a été mobilisée pour générer une partie substantielle du code de vérification sous supervision humaine, une approche susceptible de réduire les coûts de la vérification formelle en cryptographie. Les auteurs reconnaissent néanmoins que le théorème de sécurité actuel ne fournit pas encore de borne post-quantique complète dans le modèle d’oracle aléatoire quantique, et qu’aucune revendication de déploiement en production n’est avancée.
Source: Lire l’article original
