Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Automated Security Proofs with Sequences of Games

De
33 pages
Automated Security Proofs with Sequences of Games Bruno Blanchet and David Pointcheval CNRS, Departement d'Informatique, Ecole Normale Superieure October 2006 Bruno Blanchet, David Pointcheval Automated Security Proofs with Sequences of Games

  • computational assumptions

  • message authentication

  • security protocols

  • cryptographic protocols

  • property can

  • automated security

  • scheme

  • signature

  • produced proofs

  • hash


Voir plus Voir moins
rBnuAutomatedSecurityProofswithSequencesofGamesBrunoBlanchetandDavidPointchevalCNRS,De´partementd’Informatique,E´coleNormaleSupe´rieureolBnahcte,aDivdoPOctober2006nictehavluAotametdeSucirytrPofosiwhteSuqneecsfoaGems
rPofosforcpyotrgpaihcrptooocslTherearetwomainframeworksforanalyzingsecurityprotocols:TheDolev-Yaomodel:aformal,abstractmodel.Thecryptographicprimitivesareidealblackboxes.Theadversaryusesonlythoseprimitives.Proofscanbedoneautomatically.Thecomputationalmodel:arealisticmodel.Thecryptographicprimitivesarefunctionsonbit-strings.Theadversaryisapolynomial-timeTuringmachine.Proofsaredonemanually.Ourgoal:achieveautomaticprovabilityundertherealisticcomputationalassumptions.rBnuolBnahcte,aDivdoPnictehavluAotametdeSucirytrPofosiwhteSuqneecsfoaGems
nAuaotamitcrpvoreWehaveimplementedanautomaticproversoundinthecomputationalmodel:provessecrecypropertiesandthateventscanbeexecutedonlywithnegligibleprobability.handlesvariouscryptographicprimitives:MACs(messageauthenticationcodes),streamandblockciphers,public-keyencryption,signatures,hashfunctions,...worksforNsessionswithanactiveadversary.givesaboundontheprobabilityofanattack(exactsecurity).rBnuolBnahcte,aDivdoPnictehavluAotametdeSucirytrPofosiwhteSuqneecsfoaGems