In this paper we extend the notion of opacity, defined for discrete-event systems, to dense-time systems. We define the timed opacity problem for timed automata and study its algorithmic status. We show that for the very restrictive class of Event Recording Timed Automata, the opacity problem is already undecidable leaving no hope for an algorithmic solution to the opacity problem in dense-time.


Security Policy Dark Side Time Automaton Time Automaton Secret Location 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Rushby, J.: Noninterference, Transitivity and Channel-Control Security Policies. Technical report, SRI International (2005)Google Scholar
  2. 2.
    Mazaré, L.: Using unification for opacity properties. In: Proceedings of the 4th IFIP WG1.7 Workshop on Issues in the Theory of Security (WITS 2004), Barcelona, Spain, pp. 165–176 (2004)Google Scholar
  3. 3.
    Bryans, J., Koutny, M., Mazaré, L., Ryan, P.Y.A.: Opacity generalised to transition systems. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 81–95. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science (TCS) 126(2), 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Focardi, R., Gorrieri, R.: Classification of security properties (part I: Information flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Gardey, G., Mullins, J., Roux, O.H.: Non-interference control synthesis for security timed automata. In: 3rd International Workshop on Security Issues in Concurrency (SecCo 2005), San Francisco, USA. Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2005)Google Scholar
  7. 7.
    Benattar, G., Cassez, F., Lime, D., Roux, O.H.: Synthesis of Non-Interferent Timed Systems (submitted, 2009)Google Scholar
  8. 8.
    Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  9. 9.
    Bérard, B., Diekert, V., Gastin, P., Petit, A.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae 36(2–3), 145–182 (1998)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Alur, R., Fix, L., Henzinger, T.A.: Event clock automata: A determinizable class of timed automata. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 1–13. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  11. 11.
    Cassez, F., Roux, O.H.: Structural translation from time petri nets to timed automata. Journal of Software and Systems 79(10), 1456–1468 (2006)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Franck Cassez
    • 1
  1. 1.National ICT Australia & CNRSThe University of New South WalesSydneyAustralia

Personalised recommendations