MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Charatonik, Witold
Amadio, Roberto		dblp
dblp
Not MPG Author(s):
Amadio, Roberto
Editor(s):
Brim, Lubos
Jancar, Petr
Kretinsky, Mojomir
Kucera, Antonin		dblp
dblp
dblp
dblp
Not MPII Editor(s):
Brim, Lubos
Jancar, Petr
Kretinsky, Mojomir
Kucera, Antonin
BibTeX cite key*:
AmadioCharatonik2002
Title, Booktitle
Title*:
On Name Generation and Set-Based Analysis in the Dolev-Yao Model
Booktitle*:
CONCUR 2002 - Concurrency Theory. 13th International Conference
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
Brno, Czech Republic
Language:
English
Event Date*
(no longer used):
-- August 20-23, 2002
Organization:
Event Start Date:
20 August 2002
Event End Date:
23 August 2002
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
2421
Number:
Month:
Pages:
499-514
Year*:
2002
VG Wort Pages:
ISBN/ISSN:
3-540-44043-7
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We study the control reachability problem in the Dolev-Yao model of cryptographic protocols when principals are represented by tail recursive processes with generated names. We propose a conservative approximation of the problem by reduction to a non-standard collapsed operational semantics and we introduce checkable syntactic conditions entailing the equivalence of the standard and the collapsed semantics. Then we introduce a conservative and decidable set-based analysis of the collapsed operational semantics and we characterize a situation where the analysis is exact.
Keywords:
cryptographic protocols, name generation, verification, set constraints
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
Expert
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:
@INPROCEEDINGS{AmadioCharatonik2002,
AUTHOR = {Charatonik, Witold and Amadio, Roberto},
 EDITOR = {Brim, Lubos and Jancar, Petr and Kretinsky, Mojomir and Kucera, Antonin},
 TITLE = {On Name Generation and Set-Based Analysis in the Dolev-Yao Model},
 BOOKTITLE = {CONCUR 2002 - Concurrency Theory. 13th International Conference},
 PUBLISHER = {Springer},
 YEAR = {2002},
 VOLUME = {2421},
 PAGES = {499--514},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Brno, Czech Republic},
 ISBN = {3-540-44043-7},
}

Entry last modified by Christine Kiesel, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Witold Charatonik		Created
09/27/2002 09:12:03 PM
Revisions
7.
6.
5.
4.
3.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel		Edit Dates
01.09.2003 17:20:02
04.08.2003 16:06:54
04.08.2003 16:00:49
23.07.2003 15:31:01
23.07.2003 15:26:29