InforLorV4, Hal, Corpus, bibRecord, 001788

Computing knowledge in security protocols under convergent equational theories

Identifieur interne : 001788 ( Hal/Corpus ); précédent : 001787; suivant : 001789

Computing knowledge in security protocols under convergent equational theories

Auteurs : Stefan Ciobaca ; Stéphanie Delaune ; Steve Kremer

Source :

Journal of Automated Reasoning [ 0168-7433 ] ; 2012.

RBID : Hal:inria-00636794

Abstract

The analysis of security protocols requires reasoning about the knowledge an attacker acquires by eavesdropping on network traffic. In formal approaches, the messages exchanged over the network are modeled by a term algebra equipped with an equational theory axiomatizing the properties of the cryptographic primitives (e.g. encryption, signature). In this context, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems.\par We propose a procedure for both problems under arbitrary convergent equational theories. Since the underlying problems are undecidable we cannot guarantee termination. Nevertheless, our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We also provide a prototype implementation.

Url:

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

DOI: 10.1007/s10817-010-9197-7

Links to Exploration step

Hal:inria-00636794

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Computing knowledge in security protocols under convergent equational theories</title>
<author><name sortKey="Ciobaca, Stefan" sort="Ciobaca, Stefan" uniqKey="Ciobaca S" first="Stefan" last="Ciobaca">Stefan Ciobaca</name>
<affiliation><hal:affiliation type="laboratory" xml:id="struct-2571" status="VALID"><orgName>Laboratoire Spécification et Vérification [Cachan]</orgName>
<orgName type="acronym">LSV</orgName>
<desc><address><addrLine>Bâtiment d'Alembert 61 Avenue du Président Wilson 94235 CACHAN CEDEX</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lsv.ens-cachan.fr/</ref>
</desc>
<listRelation><relation active="#struct-6862" type="direct"></relation>
<relation name="UMR8643" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-6862" type="direct"><org type="institution" xml:id="struct-6862" status="VALID"><orgName>École normale supérieure - Cachan</orgName>
<orgName type="acronym">ENS Cachan</orgName>
<desc><address><addrLine>61, avenue du Président Wilson - 94230 Cachan</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.ens-cachan.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR8643" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno>
<idno type="ISNI">0000000122597504</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
<author><name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name>
<affiliation><hal:affiliation type="laboratory" xml:id="struct-2571" status="VALID"><orgName>Laboratoire Spécification et Vérification [Cachan]</orgName>
<orgName type="acronym">LSV</orgName>
<desc><address><addrLine>Bâtiment d'Alembert 61 Avenue du Président Wilson 94235 CACHAN CEDEX</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lsv.ens-cachan.fr/</ref>
</desc>
<listRelation><relation active="#struct-6862" type="direct"></relation>
<relation name="UMR8643" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-6862" type="direct"><org type="institution" xml:id="struct-6862" status="VALID"><orgName>École normale supérieure - Cachan</orgName>
<orgName type="acronym">ENS Cachan</orgName>
<desc><address><addrLine>61, avenue du Président Wilson - 94230 Cachan</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.ens-cachan.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR8643" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno>
<idno type="ISNI">0000000122597504</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
<author><name sortKey="Kremer, Steve" sort="Kremer, Steve" uniqKey="Kremer S" first="Steve" last="Kremer">Steve Kremer</name>
<affiliation><hal:affiliation type="researchteam" xml:id="struct-2337" status="OLD"><idno type="RNSR">200218376V</idno>
<orgName>Security of information systems</orgName>
<orgName type="acronym">SECSI</orgName>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/equipes/secsi</ref>
</desc>
<listRelation><relation active="#struct-2571" type="direct"></relation>
<relation name="UMR8643" active="#struct-441569" type="direct"></relation>
<relation active="#struct-6862" type="direct"></relation>
<relation active="#struct-118511" type="direct"></relation>
<relation active="#struct-300009" type="indirect"></relation>
</listRelation>
<tutelles><tutelle active="#struct-2571" type="direct"><org type="laboratory" xml:id="struct-2571" status="VALID"><orgName>Laboratoire Spécification et Vérification [Cachan]</orgName>
<orgName type="acronym">LSV</orgName>
<desc><address><addrLine>Bâtiment d'Alembert 61 Avenue du Président Wilson 94235 CACHAN CEDEX</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lsv.ens-cachan.fr/</ref>
</desc>
<listRelation><relation active="#struct-6862" type="direct"></relation>
<relation name="UMR8643" active="#struct-441569" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR8643" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno>
<idno type="ISNI">0000000122597504</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-6862" type="direct"><org type="institution" xml:id="struct-6862" status="VALID"><orgName>École normale supérieure - Cachan</orgName>
<orgName type="acronym">ENS Cachan</orgName>
<desc><address><addrLine>61, avenue du Président Wilson - 94230 Cachan</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.ens-cachan.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-118511" type="direct"><org type="laboratory" xml:id="struct-118511" status="VALID"><idno type="RNSR">200818248E</idno>
<orgName>INRIA Saclay - Ile de France</orgName>
<desc><address><addrLine>1 rue Honoré d'Estienne d'OrvesBâtiment Alan TuringCampus de l'École Polytechnique91120 Palaiseau</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre/saclay</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00636794</idno>
<idno type="halId">inria-00636794</idno>
<idno type="halUri">https://hal.inria.fr/inria-00636794</idno>
<idno type="url">https://hal.inria.fr/inria-00636794</idno>
<idno type="doi">10.1007/s10817-010-9197-7</idno>
<date when="2012">2012</date>
<idno type="wicri:Area/Hal/Corpus">001788</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Computing knowledge in security protocols under convergent equational theories</title>
<author><name sortKey="Ciobaca, Stefan" sort="Ciobaca, Stefan" uniqKey="Ciobaca S" first="Stefan" last="Ciobaca">Stefan Ciobaca</name>
<affiliation><hal:affiliation type="laboratory" xml:id="struct-2571" status="VALID"><orgName>Laboratoire Spécification et Vérification [Cachan]</orgName>
<orgName type="acronym">LSV</orgName>
<desc><address><addrLine>Bâtiment d'Alembert 61 Avenue du Président Wilson 94235 CACHAN CEDEX</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lsv.ens-cachan.fr/</ref>
</desc>
<listRelation><relation active="#struct-6862" type="direct"></relation>
<relation name="UMR8643" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-6862" type="direct"><org type="institution" xml:id="struct-6862" status="VALID"><orgName>École normale supérieure - Cachan</orgName>
<orgName type="acronym">ENS Cachan</orgName>
<desc><address><addrLine>61, avenue du Président Wilson - 94230 Cachan</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.ens-cachan.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR8643" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno>
<idno type="ISNI">0000000122597504</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
<author><name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name>
<affiliation><hal:affiliation type="laboratory" xml:id="struct-2571" status="VALID"><orgName>Laboratoire Spécification et Vérification [Cachan]</orgName>
<orgName type="acronym">LSV</orgName>
<desc><address><addrLine>Bâtiment d'Alembert 61 Avenue du Président Wilson 94235 CACHAN CEDEX</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lsv.ens-cachan.fr/</ref>
</desc>
<listRelation><relation active="#struct-6862" type="direct"></relation>
<relation name="UMR8643" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-6862" type="direct"><org type="institution" xml:id="struct-6862" status="VALID"><orgName>École normale supérieure - Cachan</orgName>
<orgName type="acronym">ENS Cachan</orgName>
<desc><address><addrLine>61, avenue du Président Wilson - 94230 Cachan</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.ens-cachan.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR8643" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno>
<idno type="ISNI">0000000122597504</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
<author><name sortKey="Kremer, Steve" sort="Kremer, Steve" uniqKey="Kremer S" first="Steve" last="Kremer">Steve Kremer</name>
<affiliation><hal:affiliation type="researchteam" xml:id="struct-2337" status="OLD"><idno type="RNSR">200218376V</idno>
<orgName>Security of information systems</orgName>
<orgName type="acronym">SECSI</orgName>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/equipes/secsi</ref>
</desc>
<listRelation><relation active="#struct-2571" type="direct"></relation>
<relation name="UMR8643" active="#struct-441569" type="direct"></relation>
<relation active="#struct-6862" type="direct"></relation>
<relation active="#struct-118511" type="direct"></relation>
<relation active="#struct-300009" type="indirect"></relation>
</listRelation>
<tutelles><tutelle active="#struct-2571" type="direct"><org type="laboratory" xml:id="struct-2571" status="VALID"><orgName>Laboratoire Spécification et Vérification [Cachan]</orgName>
<orgName type="acronym">LSV</orgName>
<desc><address><addrLine>Bâtiment d'Alembert 61 Avenue du Président Wilson 94235 CACHAN CEDEX</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lsv.ens-cachan.fr/</ref>
</desc>
<listRelation><relation active="#struct-6862" type="direct"></relation>
<relation name="UMR8643" active="#struct-441569" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR8643" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno>
<idno type="ISNI">0000000122597504</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-6862" type="direct"><org type="institution" xml:id="struct-6862" status="VALID"><orgName>École normale supérieure - Cachan</orgName>
<orgName type="acronym">ENS Cachan</orgName>
<desc><address><addrLine>61, avenue du Président Wilson - 94230 Cachan</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.ens-cachan.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-118511" type="direct"><org type="laboratory" xml:id="struct-118511" status="VALID"><idno type="RNSR">200818248E</idno>
<orgName>INRIA Saclay - Ile de France</orgName>
<desc><address><addrLine>1 rue Honoré d'Estienne d'OrvesBâtiment Alan TuringCampus de l'École Polytechnique91120 Palaiseau</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre/saclay</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
</analytic>
<idno type="DOI">10.1007/s10817-010-9197-7</idno>
<series><title level="j">Journal of Automated Reasoning</title>
<idno type="ISSN">0168-7433</idno>
<imprint><date type="datePub">2012</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The analysis of security protocols requires reasoning about the knowledge an attacker acquires by eavesdropping on network traffic. In formal approaches, the messages exchanged over the network are modeled by a term algebra equipped with an equational theory axiomatizing the properties of the cryptographic primitives (e.g. encryption, signature). In this context, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems.\par We propose a procedure for both problems under arbitrary convergent equational theories. Since the underlying problems are undecidable we cannot guarantee termination. Nevertheless, our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We also provide a prototype implementation.</div>
</front>
</TEI>
<hal api="V3"><titleStmt><title xml:lang="en">Computing knowledge in security protocols under convergent equational theories</title>
<author role="aut"><persName><forename type="first">Stefan</forename>
<surname>Ciobaca</surname>
</persName>
<email></email>
<idno type="halauthor">533722</idno>
<affiliation ref="#struct-2571"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Stéphanie</forename>
<surname>Delaune</surname>
</persName>
<email></email>
<idno type="halauthor">654533</idno>
<orgName ref="#struct-441569"></orgName>
<affiliation ref="#struct-2571"></affiliation>
<affiliation ref="#struct-2337"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Steve</forename>
<surname>Kremer</surname>
</persName>
<email>steve.kremer@inria.fr</email>
<idno type="idhal">steve-kremer</idno>
<idno type="halauthor">651222</idno>
<affiliation ref="#struct-2337"></affiliation>
<affiliation ref="#struct-189789"></affiliation>
</author>
<editor role="depositor"><persName><forename>Steve</forename>
<surname>Kremer</surname>
</persName>
<email>steve.kremer@inria.fr</email>
</editor>
</titleStmt>
<editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2015-10-07 22:31:49</date>
<date type="whenModified">2015-10-09 01:05:46</date>
<date type="whenReleased">2015-10-08 14:55:48</date>
<date type="whenProduced">2012</date>
<date type="whenEndEmbargoed">2015-10-07</date>
<ref type="file" target="https://hal.inria.fr/inria-00636794/document"><date notBefore="2015-10-07"></date>
</ref>
<ref type="file" subtype="author" n="1" target="https://hal.inria.fr/inria-00636794/file/CDK-jar10.pdf"><date notBefore="2015-10-07"></date>
</ref>
</edition>
<respStmt><resp>contributor</resp>
<name key="165868"><persName><forename>Steve</forename>
<surname>Kremer</surname>
</persName>
<email>steve.kremer@inria.fr</email>
</name>
</respStmt>
</editionStmt>
<publicationStmt><distributor>CCSD</distributor>
<idno type="halId">inria-00636794</idno>
<idno type="halUri">https://hal.inria.fr/inria-00636794</idno>
<idno type="halBibtex">ciobaca:inria-00636794</idno>
<idno type="halRefHtml">Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.219-262. <10.1007/s10817-010-9197-7></idno>
<idno type="halRef">Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.219-262. <10.1007/s10817-010-9197-7></idno>
</publicationStmt>
<seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno>
<idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
<idno type="stamp" n="UNIV-FCOMTE">Université de Franche-Comté</idno>
<idno type="stamp" n="UNIV-BM">Université de Technologie de Belfort-Montbeliard</idno>
<idno type="stamp" n="ENSMM">Ecole Nationale Supérieure de Mécanique et des Microtechniques</idno>
<idno type="stamp" n="FEMTO-ST" p="UNIV-FCOMTE">Franche-Comté Electronique, Mécanique, Thermique et Optique - Sciences et Technologies</idno>
<idno type="stamp" n="INRIA-SACLAY">INRIA Saclay - Ile de France</idno>
<idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno>
<idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno>
<idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno>
<idno type="stamp" n="UNIV-BM-THESE">Université de Technologie de Belfort-Montbeliard</idno>
<idno type="stamp" n="LORIA2">Publications du LORIA</idno>
<idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno>
<idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
<idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno>
<idno type="stamp" n="INRIA2">INRIA 2</idno>
</seriesStmt>
<notesStmt><note type="audience" n="2">International</note>
<note type="popular" n="0">No</note>
<note type="peer" n="1">Yes</note>
</notesStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Computing knowledge in security protocols under convergent equational theories</title>
<author role="aut"><persName><forename type="first">Stefan</forename>
<surname>Ciobaca</surname>
</persName>
<idno type="halAuthorId">533722</idno>
<affiliation ref="#struct-2571"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Stéphanie</forename>
<surname>Delaune</surname>
</persName>
<idno type="halAuthorId">654533</idno>
<orgName ref="#struct-441569"></orgName>
<affiliation ref="#struct-2571"></affiliation>
<affiliation ref="#struct-2337"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Steve</forename>
<surname>Kremer</surname>
</persName>
<email>steve.kremer@inria.fr</email>
<idno type="idHal">steve-kremer</idno>
<idno type="halAuthorId">651222</idno>
<affiliation ref="#struct-2337"></affiliation>
<affiliation ref="#struct-189789"></affiliation>
</author>
</analytic>
<monogr><idno type="halJournalId" status="VALID">15114</idno>
<idno type="issn">0168-7433</idno>
<idno type="eissn">1573-0670</idno>
<title level="j">Journal of Automated Reasoning</title>
<imprint><publisher>Springer Verlag</publisher>
<biblScope unit="volume">48</biblScope>
<biblScope unit="issue">2</biblScope>
<biblScope unit="pp">219-262</biblScope>
<date type="datePub">2012</date>
</imprint>
</monogr>
<idno type="doi">10.1007/s10817-010-9197-7</idno>
</biblStruct>
</sourceDesc>
<profileDesc><langUsage><language ident="en">English</language>
</langUsage>
<textClass><classCode scheme="halDomain" n="info.info-cr">Computer Science [cs]/Cryptography and Security [cs.CR]</classCode>
<classCode scheme="halTypology" n="ART">Journal articles</classCode>
</textClass>
<abstract xml:lang="en">The analysis of security protocols requires reasoning about the knowledge an attacker acquires by eavesdropping on network traffic. In formal approaches, the messages exchanged over the network are modeled by a term algebra equipped with an equational theory axiomatizing the properties of the cryptographic primitives (e.g. encryption, signature). In this context, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems.\par We propose a procedure for both problems under arbitrary convergent equational theories. Since the underlying problems are undecidable we cannot guarantee termination. Nevertheless, our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We also provide a prototype implementation.</abstract>
</profileDesc>
</hal>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Corpus

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

HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 001788 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Hal
   |étape=   Corpus
   |type=    RBID
   |clé=     Hal:inria-00636794
   |texte=   Computing knowledge in security protocols under convergent equational 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

Computing knowledge in security protocols under convergent equational theories

Computing knowledge in security protocols under convergent equational theories

Source :

Abstract

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