Recursive Ping-Pong Protocols

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

HUTTEL Hans SRBA Jiří

Year of publication 2004
Type Article in Proceedings
Conference Proceedings of 4th International Workshop on Issues in the Theory of Security (WITS'04)
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.brics.dk/~srba/publ.html
Field Informatics
Keywords cryptographic protocols; automated verification; decidability
Description This paper introduces a process calculus with recursion which allows us to express an unbounded number of runs of the ping-pong protocols introduced by Dolev and Yao. We study the decidability issues associated with two common approaches to checking security properties, namely reachability analysis and bisimulation checking. Our main result is that our channel-free and memory-less calculus is Turing powerful, assuming that at least three principals are involved. We also investigate the expressive power of the calculus in the case of two participants. Here, our main results are that reachability and, under certain conditions, also strong bisimilarity become decidable.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.