Discrete Event Dynamic Systems

, Volume 23, Issue 3, pp 307–339 | Cite as

Comparative analysis of related notions of opacity in centralized and coordinated architectures



Opacity is a confidentiality property that captures whether an intruder can infer a “secret” of a system based on its observation of the system behavior and its knowledge of the system’s structure. In this paper, we study four notions of opacity: language-based opacity, initial-state opacity, current-state opacity, and initial-and-final-state opacity. Initial-and-final-state opacity is a new opacity property introduced in this paper, motivated by secrecy considerations in anonymous network communications; the other three opacity properties have been studied in prior work. We investigate the relationships between these opacity properties. In this regard, a complete set of transformation algorithms among the four notions is provided. We also propose a new, more efficient test for initial-state opacity based on the use of reversed automata, and present a trellis-based test for the new property of initial-and-final state opacity. We then study the notions of initial-state opacity, current-state opacity, and initial-and-final-state opacity in the context of a new coordinated architecture where two intruders work as a team in order to infer the secret. In this architecture, the intruders have the capability of combining their respective state estimates at a coordinating node. In each case, a characterization of the corresponding notion of “joint opacity” and an algorithmic procedure for its verification are provided.


Language-based opacity Initial-state opacity Current-state opacity Initial-and-final-state opacity Coordinated architecture 



It is a pleasure to acknowledge useful discussions with Christoforos Hadjicostis and Hervé Marchand.


  1. Alur R, Černỳ P, Zdancewic S (2006) Preserving secrecy under refinement. Autom Lang Program 4052:107–118CrossRefGoogle Scholar
  2. Badouel E, Bednarczyk M, Borzyszkowski A, Caillaud B, Darondeau P (2007) Concurrent secrets. Discrete Event Dyn Syst 17(4):425–446MathSciNetMATHCrossRefGoogle Scholar
  3. Bryans J, Koutny M, Ryan PYA (2005) Modeling opacity using petri nets. ENTCS 121:101–115Google Scholar
  4. Bryans JW, Koutny M, Mazaré L, Ryan PYA (2008) Opacity generalized to transition systems. Int J Inf Secur 7(6):421–435CrossRefGoogle Scholar
  5. Cassandras CG, Lafortune S (2008) Introduction to discrete event systems. SpringerGoogle Scholar
  6. Cassez F, Dubreil J, Marchand H (2009) Dynamic observers for the synthesis of opaque systems. ATVA 5799:352–367Google Scholar
  7. Chaum D (1988) The dining cryptographers problem: unconditional sender and recipient untraceability. J Cryptol 1(1):65–75MathSciNetMATHCrossRefGoogle Scholar
  8. Chaum DL (1981) Untraceable electronic mail, return addresses, and digital pseudonyms. Commun ACM 24(2):84–90CrossRefGoogle Scholar
  9. Debouk R, Lafortune S, Teneketzis D (2000) Coordinated decentralized protocols for failure diagnosis of discrete event systems. Discrete Event Dyn Syst 10(1–2):33–86MathSciNetMATHCrossRefGoogle Scholar
  10. Dubreil J (2009) Monitoring and supervisory control for opacity properties. PhD thesis, Université de Rennes 1Google Scholar
  11. Dubreil J, Darondeau P, Marchand H (2008) Opacity enforcing control synthesis. In: Proc. of the 9th international workshop on discrete event systems, pp 28–35Google Scholar
  12. Dubreil J, Darondeau P, Marchand H (2010) Supervisory control for opacity. IEEE Trans Automat Contr 55(5):1089–1100MathSciNetCrossRefGoogle Scholar
  13. Dubreil J, Jéron T, Marchand H (2009) Monitoring confidentiality by diagnosis techniques. In: Proc. of the European control conference 2009Google Scholar
  14. Focardi R, Gorrieri R (1994) A taxonomy of trace-based security properties for CCS. In: Proc. of the computer security foundations workshop VII, pp 126–136Google Scholar
  15. Hadj-Alouane NB, Lafrance S, Lin F, Mullins J, Yeddes M (2005) On the verification of intransitive noninterference in mulitlevel security. IEEE Trans Syst Man Cybern Part B Cybern 35(5):948–958CrossRefGoogle Scholar
  16. Lin F (2011) Opacity of discrete event systems and its applications. Automatica 47(3):496–503MathSciNetMATHCrossRefGoogle Scholar
  17. Lin F, Wonham WM (1988) On observability of discrete-event systems. Inf Sci 44(3):173–198MathSciNetMATHCrossRefGoogle Scholar
  18. Mazaré L (2004) Using unification for opacity properties. Technical Report 24, Verimag Technical ReportGoogle Scholar
  19. Saboori A (2010) Verification and enforcement of state-based notions of opacity in discrete event systems. PhD thesis, University of Illinois, Urbana-ChampaignGoogle Scholar
  20. Saboori A, Hadjicostis CN (2007) Notions of security and opacity in discrete event systems. In: Proc. of the 46th IEEE conference on decision and control, pp 5056–5061Google Scholar
  21. Saboori A, Hadjicostis CN (2008) Opacity-enforcing supervisory strategies for secure discrete event systems. In: Proc. of 47th IEEE conference on decision and control, pp 889–894Google Scholar
  22. Saboori A, Hadjicostis CN (2008) Verification of initial-state opacity in security applications of des. In: Proc. of the 9th international workshop on discrete event systems, pp 328–333Google Scholar
  23. Saboori A, Hadjicostis CN (2009) Verification of k-step opacity and analysis of its complexity. In: Proc. of 48th IEEE conference on decision and control, pp 205–210Google Scholar
  24. Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis D (1995) Diagnosability of discrete-event systems. IEEE Trans Automat Contr 40(9):1555–1575MathSciNetMATHCrossRefGoogle Scholar
  25. Schneider S, Sidiropoulos A (1996) CSP and anonymity. ESORICS 96 1146:198–218CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  1. 1.Department of EECSUniversity of MichiganAnn ArborUSA

Personalised recommendations