Abstract
Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e. by adding an active intruder capable of storing all exchanged messages including full analysis and synthesis of messages) some verification problems become decidable. In particular we give an algorithm to decide control state reachability, a problem related to security properties like secrecy and authenticity. The proof is via a reduction to a new prefix rewriting model called Monotonic Set-extended Prefix rewriting (MSP). We demonstrate further applicability of the introduced model by encoding a fragment of the ccp (concurrent constraint programming) language into MSP.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. Nordic Journal of Computing 5(4), 267–303 (1998)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)
Amadio, R.M., Charatonik, W.: On name generation and set-based analysis in the Dolev-Yao model. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 499–514. Springer, Heidelberg (2002)
Amadio, R.M., Lugiez, D., Vanackère, V.: On the symbolic reduction of processes with cryptographic functions. Theoretical Computer Science 290(1), 695–740 (2002)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Büchi, J.R.: Regular canonical systems. Arch. Math. Logik u. Grundlagenforschung 6, 91–111 (1964)
Cécé, G., Finkel, A., Purushothaman Iyer, S.: Unreliable channels are easier to verify than perfect channels. Information and Computation 124(1), 20–31 (1996)
Comon, H., Cortier, V., Mitchell, J.: Tree automata with one memory, set constraints, and ping-pong protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 682–693. Springer, Heidelberg (2001)
Dolev, D., Even, S., Karp, R.M.: On the security of ping-pong protocols. Information and Control 55(1–3), 57–68 (1982)
Dolev, D., Yao, A.C.: On the security of public key protocols. Transactions on Information Theory IT-29(2), 198–208 (1983)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)
Hüttel, H., Srba, J.: Recursive ping-pong protocols. In: Proceedings of the 4th International Workshop on Issues in the Theory of Security (WITS 2004), pp. 129–140 (2004)
Hüttel, H., Srba, J.: Recursion vs. replication in simple cryptographic protocols. In: Vojtáš, P., Bieliková, M., Charron-Bost, B., Sýkora, O. (eds.) SOFSEM 2005. LNCS, vol. 3381, pp. 175–184. Springer, Heidelberg (2005)
Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)
Küsters, R.: On the decidability of cryptographic protocols with open-ended data structures. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 515–530. Springer, Heidelberg (2002)
Křetínský, M., Řehák, V., Strejček, J.: Extended process rewrite systems: Expressiveness and reachability. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 355–370. Springer, Heidelberg (2004)
Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of the 3rd Annual IEEE Symposium on Logic in Computer Science (LICS 1988), pp. 422–427. IEEE Computer Society Press, Los Alamitos (1988)
Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. TCS: Theoretical Computer Science 299 (2003)
Saraswat, V.A.: Concurrent Constraint Programming. MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delzanno, G., Esparza, J., Srba, J. (2006). Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. In: Graf, S., Zhang, W. (eds) Automated Technology for Verification and Analysis. ATVA 2006. Lecture Notes in Computer Science, vol 4218. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901914_31
Download citation
DOI: https://doi.org/10.1007/11901914_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47237-7
Online ISBN: 978-3-540-47238-4
eBook Packages: Computer ScienceComputer Science (R0)