Vérification formelle des protocoles de vote et de vente aux enchères : De l'anonymat à l'équité et la vérifiabilité

Dans cette thèse nous étudions formellement la sécurité des protocoles de vote et d’enchère en ligne. Le vote en ligne est utilisé en Estonie et dans certaines régions de la Suisse. D’autre part, les enchères en ligne sont de plus en plus populaires: eBay comptait plus de 112 millions utilisateurs actifs et plus de 350 millions d’objets à vendre en 2012, avec un chiffre d’affaires de 14 milliards de dollars. Dans ces deux applications, la sécurité est primordiale, à cause d’enjeux financiers et politiques.

Dans le cas des protocoles de vote, le secret du vote est crucial pour le libre choix des votants. Nous proposons une hiérarchie des notions de secret du vote par rapport à plusieurs niveaux de coercition, des attaques spécifiques (comme l’abstention forcé), et des votants corrompus. Nous développons également des notions généralisées pour le cas des votes pondérés (par exemple par rapport au nombre d’actions dans une société), et montrons que pour beaucoup de protocoles le cas avec plusieurs votants sous attaque se réduit au cas avec un seul votant sous attaque. Ce résultat a été obtenu grâce à un autre résultat dans le pi-calcul appliqué montrant que tout processus fini peut se décomposer de manière unique en processus premiers. Nous illustrons notre hiérarchie sur plusieurs exemples, soulignant comment elle permet d’évaluer le niveau d’anonymat d’un protocole donné.

Dans le cas des protocoles d’enchère en ligne, nous proposons aussi une hiérarchie de notions d’anonymat, et plusieurs notions d’équité et d’authentification comme la non-interférence, la non-annulation et la non-répudiation. Nous analysons ces propriétés automatiquement à l’aide de l’outil ProVerif sur trois exemples, et découvrons plusieurs faiblesses. De plus, nous proposons une définition abstraite de la vérifiabilité, et l’appliquons sur des exemples aussi bien dans le modèle calculatoire que dans le modèle symbolique en utilisant CryptoVerif et ProVerif respectivement. Nous démontrons dans le modèle calculatoire qu’un des protocoles est vérifiable, et découvrons plusieurs faiblesses sur le deuxième exemple.

Finalement nous étudions le concept d’«enchères vraiment vérifiable par les enchérisseurs», c’est-à-dire des protocoles d’enchère ou le bon déroulement peut être vérifié par un non-expert, car la sécurité est assurée par des moyens physiques, et non cryptographiques. Nous proposons deux tels protocoles, et une analyse formelle de ces protocoles avec ProVerif grâce à une modélisation symbolique des propriétés physiques.