Recursion vs. Replication in Simple Cryptographic Protocols
HUTTEL, Hans and Jiří SRBA. Recursion vs. Replication in Simple Cryptographic Protocols. In Proceedings of 31st Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'05). Netherlands: Springer-Verlag, 2005, p. 175-184. |
Other formats:
BibTeX
LaTeX
RIS
|
Basic information | |
---|---|
Original name | Recursion vs. Replication in Simple Cryptographic Protocols |
Name in Czech | Rekurze a replikace a jednoduchych kryptografickych protokolech |
Authors | HUTTEL, Hans (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor). |
Edition | Netherlands, Proceedings of 31st Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'05), p. 175-184, 10 pp. 2005. |
Publisher | Springer-Verlag |
Other information | |
---|---|
Original language | English |
Type of outcome | Proceedings paper |
Field of Study | 10201 Computer sciences, information science, bioinformatics |
Country of publisher | Netherlands |
Confidentiality degree | is not subject to a state or trade secret |
RIV identification code | RIV/00216224:14330/05:00012753 |
Organization unit | Faculty of Informatics |
Keywords in English | cryptographic protocols; recursion; replication; verification |
Tags | cryptographic protocols, recursion, replication, verification |
Changed by | Changed by: RNDr. JUDr. Vladimír Šmíd, CSc., učo 1084. Changed: 6/7/2007 09:03. |
Abstract |
---|
We use some recent techniques from process algebra to draw several conclusions about the well studied class of ping-pong protocols introduced by Dolev and Yao. In particular we show that all nontrivial properties, including reachability and equivalence checking wrt. the whole van Glabbeek's spectrum, become undecidable for a very simple recursive extension of the protocol. The result holds even if no nondeterministic choice operator is allowed. We also show that the extended calculus is capable of an implicit description of the active intruder, including full analysis and synthesis of messages in the sense of Amadio, Lugiez and Vanackere. We conclude by showing that reachability analysis for a replicative variant of the protocol becomes decidable. |
Abstract (in Czech) |
---|
We use some recent techniques from process algebra to draw several conclusions about the well studied class of ping-pong protocols introduced by Dolev and Yao. In particular we show that all nontrivial properties, including reachability and equivalence checking wrt. the whole van Glabbeek's spectrum, become undecidable for a very simple recursive extension of the protocol. The result holds even if no nondeterministic choice operator is allowed. We also show that the extended calculus is capable of an implicit description of the active intruder, including full analysis and synthesis of messages in the sense of Amadio, Lugiez and Vanackere. We conclude by showing that reachability analysis for a replicative variant of the protocol becomes decidable. |
Links | |
---|---|
GA201/03/1161, research and development project | Name: Verifikace nekonečně stavových systémů |
Investor: Czech Science Foundation, Verification of infinite-state systems | |
MSM0021622419, plan (intention) | Name: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems | |
1M0545, research and development project | Name: Institut Teoretické Informatiky |
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science |
PrintDisplayed: 1/9/2024 01:17