Recursion vs. Replication in Simple Cryptographic Protocols

HUTTEL, Hans and Jiří SRBA. Recursion vs. Replication in Simple Cryptographic Protocols. Online. In Proceedings of 31st Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'05). Netherlands: Springer-Verlag, 2005. p. 175-184. [citováno 2024-04-24]

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

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