InforLorV4, Main, Exploration, bibRecordById, Pascal:08-0286921

Hierarchical combination of intruder theories

Identifieur interne : 004460 ( Main/Exploration ); précédent : 004459; suivant : 004461

Hierarchical combination of intruder theories

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

Source :

Information and computation : (Print) [ 0890-5401 ] ; 2008.

RBID : Pascal:08-0286921

Descripteurs français

Pascal (Inist)
- Déduction, Théorie équationnelle, Groupe abélien, Loi groupe, Décidabilité, Hypothèse, Contrainte, Informatique théorique, 68T15, 47XX, 20Kxx, Protocole cryptographique.

English descriptors

KwdEn :
- Abelian group, Computer theory, Constraint, Cryptographic protocol, Decidability, Deduction, Equational theory, Group law, Hypothesis.

Abstract

Recently automated deduction tools have proved to be very effective for detecting attacks on cryptographic protocols. These analysis can be improved, for finding more subtle weaknesses, by a more accurate modelling of operators employed by protocols. Several works have shown how to handle a single algebraic operator (associated with a fixed intruder theory) or how to combine several operators satisfying disjoint theories. However several interesting equational theories, such as exponentiation with an abelian group law for exponents remain out of the scope of these techniques. This has motivated us to introduce a new notion of hierarchical combination for non-disjoint intruder theories and to show decidability results for the deduction problem in these theories. We have also shown that under natural hypotheses hierarchical intruder constraints can be decided. This result applies to an exponentiation theory that appears to be more general than the one considered before.

Url:

https://hal.inria.fr/inria-00329715

Affiliations:

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Hierarchical combination of intruder theories</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">08-0286921</idno>
<date when="2008">2008</date>
<idno type="stanalyst">PASCAL 08-0286921 INIST</idno>
<idno type="RBID">Pascal:08-0286921</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000313</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000715</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000280</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000280</idno>
<idno type="wicri:doubleKey">0890-5401:2008:Chevalier Y:hierarchical:combination:of</idno>
<idno type="wicri:Area/Main/Merge">004575</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00329715</idno>
<idno type="url">https://hal.inria.fr/inria-00329715</idno>
<idno type="wicri:Area/Hal/Corpus">002779</idno>
<idno type="wicri:Area/Hal/Curation">002779</idno>
<idno type="wicri:Area/Hal/Checkpoint">003629</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003629</idno>
<idno type="wicri:doubleKey">0890-5401:2008:Chevalier Y:hierarchical:combination:of</idno>
<idno type="wicri:Area/Main/Merge">004293</idno>
<idno type="wicri:Area/Main/Curation">004460</idno>
<idno type="wicri:Area/Main/Exploration">004460</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Hierarchical combination of intruder theories</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">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
<imprint><date when="2008">2008</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Abelian group</term>
<term>Computer theory</term>
<term>Constraint</term>
<term>Cryptographic protocol</term>
<term>Decidability</term>
<term>Deduction</term>
<term>Equational theory</term>
<term>Group law</term>
<term>Hypothesis</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Déduction</term>
<term>Théorie équationnelle</term>
<term>Groupe abélien</term>
<term>Loi groupe</term>
<term>Décidabilité</term>
<term>Hypothèse</term>
<term>Contrainte</term>
<term>Informatique théorique</term>
<term>68T15</term>
<term>47XX</term>
<term>20Kxx</term>
<term>Protocole cryptographique</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Recently automated deduction tools have proved to be very effective for detecting attacks on cryptographic protocols. These analysis can be improved, for finding more subtle weaknesses, by a more accurate modelling of operators employed by protocols. Several works have shown how to handle a single algebraic operator (associated with a fixed intruder theory) or how to combine several operators satisfying disjoint theories. However several interesting equational theories, such as exponentiation with an abelian group law for exponents remain out of the scope of these techniques. This has motivated us to introduce a new notion of hierarchical combination for non-disjoint intruder theories and to show decidability results for the deduction problem in these theories. We have also shown that under natural hypotheses hierarchical intruder constraints can be decided. This result applies to an exponentiation theory that appears to be more general than the one considered before.</div>
</front>
</TEI>
<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/Main/Exploration

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

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004460 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:08-0286921
   |texte=   Hierarchical combination of 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

Serveur d'exploration sur la recherche en informatique en Lorraine

Hierarchical combination of intruder theories

Hierarchical combination of intruder theories

Source :

Descripteurs français

English descriptors

Abstract

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

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

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

	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.