InforLorV4, PascalFrancis, Corpus, bibRecord, 000313

Hierarchical combination of intruder theories

Identifieur interne : 000313 ( PascalFrancis/Corpus ); précédent : 000312; suivant : 000314

Hierarchical combination of intruder theories

Auteurs : Yannick Chevalier ; Michael Rusinowitch

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.

Notice en format standard (ISO 2709)

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

A01	`01`	`1`		`@0 0890-5401`
A02	`01`			`@0 INFCEC`
A03		`1`		`@0 Inf. comput. : (Print)`
A05				`@2 206`
A06				`@2 2-4`
A08	`01`	`1`	`ENG`	`@1 Hierarchical combination of intruder theories`
A09	`01`	`1`	`ENG`	`@1 Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA '06)`
A11	`01`	`1`		`@1 CHEVALIER (Yannick)`
A11	`02`	`1`		`@1 RUSINOWITCH (Michael)`
A12	`01`	`1`		`@1 DEGANO (Pierpaolo) @9 ed.`
A12	`02`	`1`		`@1 KÜSTERS (Ralf) @9 ed.`
A12	`03`	`1`		`@1 VIGANO (Luca) @9 ed.`
A12	`04`	`1`		`@1 ZDANCEWIC (Steve) @9 ed.`
A14	`01`			`@1 IRIT Team LiLac, Université Paul Sabatier @2 Toulouse @3 FRA @Z 1 aut.`
A14	`02`			`@1 Loria-INRIA Lorraine, Cassis Project @2 Nancy @3 FRA @Z 2 aut.`
A15	`01`			`@1 Dipartimento di Informatica, Università di Pisa @3 ITA @Z 1 aut.`
A15	`02`			`@1 Department of Computer Science, ETH Zürich @3 CHE @Z 2 aut.`
A15	`03`			`@1 Dipartimento di Informatica, Università di Verona @3 ITA @Z 3 aut.`
A15	`04`			`@1 Department of Computer and Information Science, University of Pennsylvania @3 USA @Z 4 aut.`
A20				`@1 352-377`
A21				`@1 2008`
A23	`01`			`@0 ENG`
A43	`01`			`@1 INIST @2 8341 @5 354000183340040090`
A44				`@0 0000 @1 © 2008 INIST-CNRS. All rights reserved.`
A45				`@0 35 ref.`
A47	`01`	`1`		`@0 08-0286921`
A60				`@1 P @2 C`
A61				`@0 A`
A64	`01`	`1`		`@0 Information and computation : (Print)`
A66	`01`			`@0 USA`
C01	`01`		`ENG`	@0 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.
C02	`01`	`X`		`@0 001D02A08`
C02	`02`	`X`		`@0 001D02C02`
C02	`03`	`X`		`@0 001A02E17`
C02	`04`	`X`		`@0 001A02D01`
C03	`01`	`X`	`FRE`	`@0 Déduction @5 17`
C03	`01`	`X`	`ENG`	`@0 Deduction @5 17`
C03	`01`	`X`	`SPA`	`@0 Deducción @5 17`
C03	`02`	`X`	`FRE`	`@0 Théorie équationnelle @5 18`
C03	`02`	`X`	`ENG`	`@0 Equational theory @5 18`
C03	`02`	`X`	`SPA`	`@0 Teoría ecuaciónal @5 18`
C03	`03`	`X`	`FRE`	`@0 Groupe abélien @5 19`
C03	`03`	`X`	`ENG`	`@0 Abelian group @5 19`
C03	`03`	`X`	`SPA`	`@0 Grupo abeliano @5 19`
C03	`04`	`X`	`FRE`	`@0 Loi groupe @5 20`
C03	`04`	`X`	`ENG`	`@0 Group law @5 20`
C03	`04`	`X`	`SPA`	`@0 Ley grupo @5 20`
C03	`05`	`X`	`FRE`	`@0 Décidabilité @5 21`
C03	`05`	`X`	`ENG`	`@0 Decidability @5 21`
C03	`05`	`X`	`SPA`	`@0 Decidibilidad @5 21`
C03	`06`	`X`	`FRE`	`@0 Hypothèse @5 22`
C03	`06`	`X`	`ENG`	`@0 Hypothesis @5 22`
C03	`06`	`X`	`SPA`	`@0 Hipótesis @5 22`
C03	`07`	`X`	`FRE`	`@0 Contrainte @5 23`
C03	`07`	`X`	`ENG`	`@0 Constraint @5 23`
C03	`07`	`X`	`SPA`	`@0 Coacción @5 23`
C03	`08`	`X`	`FRE`	`@0 Informatique théorique @5 24`
C03	`08`	`X`	`ENG`	`@0 Computer theory @5 24`
C03	`08`	`X`	`SPA`	`@0 Informática teórica @5 24`
C03	`09`	`X`	`FRE`	`@0 68T15 @4 INC @5 70`
C03	`10`	`X`	`FRE`	`@0 47XX @4 INC @5 71`
C03	`11`	`X`	`FRE`	`@0 20Kxx @4 INC @5 72`
C03	`12`	`X`	`FRE`	`@0 Protocole cryptographique @4 CD @5 96`
C03	`12`	`X`	`ENG`	`@0 Cryptographic protocol @4 CD @5 96`
N21				`@1 182`
N44	`01`			`@1 OTO`
N82				`@1 OTO`

A30	`01`	`1`	`ENG`	`@1 Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA '06) @3 Seattle, WA USA @4 2006-08-15`

Format Inist (serveur)

NO :	PASCAL 08-0286921 INIST
ET :	Hierarchical combination of intruder theories
AU :	CHEVALIER (Yannick); RUSINOWITCH (Michael); DEGANO (Pierpaolo); KÜSTERS (Ralf); VIGANO (Luca); ZDANCEWIC (Steve)
AF :	IRIT Team LiLac, Université Paul Sabatier/Toulouse/France (1 aut.); Loria-INRIA Lorraine, Cassis Project/Nancy/France (2 aut.); Dipartimento di Informatica, Università di Pisa/Italie (1 aut.); Department of Computer Science, ETH Zürich/Suisse (2 aut.); Dipartimento di Informatica, Università di Verona/Italie (3 aut.); Department of Computer and Information Science, University of Pennsylvania/Etats-Unis (4 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	Information and computation : (Print); ISSN 0890-5401; Coden INFCEC; Etats-Unis; Da. 2008; Vol. 206; No. 2-4; Pp. 352-377; Bibl. 35 ref.
LA :	Anglais
EA :	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.
CC :	001D02A08; 001D02C02; 001A02E17; 001A02D01
FD :	Déduction; Théorie équationnelle; Groupe abélien; Loi groupe; Décidabilité; Hypothèse; Contrainte; Informatique théorique; 68T15; 47XX; 20Kxx; Protocole cryptographique
ED :	Deduction; Equational theory; Abelian group; Group law; Decidability; Hypothesis; Constraint; Computer theory; Cryptographic protocol
SD :	Deducción; Teoría ecuaciónal; Grupo abeliano; Ley grupo; Decidibilidad; Hipótesis; Coacción; Informática teórica
LO :	INIST-8341.354000183340040090
ID :	08-0286921

Links to Exploration step

Pascal:08-0286921

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><inist:fA14 i1="01"><s1>IRIT Team LiLac, Université Paul Sabatier</s1>
<s2>Toulouse</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name>
<affiliation><inist:fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
</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>
</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><inist:fA14 i1="01"><s1>IRIT Team LiLac, Université Paul Sabatier</s1>
<s2>Toulouse</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name>
<affiliation><inist:fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
</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>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0890-5401</s0>
</fA01>
<fA02 i1="01"><s0>INFCEC</s0>
</fA02>
<fA03 i2="1"><s0>Inf. comput. : (Print)</s0>
</fA03>
<fA05><s2>206</s2>
</fA05>
<fA06><s2>2-4</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>Hierarchical combination of intruder theories</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA '06)</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>DEGANO (Pierpaolo)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>KÜSTERS (Ralf)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="03" i2="1"><s1>VIGANO (Luca)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="04" i2="1"><s1>ZDANCEWIC (Steve)</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>Dipartimento di Informatica, Università di Pisa</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
</fA15>
<fA15 i1="02"><s1>Department of Computer Science, ETH Zürich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
</fA15>
<fA15 i1="03"><s1>Dipartimento di Informatica, Università di Verona</s1>
<s3>ITA</s3>
<sZ>3 aut.</sZ>
</fA15>
<fA15 i1="04"><s1>Department of Computer and Information Science, University of Pennsylvania</s1>
<s3>USA</s3>
<sZ>4 aut.</sZ>
</fA15>
<fA20><s1>352-377</s1>
</fA20>
<fA21><s1>2008</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>8341</s2>
<s5>354000183340040090</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2008 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>35 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>08-0286921</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Information and computation : (Print)</s0>
</fA64>
<fA66 i1="01"><s0>USA</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>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.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02A08</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02C02</s0>
</fC02>
<fC02 i1="03" i2="X"><s0>001A02E17</s0>
</fC02>
<fC02 i1="04" i2="X"><s0>001A02D01</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Déduction</s0>
<s5>17</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Deduction</s0>
<s5>17</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Deducción</s0>
<s5>17</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Théorie équationnelle</s0>
<s5>18</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Equational theory</s0>
<s5>18</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Teoría ecuaciónal</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Groupe abélien</s0>
<s5>19</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Abelian group</s0>
<s5>19</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Grupo abeliano</s0>
<s5>19</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Loi groupe</s0>
<s5>20</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Group law</s0>
<s5>20</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Ley grupo</s0>
<s5>20</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Décidabilité</s0>
<s5>21</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Decidability</s0>
<s5>21</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Decidibilidad</s0>
<s5>21</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Hypothèse</s0>
<s5>22</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Hypothesis</s0>
<s5>22</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Hipótesis</s0>
<s5>22</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Contrainte</s0>
<s5>23</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Constraint</s0>
<s5>23</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Coacción</s0>
<s5>23</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>24</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>24</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>24</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>68T15</s0>
<s4>INC</s4>
<s5>70</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>47XX</s0>
<s4>INC</s4>
<s5>71</s5>
</fC03>
<fC03 i1="11" i2="X" l="FRE"><s0>20Kxx</s0>
<s4>INC</s4>
<s5>72</s5>
</fC03>
<fC03 i1="12" i2="X" l="FRE"><s0>Protocole cryptographique</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="12" i2="X" l="ENG"><s0>Cryptographic protocol</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fN21><s1>182</s1>
</fN21>
<fN44 i1="01"><s1>OTO</s1>
</fN44>
<fN82><s1>OTO</s1>
</fN82>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA '06)</s1>
<s3>Seattle, WA USA</s3>
<s4>2006-08-15</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 08-0286921 INIST</NO>
<ET>Hierarchical combination of intruder theories</ET>
<AU>CHEVALIER (Yannick); RUSINOWITCH (Michael); DEGANO (Pierpaolo); KÜSTERS (Ralf); VIGANO (Luca); ZDANCEWIC (Steve)</AU>
<AF>IRIT Team LiLac, Université Paul Sabatier/Toulouse/France (1 aut.); Loria-INRIA Lorraine, Cassis Project/Nancy/France (2 aut.); Dipartimento di Informatica, Università di Pisa/Italie (1 aut.); Department of Computer Science, ETH Zürich/Suisse (2 aut.); Dipartimento di Informatica, Università di Verona/Italie (3 aut.); Department of Computer and Information Science, University of Pennsylvania/Etats-Unis (4 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Information and computation : (Print); ISSN 0890-5401; Coden INFCEC; Etats-Unis; Da. 2008; Vol. 206; No. 2-4; Pp. 352-377; Bibl. 35 ref.</SO>
<LA>Anglais</LA>
<EA>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.</EA>
<CC>001D02A08; 001D02C02; 001A02E17; 001A02D01</CC>
<FD>Déduction; Théorie équationnelle; Groupe abélien; Loi groupe; Décidabilité; Hypothèse; Contrainte; Informatique théorique; 68T15; 47XX; 20Kxx; Protocole cryptographique</FD>
<ED>Deduction; Equational theory; Abelian group; Group law; Decidability; Hypothesis; Constraint; Computer theory; Cryptographic protocol</ED>
<SD>Deducción; Teoría ecuaciónal; Grupo abeliano; Ley grupo; Decidibilidad; Hipótesis; Coacción; Informática teórica</SD>
<LO>INIST-8341.354000183340040090</LO>
<ID>08-0286921</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 000313 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000313 | 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: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
	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

Hierarchical combination of intruder theories

Hierarchical combination of intruder theories

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