×

Reachability results for timed automata with unbounded data structures. (English) Zbl 1214.68199

Summary: Systems of Data Management Timed Automata (SDMTAs) are networks of communicating timed automata with structures to store messages and functions to manipulate them. We prove the decidability of the reachability problem for a subclass of SDMTAs which assumes an unbounded knowledge, and we analyze the expressiveness of the model and the considered subclass. In particular, while SDMTAs can simulate a Turing machine, and hence the reachability problem is in general undecidable, the subclass for which reachability is decidable, when endowed with a concept of recognized language, accepts languages that are not regular. As an application, we model and analyze a variation of the Yahalom protocol.

MSC:

68Q45 Formal languages and automata
68Q05 Models of computation (Turing machines, etc.) (MSC2010)

Software:

Uppaal; Kronos
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The Spi calculus. In: 4th ACM Conference on Computer and Communications Security, pp. 36–47. ACM Press (1997)
[2] Abdullah, P.A., Jonsson, B.: Verifying networks of timed processes. In: Proceedings of TACAS’ 98, of LNCS, vol. 1384, pp. 298–312. Springer (1998)
[3] Alur R., Dill D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[4] Behrmann G., David A., Larsen K.G.: A tutorial on uppaal. Springer LNCS 3185, 200–236 (2004) · Zbl 1105.68350
[5] Berthomieu B., Diaz M.: Modeling and verification of time dependent systems using time petri nets. IEEE Trans. Softw. Eng. 17(3), 259–273 (1991) · Zbl 05113493 · doi:10.1109/32.75415
[6] Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: Proceedings Hybrid System II, Springer LNCS, vol. 999, pp. 64–85 (1995)
[7] Burrows, M., Abadi, M., Needham, R.: A logic for authentication. Technical Report 39, Digital Systems Research Center, Feb (1989) · Zbl 0687.68007
[8] Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed analysis of security protocols. Journal of Computer Security. A preliminary report appeared as CTIT Technichal Report TR–CTIT–05–14, University of Twente, The Netherlands (2005) (to appear)
[9] Cremers, C.J.F., Mauw, S., de Vink, E.P.: Defining authentication in a trace model. In: 1st International Workshop on Formal Aspects in Security and Trust (Fast 2003), pp. 131–145, Pisa, IITT-CNR technical report (2003)
[10] Dang Z.: Pushdown time automata: a binary reachability characterization and safety verification. Theor. Comp. Sci. 302, 93–121 (2003) · Zbl 1044.68085 · doi:10.1016/S0304-3975(02)00743-0
[11] Dolev D., Yao A.C.-C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983) · Zbl 0502.94005 · doi:10.1109/TIT.1983.1056650
[12] Focardi, R., Gorrieri, R., Martinelli, F.: Non interference for the analysis of cryptographic protocols. In: International Conference on Automata, Languages and Programming (ICALP’00) of LNCS, vol. 1853, pp. 354–372. Springer (2000) · Zbl 0973.94517
[13] Hoenicke J., Olderog E.R.: CSP-OZ-DC: a combination of specification techniques for processes, data and time. Nord. J. Comput. 9(4), 301–334 (2002) · Zbl 1088.68643
[14] Ibarra O.H., Su J.: Augmenting the discrete timed automaton with other data structures. Theor. Comput. Sci. 289, 191–204 (2002) · Zbl 1061.68094 · doi:10.1016/S0304-3975(01)00269-9
[15] Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: 14th Annual ACM Symposium on Theory of Computing, pp. 267–281. ACM Press (1982)
[16] Krcal, P., Yi, W.: Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. CAV’06 of LNCS, vol. 4144, pp. 249–262, Springer (2006) · Zbl 1188.68192
[17] Lanotte, R.: Expressive power of hybrid systems with real variables, integer variables and arrays. J of Automata, Languages and Combinatorics, (accepted for publication) · Zbl 1145.68462
[18] Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Timed automata with data structures for distributed systems design and analysis. In: 3nd International Conference on Software Engineering and Formal Methods (SEFM’05), pp. 44–53. IEEE Computer Society Press (2005) · Zbl 1272.68326
[19] Lowe, G.: A hierarchy of authentication specifications. In: 10th International Computer Security Foundations Workshop (CSFW’97), pp. 31–44. IEEE Computer Society Press (1997)
[20] Napoli M., Parente M., Peron A.: Specification and verification of protocols with time constraints. Electronic Notes Theor. Comput. Sci. 99, 205–227 (2004) · doi:10.1016/j.entcs.2004.02.009
[21] Paulson L.C.: Relations between secrets: two formal analyses of the Yahalom protocol. J. Comput. Secur. 9(3), 197–216 (2001)
[22] The Object-Z specification language. Kluwer Academic Publishers, Norwell (1999)
[23] Valero Ruiz, V., Cuartero Gomez, F., de Frutos-Escrig, D.: On non-decidability of reachability for timed-arc Petri nets. In: Proceedings 8th International Work. Petri Nets and Performance Models (PNPM’03) IEEE Computer Society Press, pp. 188–196 (1999)
[24] Wang J.: Timed Petri Nets: Theory and Application. Kluwer Academic Publishers, Dordrecht (1998) · Zbl 0924.68147
[25] Yovine S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. 1, 123–133 (1997) · Zbl 1060.68606 · doi:10.1007/s100090050009
[26] Zhou C., Hoare C.A.R., Ravn A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991) · Zbl 0743.68097 · doi:10.1016/0020-0190(91)90122-X
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.