InforLorV4, PascalFrancis, Corpus, bibRecord, 000539

Regular protocols and attacks with regular knowledge

Identifieur interne : 000539 ( PascalFrancis/Corpus ); précédent : 000538; suivant : 000540

Regular protocols and attacks with regular knowledge

Auteurs : Tomasz Truderung

Source :

Lecture notes in computer science [ 0302-9743 ] ; 2005.

RBID : Pascal:05-0355351

Descripteurs français

Pascal (Inist)
- Intelligence artificielle, Programmation logique, Déduction, Démonstration automatique, Sécurité, Automate déterministe, Automate arbre, Protocole transmission, Cryptographie, Langage rationnel, Intrus, Méthode ascendante, ..

English descriptors

KwdEn :
- Artificial intelligence, Automatic proving, Bottom up method, Cryptography, Deduction, Deterministic automaton, Intruder, Logical programming, Regular language, Safety, Transmission protocol, Tree automaton.

Abstract

We prove that, if the initial knowledge of the intruder is given by a deterministic bottom-up tree automaton, then the insecurity problem for cryptographic protocols with atomic keys for a bounded number of sessions is NP-complete. We prove also that if regural languages (given by tree automata) are used in protocol descriptions to restrict the form of messages, then the insecurity problem is NEXPTIME-complete. Furthermore, we define a class of cryptographic protocols, called regular protocols, such that the knowledge which the intruder can gain during an unlimited number of sessions of a protocol is a regular language.

Notice en format standard (ISO 2709)

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

A01	`01`	`1`		`@0 0302-9743`
A05				`@2 3632`
A08	`01`	`1`	`ENG`	`@1 Regular protocols and attacks with regular knowledge`
A09	`01`	`1`	`ENG`	`@1 CADE-20 : automated deduction : Tallinn, 22-27 July 2005`
A11	`01`	`1`		`@1 TRUDERUNG (Tomasz)`
A12	`01`	`1`		`@1 NIEUWENHUIS (Robert) @9 ed.`
A14	`01`			`@1 LORIA-INRIA-Lorraine @3 FRA @Z 1 aut.`
A14	`02`			`@1 Institute of Computer Science, Wroclaw University @3 POL @Z 1 aut.`
A20				`@1 377-391`
A21				`@1 2005`
A23	`01`			`@0 ENG`
A26	`01`			`@0 3-540-28005-7`
A43	`01`			`@1 INIST @2 16343 @5 354000124491700280`
A44				`@0 0000 @1 © 2005 INIST-CNRS. All rights reserved.`
A45				`@0 15 ref.`
A47	`01`	`1`		`@0 05-0355351`
A60				`@1 P @2 C`
A61				`@0 A`
A64	`01`	`1`		`@0 Lecture notes in computer science`
A66	`01`			`@0 DEU`
C01	`01`		`ENG`	@0 We prove that, if the initial knowledge of the intruder is given by a deterministic bottom-up tree automaton, then the insecurity problem for cryptographic protocols with atomic keys for a bounded number of sessions is NP-complete. We prove also that if regural languages (given by tree automata) are used in protocol descriptions to restrict the form of messages, then the insecurity problem is NEXPTIME-complete. Furthermore, we define a class of cryptographic protocols, called regular protocols, such that the knowledge which the intruder can gain during an unlimited number of sessions of a protocol is a regular language.
C02	`01`	`X`		`@0 001D02C02`
C03	`01`	`X`	`FRE`	`@0 Intelligence artificielle @5 01`
C03	`01`	`X`	`ENG`	`@0 Artificial intelligence @5 01`
C03	`01`	`X`	`SPA`	`@0 Inteligencia artificial @5 01`
C03	`02`	`X`	`FRE`	`@0 Programmation logique @5 02`
C03	`02`	`X`	`ENG`	`@0 Logical programming @5 02`
C03	`02`	`X`	`SPA`	`@0 Programación lógica @5 02`
C03	`03`	`X`	`FRE`	`@0 Déduction @5 03`
C03	`03`	`X`	`ENG`	`@0 Deduction @5 03`
C03	`03`	`X`	`SPA`	`@0 Deducción @5 03`
C03	`04`	`X`	`FRE`	`@0 Démonstration automatique @5 04`
C03	`04`	`X`	`ENG`	`@0 Automatic proving @5 04`
C03	`04`	`X`	`SPA`	`@0 Demostración automática @5 04`
C03	`05`	`X`	`FRE`	`@0 Sécurité @5 06`
C03	`05`	`X`	`ENG`	`@0 Safety @5 06`
C03	`05`	`X`	`SPA`	`@0 Seguridad @5 06`
C03	`06`	`X`	`FRE`	`@0 Automate déterministe @5 07`
C03	`06`	`X`	`ENG`	`@0 Deterministic automaton @5 07`
C03	`06`	`X`	`SPA`	`@0 Autómata determinista @5 07`
C03	`07`	`X`	`FRE`	`@0 Automate arbre @5 08`
C03	`07`	`X`	`ENG`	`@0 Tree automaton @5 08`
C03	`07`	`X`	`SPA`	`@0 Autómata árbol @5 08`
C03	`08`	`X`	`FRE`	`@0 Protocole transmission @5 09`
C03	`08`	`X`	`ENG`	`@0 Transmission protocol @5 09`
C03	`08`	`X`	`SPA`	`@0 Protocolo transmisión @5 09`
C03	`09`	`X`	`FRE`	`@0 Cryptographie @5 10`
C03	`09`	`X`	`ENG`	`@0 Cryptography @5 10`
C03	`09`	`X`	`SPA`	`@0 Criptografía @5 10`
C03	`10`	`X`	`FRE`	`@0 Langage rationnel @5 11`
C03	`10`	`X`	`ENG`	`@0 Regular language @5 11`
C03	`10`	`X`	`SPA`	`@0 Lenguaje racional @5 11`
C03	`11`	`X`	`FRE`	`@0 Intrus @5 18`
C03	`11`	`X`	`ENG`	`@0 Intruder @5 18`
C03	`11`	`X`	`SPA`	`@0 Intruso @5 18`
C03	`12`	`X`	`FRE`	`@0 Méthode ascendante @5 23`
C03	`12`	`X`	`ENG`	`@0 Bottom up method @5 23`
C03	`12`	`X`	`SPA`	`@0 Método ascendente @5 23`
C03	`13`	`X`	`FRE`	`@0 . @4 INC @5 82`
N21				`@1 248`
N44	`01`			`@1 OTO`
N82				`@1 OTO`

A30	`01`	`1`	`ENG`	`@1 International conference on automated deduction @2 20 @3 Tallinn EST @4 2005-07-22`

Format Inist (serveur)

NO :	PASCAL 05-0355351 INIST
ET :	Regular protocols and attacks with regular knowledge
AU :	TRUDERUNG (Tomasz); NIEUWENHUIS (Robert)
AF :	LORIA-INRIA-Lorraine/France (1 aut.); Institute of Computer Science, Wroclaw University/Pologne (1 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2005; Vol. 3632; Pp. 377-391; Bibl. 15 ref.
LA :	Anglais
EA :	We prove that, if the initial knowledge of the intruder is given by a deterministic bottom-up tree automaton, then the insecurity problem for cryptographic protocols with atomic keys for a bounded number of sessions is NP-complete. We prove also that if regural languages (given by tree automata) are used in protocol descriptions to restrict the form of messages, then the insecurity problem is NEXPTIME-complete. Furthermore, we define a class of cryptographic protocols, called regular protocols, such that the knowledge which the intruder can gain during an unlimited number of sessions of a protocol is a regular language.
CC :	001D02C02
FD :	Intelligence artificielle; Programmation logique; Déduction; Démonstration automatique; Sécurité; Automate déterministe; Automate arbre; Protocole transmission; Cryptographie; Langage rationnel; Intrus; Méthode ascendante; .
ED :	Artificial intelligence; Logical programming; Deduction; Automatic proving; Safety; Deterministic automaton; Tree automaton; Transmission protocol; Cryptography; Regular language; Intruder; Bottom up method
SD :	Inteligencia artificial; Programación lógica; Deducción; Demostración automática; Seguridad; Autómata determinista; Autómata árbol; Protocolo transmisión; Criptografía; Lenguaje racional; Intruso; Método ascendente
LO :	INIST-16343.354000124491700280
ID :	05-0355351

Links to Exploration step

Pascal:05-0355351

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Regular protocols and attacks with regular knowledge</title>
<author><name sortKey="Truderung, Tomasz" sort="Truderung, Tomasz" uniqKey="Truderung T" first="Tomasz" last="Truderung">Tomasz Truderung</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="02"><s1>Institute of Computer Science, Wroclaw University</s1>
<s3>POL</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">05-0355351</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 05-0355351 INIST</idno>
<idno type="RBID">Pascal:05-0355351</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000539</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Regular protocols and attacks with regular knowledge</title>
<author><name sortKey="Truderung, Tomasz" sort="Truderung, Tomasz" uniqKey="Truderung T" first="Tomasz" last="Truderung">Tomasz Truderung</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="02"><s1>Institute of Computer Science, Wroclaw University</s1>
<s3>POL</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2005">2005</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Artificial intelligence</term>
<term>Automatic proving</term>
<term>Bottom up method</term>
<term>Cryptography</term>
<term>Deduction</term>
<term>Deterministic automaton</term>
<term>Intruder</term>
<term>Logical programming</term>
<term>Regular language</term>
<term>Safety</term>
<term>Transmission protocol</term>
<term>Tree automaton</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Intelligence artificielle</term>
<term>Programmation logique</term>
<term>Déduction</term>
<term>Démonstration automatique</term>
<term>Sécurité</term>
<term>Automate déterministe</term>
<term>Automate arbre</term>
<term>Protocole transmission</term>
<term>Cryptographie</term>
<term>Langage rationnel</term>
<term>Intrus</term>
<term>Méthode ascendante</term>
<term>.</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We prove that, if the initial knowledge of the intruder is given by a deterministic bottom-up tree automaton, then the insecurity problem for cryptographic protocols with atomic keys for a bounded number of sessions is NP-complete. We prove also that if regural languages (given by tree automata) are used in protocol descriptions to restrict the form of messages, then the insecurity problem is NEXPTIME-complete. Furthermore, we define a class of cryptographic protocols, called regular protocols, such that the knowledge which the intruder can gain during an unlimited number of sessions of a protocol is a regular language.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01>
<fA05><s2>3632</s2>
</fA05>
<fA08 i1="01" i2="1" l="ENG"><s1>Regular protocols and attacks with regular knowledge</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>CADE-20 : automated deduction : Tallinn, 22-27 July 2005</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>TRUDERUNG (Tomasz)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>NIEUWENHUIS (Robert)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>Institute of Computer Science, Wroclaw University</s1>
<s3>POL</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA20><s1>377-391</s1>
</fA20>
<fA21><s1>2005</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA26 i1="01"><s0>3-540-28005-7</s0>
</fA26>
<fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000124491700280</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2005 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>15 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>05-0355351</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64>
<fA66 i1="01"><s0>DEU</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>We prove that, if the initial knowledge of the intruder is given by a deterministic bottom-up tree automaton, then the insecurity problem for cryptographic protocols with atomic keys for a bounded number of sessions is NP-complete. We prove also that if regural languages (given by tree automata) are used in protocol descriptions to restrict the form of messages, then the insecurity problem is NEXPTIME-complete. Furthermore, we define a class of cryptographic protocols, called regular protocols, such that the knowledge which the intruder can gain during an unlimited number of sessions of a protocol is a regular language.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02C02</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Intelligence artificielle</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Artificial intelligence</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Inteligencia artificial</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Programmation logique</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Logical programming</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Programación lógica</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Déduction</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Deduction</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Deducción</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Démonstration automatique</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Automatic proving</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Demostración automática</s0>
<s5>04</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Sécurité</s0>
<s5>06</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Safety</s0>
<s5>06</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Seguridad</s0>
<s5>06</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Automate déterministe</s0>
<s5>07</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Deterministic automaton</s0>
<s5>07</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Autómata determinista</s0>
<s5>07</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Automate arbre</s0>
<s5>08</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Tree automaton</s0>
<s5>08</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Autómata árbol</s0>
<s5>08</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Protocole transmission</s0>
<s5>09</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Transmission protocol</s0>
<s5>09</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA"><s0>Protocolo transmisión</s0>
<s5>09</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Cryptographie</s0>
<s5>10</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG"><s0>Cryptography</s0>
<s5>10</s5>
</fC03>
<fC03 i1="09" i2="X" l="SPA"><s0>Criptografía</s0>
<s5>10</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Langage rationnel</s0>
<s5>11</s5>
</fC03>
<fC03 i1="10" i2="X" l="ENG"><s0>Regular language</s0>
<s5>11</s5>
</fC03>
<fC03 i1="10" i2="X" l="SPA"><s0>Lenguaje racional</s0>
<s5>11</s5>
</fC03>
<fC03 i1="11" i2="X" l="FRE"><s0>Intrus</s0>
<s5>18</s5>
</fC03>
<fC03 i1="11" i2="X" l="ENG"><s0>Intruder</s0>
<s5>18</s5>
</fC03>
<fC03 i1="11" i2="X" l="SPA"><s0>Intruso</s0>
<s5>18</s5>
</fC03>
<fC03 i1="12" i2="X" l="FRE"><s0>Méthode ascendante</s0>
<s5>23</s5>
</fC03>
<fC03 i1="12" i2="X" l="ENG"><s0>Bottom up method</s0>
<s5>23</s5>
</fC03>
<fC03 i1="12" i2="X" l="SPA"><s0>Método ascendente</s0>
<s5>23</s5>
</fC03>
<fC03 i1="13" i2="X" l="FRE"><s0>.</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03>
<fN21><s1>248</s1>
</fN21>
<fN44 i1="01"><s1>OTO</s1>
</fN44>
<fN82><s1>OTO</s1>
</fN82>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>International conference on automated deduction</s1>
<s2>20</s2>
<s3>Tallinn EST</s3>
<s4>2005-07-22</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 05-0355351 INIST</NO>
<ET>Regular protocols and attacks with regular knowledge</ET>
<AU>TRUDERUNG (Tomasz); NIEUWENHUIS (Robert)</AU>
<AF>LORIA-INRIA-Lorraine/France (1 aut.); Institute of Computer Science, Wroclaw University/Pologne (1 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2005; Vol. 3632; Pp. 377-391; Bibl. 15 ref.</SO>
<LA>Anglais</LA>
<EA>We prove that, if the initial knowledge of the intruder is given by a deterministic bottom-up tree automaton, then the insecurity problem for cryptographic protocols with atomic keys for a bounded number of sessions is NP-complete. We prove also that if regural languages (given by tree automata) are used in protocol descriptions to restrict the form of messages, then the insecurity problem is NEXPTIME-complete. Furthermore, we define a class of cryptographic protocols, called regular protocols, such that the knowledge which the intruder can gain during an unlimited number of sessions of a protocol is a regular language.</EA>
<CC>001D02C02</CC>
<FD>Intelligence artificielle; Programmation logique; Déduction; Démonstration automatique; Sécurité; Automate déterministe; Automate arbre; Protocole transmission; Cryptographie; Langage rationnel; Intrus; Méthode ascendante; .</FD>
<ED>Artificial intelligence; Logical programming; Deduction; Automatic proving; Safety; Deterministic automaton; Tree automaton; Transmission protocol; Cryptography; Regular language; Intruder; Bottom up method</ED>
<SD>Inteligencia artificial; Programación lógica; Deducción; Demostración automática; Seguridad; Autómata determinista; Autómata árbol; Protocolo transmisión; Criptografía; Lenguaje racional; Intruso; Método ascendente</SD>
<LO>INIST-16343.354000124491700280</LO>
<ID>05-0355351</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 000539 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000539 | 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-0355351
   |texte=   Regular protocols and attacks with regular knowledge
}}

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

Regular protocols and attacks with regular knowledge

Regular protocols and attacks with regular knowledge

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