Sécurité des protocoles cryptographiques : décidabilité et complexité
Identifieur interne : 000915 ( Crin/Checkpoint ); précédent : 000914; suivant : 000916Sécurité des protocoles cryptographiques : décidabilité et complexité
Auteurs : Mathieu TuruaniSource :
English descriptors
Abstract
Cette thèse est centrée sur les aspects théoriques du problème de l'insécurité de protocoles. Ce problème consiste à décider si un protocole, i.e. typiquement un échange de messages entre des clients et serveurs, admet une "attaque" ou non, p.ex. l'acquisition d'un secret par un intrus. Le modèle de Dolev-Yao permet à l'intrus d'intercepter tous les messages, de les analyser, et d'en créer de nouveaux à l'aide d'opérateurs standards comme l'encryption. En revanche, l'intrus ne peut pas décrypter un message sans la clef adéquate. C'est l'hypothèse dite de "chiffrement parfait". Dans le cas général, ce problème est connu pour être indécidable. Dans un premier temps, la complexité théorique de ce problème pour un nombre fini de sessions (mais sans aucune autre contrainte) est étudiée, avec un résultat de NP-complétude. Ensuite, ce résultat est étendu de plusieurs manières. Tout d'abord, il est prouvé que ce problème est encore NP-complet quand on ajoute un opérateur xor, et surtout ses propriétés algébriques, au modèle de protocole. Ensuite, ce résultat est étendu pour couvrir les propriétés d'opérateurs basés sur les groupes abéliens comme l'exponentiation avec les propriétés de Diffie-Hellman (NP-complet). Dans le modèle précédent, l'intrus peut d'inverser un terme connu (pour le produit). Le cas où cette inversion n'est pas possible a également été considéré, pour modéliser la commutation de clefs (encore NP-complet). En outre, il est également prouvé que l'extension des protocoles ping-pong avec une propriété de commutation de clefs est aussi NP-complet (protocoles plus simples mais à nombre de sessions non borné). Enfin, le modèle initial a également été étendu de manière à fusionner le modèle de protocoles à nombre de sessions borné mais messages quelconques, et le modèle à nombre de sessions quelconques mais messages bornés (DEXP-complet). Par ailleurs, une implémentation d'une procédure de décision efficace à nombre de sessions borné dans le prototype ATSE, développé dans le cadre du projet européen AVISPA, est également décrite.
Links toward previous steps (curation, corpus...)
Links to Exploration step
CRIN:turuani03aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="-304">Sécurité des protocoles cryptographiques : décidabilité et complexité</title></titleStmt><publicationStmt><idno type="RBID">CRIN:turuani03a</idno><date when="2003" year="2003">2003</date><idno type="wicri:Area/Crin/Corpus">003C37</idno><idno type="wicri:Area/Crin/Curation">003C37</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">003C37</idno><idno type="wicri:Area/Crin/Checkpoint">000915</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000915</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Sécurité des protocoles cryptographiques : décidabilité et complexité</title><author><name sortKey="Turuani, Mathieu" sort="Turuani, Mathieu" uniqKey="Turuani M" first="Mathieu" last="Turuani">Mathieu Turuani</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>algebraic properties</term><term>complexity</term><term>cryptographic protocol</term><term>decision procedure</term><term>security</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr" wicri:score="-6275">Cette thèse est centrée sur les aspects théoriques du problème de l'insécurité de protocoles. Ce problème consiste à décider si un protocole, i.e. typiquement un échange de messages entre des clients et serveurs, admet une "attaque" ou non, p.ex. l'acquisition d'un secret par un intrus. Le modèle de Dolev-Yao permet à l'intrus d'intercepter tous les messages, de les analyser, et d'en créer de nouveaux à l'aide d'opérateurs standards comme l'encryption. En revanche, l'intrus ne peut pas décrypter un message sans la clef adéquate. C'est l'hypothèse dite de "chiffrement parfait". Dans le cas général, ce problème est connu pour être indécidable. Dans un premier temps, la complexité théorique de ce problème pour un nombre fini de sessions (mais sans aucune autre contrainte) est étudiée, avec un résultat de NP-complétude. Ensuite, ce résultat est étendu de plusieurs manières. Tout d'abord, il est prouvé que ce problème est encore NP-complet quand on ajoute un opérateur xor, et surtout ses propriétés algébriques, au modèle de protocole. Ensuite, ce résultat est étendu pour couvrir les propriétés d'opérateurs basés sur les groupes abéliens comme l'exponentiation avec les propriétés de Diffie-Hellman (NP-complet). Dans le modèle précédent, l'intrus peut d'inverser un terme connu (pour le produit). Le cas où cette inversion n'est pas possible a également été considéré, pour modéliser la commutation de clefs (encore NP-complet). En outre, il est également prouvé que l'extension des protocoles ping-pong avec une propriété de commutation de clefs est aussi NP-complet (protocoles plus simples mais à nombre de sessions non borné). Enfin, le modèle initial a également été étendu de manière à fusionner le modèle de protocoles à nombre de sessions borné mais messages quelconques, et le modèle à nombre de sessions quelconques mais messages bornés (DEXP-complet). Par ailleurs, une implémentation d'une procédure de décision efficace à nombre de sessions borné dans le prototype ATSE, développé dans le cadre du projet européen AVISPA, est également décrite.</div></front></TEI><BibTex type="phdthesis"><ref>turuani03a</ref><crinnumber>A03-T-521</crinnumber><category>9</category><equipe>CASSIS</equipe><author><e>Turuani, Mathieu</e></author><title>Sécurité des protocoles cryptographiques : décidabilité et complexité</title><school>Université Henri Poincaré</school><year>2003</year><type>Thèse d'université</type><month>Dec</month><keywords><e>cryptographic protocol</e><e>decision procedure</e><e>complexity</e><e>security</e><e>algebraic properties</e></keywords><abstract>Cette thèse est centrée sur les aspects théoriques du problème de l'insécurité de protocoles. Ce problème consiste à décider si un protocole, i.e. typiquement un échange de messages entre des clients et serveurs, admet une "attaque" ou non, p.ex. l'acquisition d'un secret par un intrus. Le modèle de Dolev-Yao permet à l'intrus d'intercepter tous les messages, de les analyser, et d'en créer de nouveaux à l'aide d'opérateurs standards comme l'encryption. En revanche, l'intrus ne peut pas décrypter un message sans la clef adéquate. C'est l'hypothèse dite de "chiffrement parfait". Dans le cas général, ce problème est connu pour être indécidable. Dans un premier temps, la complexité théorique de ce problème pour un nombre fini de sessions (mais sans aucune autre contrainte) est étudiée, avec un résultat de NP-complétude. Ensuite, ce résultat est étendu de plusieurs manières. Tout d'abord, il est prouvé que ce problème est encore NP-complet quand on ajoute un opérateur xor, et surtout ses propriétés algébriques, au modèle de protocole. Ensuite, ce résultat est étendu pour couvrir les propriétés d'opérateurs basés sur les groupes abéliens comme l'exponentiation avec les propriétés de Diffie-Hellman (NP-complet). Dans le modèle précédent, l'intrus peut d'inverser un terme connu (pour le produit). Le cas où cette inversion n'est pas possible a également été considéré, pour modéliser la commutation de clefs (encore NP-complet). En outre, il est également prouvé que l'extension des protocoles ping-pong avec une propriété de commutation de clefs est aussi NP-complet (protocoles plus simples mais à nombre de sessions non borné). Enfin, le modèle initial a également été étendu de manière à fusionner le modèle de protocoles à nombre de sessions borné mais messages quelconques, et le modèle à nombre de sessions quelconques mais messages bornés (DEXP-complet). Par ailleurs, une implémentation d'une procédure de décision efficace à nombre de sessions borné dans le prototype ATSE, développé dans le cadre du projet européen AVISPA, est également décrite.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000915 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Checkpoint/biblio.hfd -nk 000915 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Checkpoint
|type= RBID
|clé= CRIN:turuani03a
|texte= Sécurité des protocoles cryptographiques : décidabilité et complexité
}}
| This area was generated with Dilib version V0.6.33. |  |