Amphiteatre Maison Jean Kuntzmann
25 novembre 2013 - 14h00
Vérification formelle des protocoles de vote et de vente aux enchères: De l'anonymat à l'équité et la vérifiabilité (Phd Defense)
par Jannik Dreier de VERIMAG
Résumé : 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.
