Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








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

URL of the conference:


URL for downloading the paper:


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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section