InforLorV4, PascalFrancis, Corpus, bibRecord, 000570

An NP decision procedure for protocol insecurity with XOR

Identifieur interne : 000570 ( PascalFrancis/Corpus ); précédent : 000569; suivant : 000571

An NP decision procedure for protocol insecurity with XOR

Auteurs : Yannick Chevalier ; Ralf Küsters ; Michaël Rusinowitch ; Mathieu Turuani

Source :

Theoretical computer science [ 0304-3975 ] ; 2005.

RBID : Pascal:05-0253621

Descripteurs français

Pascal (Inist)
- Décision, Oracle, Déduction, Vérification, Complexité, Informatique théorique, Protocole cryptographique, Protocole sécurité.

English descriptors

KwdEn :
- Complexity, Computer theory, Cryptographic protocol, Decision, Deduction, Oracle, Security protocol, Verification.

Abstract

We provide a method for deciding the insecurity of cryptographic protocols in the presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we obtain that protocol insecurity is in NP for an intruder that can exploit the properties of the exclusive or (XOR) operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in PTIME. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 0304-3975`
A02	`01`			`@0 TCSCDI`
A03		`1`		`@0 Theor. comput. sci.`
A05				`@2 338`
A06				`@2 1-3`
A08	`01`	`1`	`ENG`	`@1 An NP decision procedure for protocol insecurity with XOR`
A11	`01`	`1`		`@1 CHEVALIER (Yannick)`
A11	`02`	`1`		`@1 KÜSTERS (Ralf)`
A11	`03`	`1`		`@1 RUSINOWITCH (Michaël)`
A11	`04`	`1`		`@1 TURUANI (Mathieu)`
A14	`01`			`@1 LORIA-INRIA-Université Henri Poincaré @2 54506 Vandoeuvre-les-Nancy @3 FRA @Z 1 aut. @Z 3 aut. @Z 4 aut.`
A14	`02`			`@1 Christian-Albrechts-Universität zu Kiel, Inst. f. Informatik @2 24098 Kiel @3 DEU @Z 2 aut.`
A20				`@1 247-274`
A21				`@1 2005`
A23	`01`			`@0 ENG`
A43	`01`			`@1 INIST @2 17243 @5 354000124638820090`
A44				`@0 0000 @1 © 2005 INIST-CNRS. All rights reserved.`
A45				`@0 30 ref.`
A47	`01`	`1`		`@0 05-0253621`
A60				`@1 P`
A61				`@0 A`
A64	`01`	`1`		`@0 Theoretical computer science`
A66	`01`			`@0 NLD`
C01	`01`		`ENG`	@0 We provide a method for deciding the insecurity of cryptographic protocols in the presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we obtain that protocol insecurity is in NP for an intruder that can exploit the properties of the exclusive or (XOR) operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in PTIME. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).
C02	`01`	`X`		`@0 001D04A04E`
C02	`02`	`X`		`@0 001D02A05`
C03	`01`	`X`	`FRE`	`@0 Décision @5 17`
C03	`01`	`X`	`ENG`	`@0 Decision @5 17`
C03	`01`	`X`	`SPA`	`@0 Decisión @5 17`
C03	`02`	`X`	`FRE`	`@0 Oracle @5 19`
C03	`02`	`X`	`ENG`	`@0 Oracle @5 19`
C03	`03`	`X`	`FRE`	`@0 Déduction @5 20`
C03	`03`	`X`	`ENG`	`@0 Deduction @5 20`
C03	`03`	`X`	`SPA`	`@0 Deducción @5 20`
C03	`04`	`X`	`FRE`	`@0 Vérification @5 21`
C03	`04`	`X`	`ENG`	`@0 Verification @5 21`
C03	`04`	`X`	`SPA`	`@0 Verificación @5 21`
C03	`05`	`X`	`FRE`	`@0 Complexité @5 22`
C03	`05`	`X`	`ENG`	`@0 Complexity @5 22`
C03	`05`	`X`	`SPA`	`@0 Complejidad @5 22`
C03	`06`	`X`	`FRE`	`@0 Informatique théorique @5 23`
C03	`06`	`X`	`ENG`	`@0 Computer theory @5 23`
C03	`06`	`X`	`SPA`	`@0 Informática teórica @5 23`
C03	`07`	`X`	`FRE`	`@0 Protocole cryptographique @4 CD @5 96`
C03	`07`	`X`	`ENG`	`@0 Cryptographic protocol @4 CD @5 96`
C03	`08`	`X`	`FRE`	`@0 Protocole sécurité @4 CD @5 97`
C03	`08`	`X`	`ENG`	`@0 Security protocol @4 CD @5 97`
N21				`@1 178`

Format Inist (serveur)

NO :	PASCAL 05-0253621 INIST
ET :	An NP decision procedure for protocol insecurity with XOR
AU :	CHEVALIER (Yannick); KÜSTERS (Ralf); RUSINOWITCH (Michaël); TURUANI (Mathieu)
AF :	LORIA-INRIA-Université Henri Poincaré/54506 Vandoeuvre-les-Nancy/France (1 aut., 3 aut., 4 aut.); Christian-Albrechts-Universität zu Kiel, Inst. f. Informatik/24098 Kiel/Allemagne (2 aut.)
DT :	Publication en série; Niveau analytique
SO :	Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2005; Vol. 338; No. 1-3; Pp. 247-274; Bibl. 30 ref.
LA :	Anglais
EA :	We provide a method for deciding the insecurity of cryptographic protocols in the presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we obtain that protocol insecurity is in NP for an intruder that can exploit the properties of the exclusive or (XOR) operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in PTIME. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).
CC :	001D04A04E; 001D02A05
FD :	Décision; Oracle; Déduction; Vérification; Complexité; Informatique théorique; Protocole cryptographique; Protocole sécurité
ED :	Decision; Oracle; Deduction; Verification; Complexity; Computer theory; Cryptographic protocol; Security protocol
SD :	Decisión; Deducción; Verificación; Complejidad; Informática teórica
LO :	INIST-17243.354000124638820090
ID :	05-0253621

Links to Exploration step

Pascal:05-0253621

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">An NP decision procedure for protocol insecurity with XOR</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Université Henri Poincaré</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Kusters, Ralf" sort="Kusters, Ralf" uniqKey="Kusters R" first="Ralf" last="Küsters">Ralf Küsters</name>
<affiliation><inist:fA14 i1="02"><s1>Christian-Albrechts-Universität zu Kiel, Inst. f. Informatik</s1>
<s2>24098 Kiel</s2>
<s3>DEU</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Université Henri Poincaré</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Turuani, Mathieu" sort="Turuani, Mathieu" uniqKey="Turuani M" first="Mathieu" last="Turuani">Mathieu Turuani</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Université Henri Poincaré</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">05-0253621</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 05-0253621 INIST</idno>
<idno type="RBID">Pascal:05-0253621</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000570</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">An NP decision procedure for protocol insecurity with XOR</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Université Henri Poincaré</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Kusters, Ralf" sort="Kusters, Ralf" uniqKey="Kusters R" first="Ralf" last="Küsters">Ralf Küsters</name>
<affiliation><inist:fA14 i1="02"><s1>Christian-Albrechts-Universität zu Kiel, Inst. f. Informatik</s1>
<s2>24098 Kiel</s2>
<s3>DEU</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Université Henri Poincaré</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Turuani, Mathieu" sort="Turuani, Mathieu" uniqKey="Turuani M" first="Mathieu" last="Turuani">Mathieu Turuani</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Université Henri Poincaré</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date when="2005">2005</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Complexity</term>
<term>Computer theory</term>
<term>Cryptographic protocol</term>
<term>Decision</term>
<term>Deduction</term>
<term>Oracle</term>
<term>Security protocol</term>
<term>Verification</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Décision</term>
<term>Oracle</term>
<term>Déduction</term>
<term>Vérification</term>
<term>Complexité</term>
<term>Informatique théorique</term>
<term>Protocole cryptographique</term>
<term>Protocole sécurité</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We provide a method for deciding the insecurity of cryptographic protocols in the presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we obtain that protocol insecurity is in NP for an intruder that can exploit the properties of the exclusive or (XOR) operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in PTIME. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0304-3975</s0>
</fA01>
<fA02 i1="01"><s0>TCSCDI</s0>
</fA02>
<fA03 i2="1"><s0>Theor. comput. sci.</s0>
</fA03>
<fA05><s2>338</s2>
</fA05>
<fA06><s2>1-3</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>An NP decision procedure for protocol insecurity with XOR</s1>
</fA08>
<fA11 i1="01" i2="1"><s1>CHEVALIER (Yannick)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>KÜSTERS (Ralf)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>RUSINOWITCH (Michaël)</s1>
</fA11>
<fA11 i1="04" i2="1"><s1>TURUANI (Mathieu)</s1>
</fA11>
<fA14 i1="01"><s1>LORIA-INRIA-Université Henri Poincaré</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>Christian-Albrechts-Universität zu Kiel, Inst. f. Informatik</s1>
<s2>24098 Kiel</s2>
<s3>DEU</s3>
<sZ>2 aut.</sZ>
</fA14>
<fA20><s1>247-274</s1>
</fA20>
<fA21><s1>2005</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000124638820090</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2005 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>30 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>05-0253621</s0>
</fA47>
<fA60><s1>P</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64>
<fA66 i1="01"><s0>NLD</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>We provide a method for deciding the insecurity of cryptographic protocols in the presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we obtain that protocol insecurity is in NP for an intruder that can exploit the properties of the exclusive or (XOR) operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in PTIME. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D04A04E</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02A05</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Décision</s0>
<s5>17</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Decision</s0>
<s5>17</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Decisión</s0>
<s5>17</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Oracle</s0>
<s5>19</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Oracle</s0>
<s5>19</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Déduction</s0>
<s5>20</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Deduction</s0>
<s5>20</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Deducción</s0>
<s5>20</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Vérification</s0>
<s5>21</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Verification</s0>
<s5>21</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Verificación</s0>
<s5>21</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Complexité</s0>
<s5>22</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Complexity</s0>
<s5>22</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Complejidad</s0>
<s5>22</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>23</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>23</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>23</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Protocole cryptographique</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Cryptographic protocol</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Protocole sécurité</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Security protocol</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fN21><s1>178</s1>
</fN21>
</pA>
</standard>
<server><NO>PASCAL 05-0253621 INIST</NO>
<ET>An NP decision procedure for protocol insecurity with XOR</ET>
<AU>CHEVALIER (Yannick); KÜSTERS (Ralf); RUSINOWITCH (Michaël); TURUANI (Mathieu)</AU>
<AF>LORIA-INRIA-Université Henri Poincaré/54506 Vandoeuvre-les-Nancy/France (1 aut., 3 aut., 4 aut.); Christian-Albrechts-Universität zu Kiel, Inst. f. Informatik/24098 Kiel/Allemagne (2 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2005; Vol. 338; No. 1-3; Pp. 247-274; Bibl. 30 ref.</SO>
<LA>Anglais</LA>
<EA>We provide a method for deciding the insecurity of cryptographic protocols in the presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we obtain that protocol insecurity is in NP for an intruder that can exploit the properties of the exclusive or (XOR) operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in PTIME. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).</EA>
<CC>001D04A04E; 001D02A05</CC>
<FD>Décision; Oracle; Déduction; Vérification; Complexité; Informatique théorique; Protocole cryptographique; Protocole sécurité</FD>
<ED>Decision; Oracle; Deduction; Verification; Complexity; Computer theory; Cryptographic protocol; Security protocol</ED>
<SD>Decisión; Deducción; Verificación; Complejidad; Informática teórica</SD>
<LO>INIST-17243.354000124638820090</LO>
<ID>05-0253621</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000570 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000570 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:05-0253621
   |texte=   An NP decision procedure for protocol insecurity with XOR
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

An NP decision procedure for protocol insecurity with XOR

An NP decision procedure for protocol insecurity with XOR

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri