InforLorV4, PascalFrancis, Checkpoint, bibRecord, 000168

Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures

Identifieur interne : 000168 ( PascalFrancis/Checkpoint ); précédent : 000167; suivant : 000169

Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures

Auteurs : Yannick Chevalier [France] ; Michael Rusinowitch [France]

Source :

Theoretical computer science [ 0304-3975 ] ; 2010.

RBID : Pascal:10-0147183

Descripteurs français

Pascal (Inist)
- Théorie décision, Analyse décision, Analyse limite, Multiplication, Décryptage, Algorithme, Théorie ensemble, Résolubilité, Contrainte, Trace, Opérateur borné, Informatique théorique, Union disjointe, Procédure décision, 68P25, 68Wxx, 03Exx, Protocole sécurité, Chiffrement, Protocole cryptographique.

English descriptors

KwdEn :
- Algorithm, Bounded operator, Computer theory, Constraint, Cryptographic protocol, Decision analysis, Decision theory, Decryption, Encryption, Limit analysis, Multiplication, Security protocol, Set theory, Solvability, Trace.

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, abstract encryption/decryption. In this report 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.

Affiliations:

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000227
to stream PascalFrancis, to step Curation: 000791

Links to Exploration step

Pascal:10-0147183

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>IRIT, Team LiLac, Université Paul Sabatier</s1>
<s2>Toulouse</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Occitanie (région administrative)</region>
<region type="old region">Midi-Pyrénées</region>
<settlement type="city">Toulouse</settlement>
</placeName>
<orgName type="university">Université Toulouse III - Paul Sabatier</orgName>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">10-0147183</idno>
<date when="2010">2010</date>
<idno type="stanalyst">PASCAL 10-0147183 INIST</idno>
<idno type="RBID">Pascal:10-0147183</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000227</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000791</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000168</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000168</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>IRIT, Team LiLac, Université Paul Sabatier</s1>
<s2>Toulouse</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Occitanie (région administrative)</region>
<region type="old region">Midi-Pyrénées</region>
<settlement type="city">Toulouse</settlement>
</placeName>
<orgName type="university">Université Toulouse III - Paul Sabatier</orgName>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</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="2010">2010</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>Algorithm</term>
<term>Bounded operator</term>
<term>Computer theory</term>
<term>Constraint</term>
<term>Cryptographic protocol</term>
<term>Decision analysis</term>
<term>Decision theory</term>
<term>Decryption</term>
<term>Encryption</term>
<term>Limit analysis</term>
<term>Multiplication</term>
<term>Security protocol</term>
<term>Set theory</term>
<term>Solvability</term>
<term>Trace</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Théorie décision</term>
<term>Analyse décision</term>
<term>Analyse limite</term>
<term>Multiplication</term>
<term>Décryptage</term>
<term>Algorithme</term>
<term>Théorie ensemble</term>
<term>Résolubilité</term>
<term>Contrainte</term>
<term>Trace</term>
<term>Opérateur borné</term>
<term>Informatique théorique</term>
<term>Union disjointe</term>
<term>Procédure décision</term>
<term>68P25</term>
<term>68Wxx</term>
<term>03Exx</term>
<term>Protocole sécurité</term>
<term>Chiffrement</term>
<term>Protocole cryptographique</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<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, abstract encryption/decryption. In this report 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>
</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>411</s2>
</fA05>
<fA06><s2>10</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>Security and Cryptography Foundations</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>CHEVALIER (Yannick)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>RUSINOWITCH (Michael)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>YUNG (Moti)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>IRIT, Team LiLac, Université Paul Sabatier</s1>
<s2>Toulouse</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</fA14>
<fA15 i1="01"><s1>Google Research and Computer Science, Columbia University</s1>
<s2>10027 New York, NY</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
</fA15>
<fA20><s1>1261-1282</s1>
</fA20>
<fA21><s1>2010</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000190124430030</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2010 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>31 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>10-0147183</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64>
<fA66 i1="01"><s0>GBR</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, abstract encryption/decryption. In this report 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>001D02A08</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02B07B</s0>
</fC02>
<fC02 i1="03" i2="X"><s0>001D02A05</s0>
</fC02>
<fC02 i1="04" i2="X"><s0>001A02A01E</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Théorie décision</s0>
<s5>17</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Decision theory</s0>
<s5>17</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Teoría decisión</s0>
<s5>17</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Analyse décision</s0>
<s5>18</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Decision analysis</s0>
<s5>18</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Análisis decisión</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Analyse limite</s0>
<s5>19</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Limit analysis</s0>
<s5>19</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Análisis límite</s0>
<s5>19</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Multiplication</s0>
<s5>20</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Multiplication</s0>
<s5>20</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Multiplicación</s0>
<s5>20</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Décryptage</s0>
<s5>21</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Decryption</s0>
<s5>21</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Desciframiento</s0>
<s5>21</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Algorithme</s0>
<s5>22</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Algorithm</s0>
<s5>22</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Algoritmo</s0>
<s5>22</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Théorie ensemble</s0>
<s5>23</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Set theory</s0>
<s5>23</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Teoría conjunto</s0>
<s5>23</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Résolubilité</s0>
<s5>24</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Solvability</s0>
<s5>24</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA"><s0>Resolubilidad</s0>
<s5>24</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Contrainte</s0>
<s5>25</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG"><s0>Constraint</s0>
<s5>25</s5>
</fC03>
<fC03 i1="09" i2="X" l="SPA"><s0>Coacción</s0>
<s5>25</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Trace</s0>
<s5>26</s5>
</fC03>
<fC03 i1="10" i2="X" l="ENG"><s0>Trace</s0>
<s5>26</s5>
</fC03>
<fC03 i1="10" i2="X" l="SPA"><s0>Traza</s0>
<s5>26</s5>
</fC03>
<fC03 i1="11" i2="X" l="FRE"><s0>Opérateur borné</s0>
<s5>27</s5>
</fC03>
<fC03 i1="11" i2="X" l="ENG"><s0>Bounded operator</s0>
<s5>27</s5>
</fC03>
<fC03 i1="11" i2="X" l="SPA"><s0>Operador acotado</s0>
<s5>27</s5>
</fC03>
<fC03 i1="12" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>28</s5>
</fC03>
<fC03 i1="12" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>28</s5>
</fC03>
<fC03 i1="12" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>28</s5>
</fC03>
<fC03 i1="13" i2="X" l="FRE"><s0>Union disjointe</s0>
<s4>INC</s4>
<s5>70</s5>
</fC03>
<fC03 i1="14" i2="X" l="FRE"><s0>Procédure décision</s0>
<s4>INC</s4>
<s5>71</s5>
</fC03>
<fC03 i1="15" i2="X" l="FRE"><s0>68P25</s0>
<s4>INC</s4>
<s5>72</s5>
</fC03>
<fC03 i1="16" i2="X" l="FRE"><s0>68Wxx</s0>
<s4>INC</s4>
<s5>73</s5>
</fC03>
<fC03 i1="17" i2="X" l="FRE"><s0>03Exx</s0>
<s4>INC</s4>
<s5>74</s5>
</fC03>
<fC03 i1="18" i2="X" l="FRE"><s0>Protocole sécurité</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="18" i2="X" l="ENG"><s0>Security protocol</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="19" i2="X" l="FRE"><s0>Chiffrement</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="19" i2="X" l="ENG"><s0>Encryption</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="20" i2="X" l="FRE"><s0>Protocole cryptographique</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03>
<fC03 i1="20" i2="X" l="ENG"><s0>Cryptographic protocol</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03>
<fN21><s1>095</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 Colloquium on Automata, Languages and Programming (ICALP 2005)</s1>
<s2>32</s2>
<s3>Lisboa PRT</s3>
<s4>2005-07-11</s4>
</fA30>
</pR>
</standard>
</inist>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
<li>Midi-Pyrénées</li>
<li>Occitanie (région administrative)</li>
</region>
<settlement><li>Nancy</li>
<li>Toulouse</li>
</settlement>
<orgName><li>Université Toulouse III - Paul Sabatier</li>
</orgName>
</list>
<tree><country name="France"><region name="Occitanie (région administrative)"><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
</region>
<name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

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

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

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000168 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Checkpoint
   |type=    RBID
   |clé=     Pascal:10-0147183
   |texte=   Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures
}}

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

Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures

Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

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