33 Pages
English
Gain access to the library to view online
Learn more

Automated Security Proofs with Sequences of Games

-

Gain access to the library to view online
Learn more
33 Pages
English

Description

Automated Security Proofs with Sequences of Games Bruno Blanchet and David Pointcheval CNRS, Departement d'Informatique, Ecole Normale Superieure January 2008 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


Subjects

Informations

Published by
Reads 14
Language English

Exrait

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