Combining intruder theories
Identifieur interne :
000491 ( PascalFrancis/Curation );
précédent :
000490;
suivant :
000492
Combining intruder theories
Auteurs : Yannick Chevalier [
France] ;
Michaël Rusinowitch [
France]
Source :
-
Lecture notes in computer science [ 0302-9743 ] ; 2005.
RBID : Pascal:05-0336972
Descripteurs français
- Pascal (Inist)
- Analyse symbolique,
Cryptage,
Cryptographie,
Décryptage,
Théorie décision,
Protocole transmission,
Sécurité,
Intrus,
Analyse décision,
Théorie ensemble,
Résolubilité,
Opérateur borné,
Automate,
.,
Exponentiation.
- Wicri :
English descriptors
- KwdEn :
- Automaton,
Bounded operator,
Cryptography,
Decision analysis,
Decision theory,
Decryption,
Encryption,
Exponentiation,
Intruder,
Safety,
Set theory,
Solvability,
Symbolic analysis,
Transmission protocol.
Abstract
Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication/exponentiation, abstract encryption/decryption. In this paper we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.
| pA |
| A01 | 01 | 1 | | @0 0302-9743 |
|---|
| A05 | | | | @2 3580 |
|---|
| A08 | 01 | 1 | ENG | @1 Combining intruder theories |
|---|
| A09 | 01 | 1 | ENG | @1 Automata, languages and programming : Lisbon, 11-15 July 2005 |
|---|
| A11 | 01 | 1 | | @1 CHEVALIER (Yannick) |
|---|
| A11 | 02 | 1 | | @1 RUSINOWITCH (Michaël) |
|---|
| A12 | 01 | 1 | | @1 CAIRES (Luis) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 ITALIANO (Giuseppe F.) @9 ed. |
|---|
| A12 | 03 | 1 | | @1 MONTEIRO (Luis) @9 ed. |
|---|
| A12 | 04 | 1 | | @1 PALAMIDESSI (Catuscia) @9 ed. |
|---|
| A12 | 05 | 1 | | @1 YUNG (Moti) @9 ed. |
|---|
| A14 | 01 | | | @1 IRIT Université Paul Sabatier @3 FRA @Z 1 aut. |
|---|
| A14 | 02 | | | @1 LORIA-INRIA-Lorraine @3 FRA @Z 2 aut. |
|---|
| A20 | | | | @1 639-651 |
|---|
| A21 | | | | @1 2005 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-27580-0 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000124488420520 |
|---|
| A44 | | | | @0 0000 @1 © 2005 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 19 ref. |
|---|
| A47 | 01 | 1 | | @0 05-0336972 |
|---|
| 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 Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication/exponentiation, abstract encryption/decryption. In this paper we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions. |
|---|
| C02 | 01 | X | | @0 001D02A03 |
|---|
| C03 | 01 | X | FRE | @0 Analyse symbolique @5 06 |
|---|
| C03 | 01 | X | ENG | @0 Symbolic analysis @5 06 |
|---|
| C03 | 01 | X | SPA | @0 Análisis simbolico @5 06 |
|---|
| C03 | 02 | X | FRE | @0 Cryptage @5 07 |
|---|
| C03 | 02 | X | ENG | @0 Encryption @5 07 |
|---|
| C03 | 02 | X | SPA | @0 Cifrado @5 07 |
|---|
| C03 | 03 | X | FRE | @0 Cryptographie @5 08 |
|---|
| C03 | 03 | X | ENG | @0 Cryptography @5 08 |
|---|
| C03 | 03 | X | SPA | @0 Criptografía @5 08 |
|---|
| C03 | 04 | X | FRE | @0 Décryptage @5 09 |
|---|
| C03 | 04 | X | ENG | @0 Decryption @5 09 |
|---|
| C03 | 04 | X | SPA | @0 Desciframiento @5 09 |
|---|
| C03 | 05 | X | FRE | @0 Théorie décision @5 10 |
|---|
| C03 | 05 | X | ENG | @0 Decision theory @5 10 |
|---|
| C03 | 05 | X | SPA | @0 Teoría decisión @5 10 |
|---|
| C03 | 06 | X | FRE | @0 Protocole transmission @5 11 |
|---|
| C03 | 06 | X | ENG | @0 Transmission protocol @5 11 |
|---|
| C03 | 06 | X | SPA | @0 Protocolo transmisión @5 11 |
|---|
| C03 | 07 | X | FRE | @0 Sécurité @5 12 |
|---|
| C03 | 07 | X | ENG | @0 Safety @5 12 |
|---|
| C03 | 07 | X | SPA | @0 Seguridad @5 12 |
|---|
| C03 | 08 | X | FRE | @0 Intrus @5 18 |
|---|
| C03 | 08 | X | ENG | @0 Intruder @5 18 |
|---|
| C03 | 08 | X | SPA | @0 Intruso @5 18 |
|---|
| C03 | 09 | X | FRE | @0 Analyse décision @5 19 |
|---|
| C03 | 09 | X | ENG | @0 Decision analysis @5 19 |
|---|
| C03 | 09 | X | SPA | @0 Análisis decisión @5 19 |
|---|
| C03 | 10 | X | FRE | @0 Théorie ensemble @5 23 |
|---|
| C03 | 10 | X | ENG | @0 Set theory @5 23 |
|---|
| C03 | 10 | X | SPA | @0 Teoría conjunto @5 23 |
|---|
| C03 | 11 | X | FRE | @0 Résolubilité @5 24 |
|---|
| C03 | 11 | X | ENG | @0 Solvability @5 24 |
|---|
| C03 | 11 | X | SPA | @0 Resolubilidad @5 24 |
|---|
| C03 | 12 | X | FRE | @0 Opérateur borné @5 25 |
|---|
| C03 | 12 | X | ENG | @0 Bounded operator @5 25 |
|---|
| C03 | 12 | X | SPA | @0 Operador acotado @5 25 |
|---|
| C03 | 13 | X | FRE | @0 Automate @5 41 |
|---|
| C03 | 13 | X | ENG | @0 Automaton @5 41 |
|---|
| C03 | 13 | X | SPA | @0 Autómata @5 41 |
|---|
| C03 | 14 | X | FRE | @0 . @4 INC @5 82 |
|---|
| C03 | 15 | X | FRE | @0 Exponentiation @4 CD @5 96 |
|---|
| C03 | 15 | X | ENG | @0 Exponentiation @4 CD @5 96 |
|---|
| C03 | 15 | X | SPA | @0 Expositoración @4 CD @5 96 |
|---|
| N21 | | | | @1 234 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 ICALP : international colloquium on automata, languages and programming @2 32 @3 Lisbon PRT @4 2005-07-11 |
|---|
|
|---|
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000547
Links to Exploration step
Pascal:05-0336972
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Combining intruder theories</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>IRIT Université Paul Sabatier</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">05-0336972</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 05-0336972 INIST</idno>
<idno type="RBID">Pascal:05-0336972</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000547</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000491</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Combining intruder theories</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>IRIT Université Paul Sabatier</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><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><seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Automaton</term>
<term>Bounded operator</term>
<term>Cryptography</term>
<term>Decision analysis</term>
<term>Decision theory</term>
<term>Decryption</term>
<term>Encryption</term>
<term>Exponentiation</term>
<term>Intruder</term>
<term>Safety</term>
<term>Set theory</term>
<term>Solvability</term>
<term>Symbolic analysis</term>
<term>Transmission protocol</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Analyse symbolique</term>
<term>Cryptage</term>
<term>Cryptographie</term>
<term>Décryptage</term>
<term>Théorie décision</term>
<term>Protocole transmission</term>
<term>Sécurité</term>
<term>Intrus</term>
<term>Analyse décision</term>
<term>Théorie ensemble</term>
<term>Résolubilité</term>
<term>Opérateur borné</term>
<term>Automate</term>
<term>.</term>
<term>Exponentiation</term>
</keywords><keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Cryptographie</term>
</keywords><front><div type="abstract" xml:lang="en">Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication/exponentiation, abstract encryption/decryption. In this paper we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>3580</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Combining intruder theories</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>Automata, languages and programming : Lisbon, 11-15 July 2005</s1>
</fA09><fA11 i1="01" i2="1"><s1>CHEVALIER (Yannick)</s1>
</fA11><fA11 i1="02" i2="1"><s1>RUSINOWITCH (Michaël)</s1>
</fA11><fA12 i1="01" i2="1"><s1>CAIRES (Luis)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>ITALIANO (Giuseppe F.)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="03" i2="1"><s1>MONTEIRO (Luis)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="04" i2="1"><s1>PALAMIDESSI (Catuscia)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="05" i2="1"><s1>YUNG (Moti)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>IRIT Université Paul Sabatier</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14><fA14 i1="02"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</fA14><fA20><s1>639-651</s1>
</fA20><fA21><s1>2005</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-27580-0</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000124488420520</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2005 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>19 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>05-0336972</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><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>Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication/exponentiation, abstract encryption/decryption. In this paper we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A03</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Analyse symbolique</s0>
<s5>06</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Symbolic analysis</s0>
<s5>06</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Análisis simbolico</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Cryptage</s0>
<s5>07</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Encryption</s0>
<s5>07</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Cifrado</s0>
<s5>07</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Cryptographie</s0>
<s5>08</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Cryptography</s0>
<s5>08</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Criptografía</s0>
<s5>08</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Décryptage</s0>
<s5>09</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Decryption</s0>
<s5>09</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Desciframiento</s0>
<s5>09</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Théorie décision</s0>
<s5>10</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Decision theory</s0>
<s5>10</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Teoría decisión</s0>
<s5>10</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Protocole transmission</s0>
<s5>11</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Transmission protocol</s0>
<s5>11</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Protocolo transmisión</s0>
<s5>11</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Sécurité</s0>
<s5>12</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Safety</s0>
<s5>12</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Seguridad</s0>
<s5>12</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Intrus</s0>
<s5>18</s5>
</fC03><fC03 i1="08" i2="X" l="ENG"><s0>Intruder</s0>
<s5>18</s5>
</fC03><fC03 i1="08" i2="X" l="SPA"><s0>Intruso</s0>
<s5>18</s5>
</fC03><fC03 i1="09" i2="X" l="FRE"><s0>Analyse décision</s0>
<s5>19</s5>
</fC03><fC03 i1="09" i2="X" l="ENG"><s0>Decision analysis</s0>
<s5>19</s5>
</fC03><fC03 i1="09" i2="X" l="SPA"><s0>Análisis decisión</s0>
<s5>19</s5>
</fC03><fC03 i1="10" i2="X" l="FRE"><s0>Théorie ensemble</s0>
<s5>23</s5>
</fC03><fC03 i1="10" i2="X" l="ENG"><s0>Set theory</s0>
<s5>23</s5>
</fC03><fC03 i1="10" i2="X" l="SPA"><s0>Teoría conjunto</s0>
<s5>23</s5>
</fC03><fC03 i1="11" i2="X" l="FRE"><s0>Résolubilité</s0>
<s5>24</s5>
</fC03><fC03 i1="11" i2="X" l="ENG"><s0>Solvability</s0>
<s5>24</s5>
</fC03><fC03 i1="11" i2="X" l="SPA"><s0>Resolubilidad</s0>
<s5>24</s5>
</fC03><fC03 i1="12" i2="X" l="FRE"><s0>Opérateur borné</s0>
<s5>25</s5>
</fC03><fC03 i1="12" i2="X" l="ENG"><s0>Bounded operator</s0>
<s5>25</s5>
</fC03><fC03 i1="12" i2="X" l="SPA"><s0>Operador acotado</s0>
<s5>25</s5>
</fC03><fC03 i1="13" i2="X" l="FRE"><s0>Automate</s0>
<s5>41</s5>
</fC03><fC03 i1="13" i2="X" l="ENG"><s0>Automaton</s0>
<s5>41</s5>
</fC03><fC03 i1="13" i2="X" l="SPA"><s0>Autómata</s0>
<s5>41</s5>
</fC03><fC03 i1="14" i2="X" l="FRE"><s0>.</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03><fC03 i1="15" i2="X" l="FRE"><s0>Exponentiation</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="15" i2="X" l="ENG"><s0>Exponentiation</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="15" i2="X" l="SPA"><s0>Expositoración</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fN21><s1>234</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>ICALP : international colloquium on automata, languages and programming</s1>
<s2>32</s2>
<s3>Lisbon PRT</s3>
<s4>2005-07-11</s4>
</fA30>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000491 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Curation/biblio.hfd -nk 000491 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Curation
|type= RBID
|clé= Pascal:05-0336972
|texte= Combining intruder theories
}}
| 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 |  |
