![\"cortier\"](\"http:\/\/iww.inria.fr\/colloquium\/files\/2015\/12\/cortier.jpg\")
<\/a>De nombreux dispositifs \u00e9lectroniques visent \u00e0 am\u00e9liorer la s\u00e9curit\u00e9 des \u00e9changes sur des r\u00e9seaux ouverts comme Internet. Ces dispositifs, tels que les protocoles cryptographiques, reposent souvent sur le chiffrement des donn\u00e9es et plus g\u00e9n\u00e9ralement sur des fonctions cryptographiques. Chiffrer les donn\u00e9es sensibles est cependant loin d’\u00eatre suffisant pour assurer la s\u00e9curit\u00e9 des communications. Ainsi, les protocoles cryptographiques peuvent comporter des failles subtiles, qui ne sont r\u00e9v\u00e9l\u00e9es que plusieurs ann\u00e9es apr\u00e8s. Il est donc n\u00e9cessaire de concevoir des techniques rigoureuses pour analyser la s\u00e9curit\u00e9 de syst\u00e8mes \u00e9lectroniques comme les protocoles.<\/p>\nEst-il possible d’aller plus loin et de prouver la s\u00e9curit\u00e9 d’un syst\u00e8me, quelque soit le comportement d’adversaires malicieux ? Nous verrons dans quels cadres (ou mod\u00e8les) des preuves de s\u00e9curit\u00e9 sont possibles. Nous \u00e9voquerons ainsi les mod\u00e8les symboliques, o\u00f9 les protocoles sont repr\u00e9sent\u00e9s par des objets abstraits (comme la logique du premier ordre) et les mod\u00e8les cryptographiques, o\u00f9 les messages et les protocoles sont repr\u00e9sent\u00e9s beaucoup plus fid\u00e8lement. Les premiers offrent un cadre simplifi\u00e9, plus accessible \u00e0 la preuve tandis que les seconds offrent des garanties de s\u00e9curit\u00e9 plus fortes.<\/p>\n
Nous illustrerons nos propos avec un exemple important et controvers\u00e9 : les protocoles de vote \u00e9lectronique.<\/p>\n
V\u00e9ronique Cortier (Loria)<\/em><\/p>\n