Document Open Access Logo

Speed Me up If You Can: Conditional Lower Bounds on Opacity Verification

Authors Jiří Balun , Tomáš Masopust , Petr Osička

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2023.16.pdf
  • Filesize: 0.98 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Finite automata
  • opacity
  • fine-grained complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Opacity is a property of privacy and security applications asking whether, given a system model, a passive intruder that makes online observations of system’s behaviour can ascertain some "secret" information of the system. Deciding opacity is a PSpace-complete problem, and hence there are no polynomial-time algorithms to verify opacity under the assumption that PSpace differs from PTime. This assumption, however, gives rise to a question whether the existing exponential-time algorithms are the best possible or whether there are faster, sub-exponential-time algorithms. We show that under the (Strong) Exponential Time Hypothesis, there are no algorithms that would be significantly faster than the existing algorithms. As a by-product, we obtained a new conditional lower bound on the time complexity of deciding universality (and therefore also inclusion and equivalence) for nondeterministic finite automata.

Cite As Get BibTex

Jiří Balun, Tomáš Masopust, and Petr Osička. Speed Me up If You Can: Conditional Lower Bounds on Opacity Verification. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.MFCS.2023.16

Author Details

Jiří Balun
  • Faculty of Science, Palacky University Olomouc, Czech Republic
Tomáš Masopust
  • Faculty of Science, Palacky University Olomouc, Czech Republic
Petr Osička
  • Faculty of Science, Palacky University Olomouc, Czech Republic

Funding

  • Balun, Jiří: Supported by IGA PrF 2023 026.

Acknowledgements

We acknowledge valuable comments and suggestions of anonymous referees.

References

  1. Rajeev Alur, Pavol Černý, and Steve Zdancewic. Preserving secrecy under refinement. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, International Colloquium on Automata, Languages and Programming, ICALP 2006, Venice, Italy, July 10-14, 2006, volume 4052 of Lecture Notes in Computer Science, pages 107-118. Springer, 2006. URL: https://doi.org/10.1007/11787006_10.
  2. Peter R. J. Asveld and Anton Nijholt. The inclusion problem for some subclasses of context-free languages. Theoretical Computer Science, 230(1-2):247-256, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00113-9.
  3. Éric Badouel, Marek A. Bednarczyk, Andrzej M. Borzyszkowski, Benoît Caillaud, and Philippe Darondeau. Concurrent secrets. Discrete Event Dynamic Systems, 17(4):425-446, 2007. URL: https://doi.org/10.1007/s10626-007-0020-5.
  4. Jiří Balun and Tomáš Masopust. On opacity verification for discrete-event systems. In IFAC World Congress, Berlin, Germany, July 11-17, 2020, pages 2105-2110, 2020. URL: https://doi.org/10.1016/j.ifacol.2020.12.2524.
  5. Jiří Balun and Tomáš Masopust. Comparing the notions of opacity for discrete-event systems. Discrete Event Dynamic Systems, 31(4):553-582, 2021. URL: https://doi.org/10.1007/s10626-021-00344-2.
  6. Jiří Balun and Tomáš Masopust. On transformations among opacity notions. In IEEE International Conference on Systems, Man, and Cybernetics, SMC 2022, Prague, Czech Republic, October 9-12, 2022, pages 3012-3017. IEEE, 2022. URL: https://doi.org/10.1109/SMC53654.2022.9945608.
  7. Jiří Balun, Tomáš Masopust, and Petr Osička. Speed me up if you can: Conditional lower bounds on opacity verification. CoRR, abs/2304.09920, 2023. URL: https://doi.org/10.48550/arXiv.2304.09920.
  8. Eike Best, Philippe Darondeau, and Roberto Gorrieri. On the decidability of non interference over unbounded Petri nets. In Konstantinos Chatzikokolakis and Véronique Cortier, editors, International Workshop on Security Issues in Concurrency, SecCo 2010, Paris, France, August 30, 2010, volume 51 of EPTCS, pages 16-33, 2010. URL: https://doi.org/10.4204/EPTCS.51.2.
  9. Jeremy W. Bryans, Maciej Koutny, Laurent Mazaré, and Peter Y. A. Ryan. Opacity generalised to transition systems. International Journal of Information Security, 7(6):421-435, 2008. URL: https://doi.org/10.1007/s10207-008-0058-x.
  10. Jeremy W. Bryans, Maciej Koutny, and Peter Y. A. Ryan. Modelling dynamic opacity using petri nets with silent actions. In Theodosis Dimitrakos and Fabio Martinelli, editors, Formal Aspects in Security and Trust: Second IFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust (FAST), an event of the 18th IFIP World Computer Congress, Toulouse, France, August 22-27, 2004, volume 173 of IFIP, pages 159-172. Springer, 2004. URL: https://doi.org/10.1007/0-387-24098-5_12.
  11. Jeremy W. Bryans, Maciej Koutny, and Peter Y.A. Ryan. Modelling opacity using Petri nets. Electronic Notes in Theoretical Computer Science, 121:101-115, 2005. Proceedings of the 2nd International Workshop on Security Issues with Petri Nets and other Computational Models (WISP 2004). URL: https://doi.org/10.1016/j.entcs.2004.10.010.
  12. Nadia Busi and Roberto Gorrieri. Structural non-interference in elementary and trace nets. Mathematical Structures in Computer Science, 19(6):1065-1090, 2009. URL: https://doi.org/10.1017/S0960129509990120.
  13. Franck Cassez, Jérémy Dubreil, and Hervé Marchand. Synthesis of opaque systems with static and dynamic masks. Formal Methods in System Design, 40(1):88-115, 2012. URL: https://doi.org/10.1007/s10703-012-0141-9.
  14. Roger Dingledine, Nick Mathewson, and Paul Syverson. Reputation in P2P anonymity systems. In Workshop on Economics of Peer-to-Peer Systems, P2P Econ 2003, Berkeley, CA, USA, June 5-6, 2003, 2003. Google Scholar
  15. Jeremy Dubreil, Philippe Darondeau, and Herve Marchand. Opacity enforcing control synthesis. In International Workshop on Discrete Event Systems, WODES 2008, Gothenburg, Sweden, May 28-30, 2008, pages 28-35. IEEE, 2008. URL: https://doi.org/10.1109/WODES.2008.4605918.
  16. Henning Fernau and Andreas Krebs. Problems on finite automata and the exponential time hypothesis. Algorithms, 10(1):24, 2017. URL: https://doi.org/10.3390/a10010024.
  17. R. Focardi and R. Gorrieri. A taxonomy of trace-based security properties for CCS. In Computer Security Foundations Workshop VII, Franconia, NH, USA, June 14-16, 1994, pages 126-136, 1994. URL: https://doi.org/10.1109/CSFW.1994.315941.
  18. Rômulo Meira Góes, Blake C. Rawlings, Nicholas Recker, Gregory Willett, and Stéphane Lafortune. Demonstration of indoor location privacy enforcement using obfuscation. IFAC-PapersOnLine, 51(7):145-151, 2018. URL: https://doi.org/10.1016/j.ifacol.2018.06.293.
  19. N. B. Hadj-Alouane, S. Lafrance, Feng Lin, J. Mullins, and M. M. Yeddes. On the verification of intransitive noninterference in mulitlevel security. IEEE Transactions on Systems, Man, and Cybernetics, Part B, 35(5):948-958, 2005. URL: https://doi.org/10.1109/TSMCB.2005.847749.
  20. Christoforos N. Hadjicostis. Estimation and Inference in Discrete Event Systems: A Model-Based Approach with Finite Automata. Communications and Control Engineering. Springer Cham, 2020. URL: https://doi.org/10.1007/978-3-030-30821-6.
  21. Timon Hertli. 3-SAT faster and simpler - unique-sat bounds for PPSZ hold in general. SIAM Journal on Computing, 43(2):718-729, 2014. URL: https://doi.org/10.1137/120868177.
  22. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to automata theory, languages, and computation. Pearson international edition. Addison-Wesley, third edition, 2007. Google Scholar
  23. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-SAT. Journal of Computer and System Sciences, 62(2):367-375, 2001. URL: https://doi.org/10.1006/jcss.2000.1727.
  24. Romain Jacob, Jean-Jacques Lesage, and Jean-Marc Faure. Overview of discrete event systems opacity: Models, validation, and quantification. Annual Reviews in Control, 41:135-146, 2016. URL: https://doi.org/10.1016/j.arcontrol.2016.04.015.
  25. Feng Lin. Diagnosability of discrete event systems and its applications. Discrete Event Dynamic Systems, 4(2):197-212, 1994. URL: https://doi.org/10.1007/BF01441211.
  26. Feng Lin. Opacity of discrete event systems and its applications. Automatica, 47(3):496-503, 2011. URL: https://doi.org/10.1016/j.automatica.2011.01.002.
  27. Feng Lin and Walter Murray Wonham. On observability of discrete-event systems. Information Sciences, 44(3):173-198, 1988. URL: https://doi.org/10.1016/0020-0255(88)90001-1.
  28. Tomáš Masopust. Complexity of deciding detectability in discrete event systems. Automatica, 93:257-261, 2018. URL: https://doi.org/10.1016/j.automatica.2018.03.077.
  29. Tomáš Masopust and Xiang Yin. Complexity of detectability, opacity and A-diagnosability for modular discrete event systems. Automatica, 101:290-295, 2019. URL: https://doi.org/10.1016/j.automatica.2018.12.019.
  30. Laurent Mazaré. Decidability of opacity with non-atomic keys. In Theodosis Dimitrakos and Fabio Martinelli, editors, Formal Aspects in Security and Trust: Second IFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust (FAST), an event of the 18th IFIP World Computer Congress, Toulouse, France, August 22-27, 2004, volume 173 of IFIP, pages 71-84. Springer, 2004. URL: https://doi.org/10.1007/0-387-24098-5_6.
  31. Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane. An improved exponential-time algorithm for k-SAT. Journal of the ACM, 52(3):337-364, 2005. URL: https://doi.org/10.1145/1066100.1066101.
  32. Michael K. Reiter and Aviel D. Rubin. Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security, 1(1):66-92, 1998. URL: https://doi.org/10.1145/290163.290168.
  33. Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, 2003. URL: https://doi.org/10.1109/JSAC.2002.806121.
  34. Anooshiravan Saboori. Verification and enforcement of state-based notions of opacity in discrete event systems. PhD thesis, University of Illinois at Urbana-Champaign, 2011. Google Scholar
  35. Anooshiravan Saboori and Christoforos N. Hadjicostis. Verification of infinite-step opacity and complexity considerations. IEEE Transactions on Automatic Control, 57(5):1265-1269, 2012. URL: https://doi.org/10.1109/TAC.2011.2173774.
  36. Anooshiravan Saboori and Christoforos N. Hadjicostis. Verification of initial-state opacity in security applications of discrete event systems. Information Sciences, 246:115-132, 2013. URL: https://doi.org/10.1016/j.ins.2013.05.033.
  37. Meera Sampath, Raja Sengupta, Stéphane Lafortune, Kasim Sinnamohideen, and Demosthenis Teneketzis. Diagnosability of discrete-event systems. IEEE Transactions on Automatic Control, 40(9):1555-1575, 1995. URL: https://doi.org/10.1109/9.412626.
  38. Steve A. Schneider and Abraham Sidiropoulos. CSP and anonymity. In Elisa Bertino, Helmut Kurth, Giancarlo Martella, and Emilio Montolivo, editors, European Symposium on Research in Computer Security, ESORICS 1996, Rome, Italy, September 25-27, 1996, volume 1146 of Lecture Notes in Computer Science, pages 198-218. Springer, 1996. URL: https://doi.org/10.1007/3-540-61770-1_38.
  39. Shaolong Shu, Feng Lin, and Hao Ying. Detectability of discrete event systems. IEEE Transactions on Automatic Control, 52(12):2356-2359, 2007. URL: https://doi.org/10.1109/TAC.2007.910713.
  40. N. J. A. Sloan. The on-line encyclopedia of integer sequences (OEIS), 2023. A123121. URL: https://oeis.org/A123121.
  41. N. J. A. Sloan. The on-line encyclopedia of integer sequences (OEIS), 2023. A001511. URL: https://oeis.org/A001511.
  42. Andrew Wintenberg, Matthew Blischke, Stéphane Lafortune, and Necmiye Ozay. A dynamic obfuscation framework for security and utility. In ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2022, Milano, Italy, May 4-6, 2022, pages 236-246. IEEE, 2022. URL: https://doi.org/10.1109/ICCPS54341.2022.00028.
  43. Yi-Chin Wu and Stéphane Lafortune. Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discrete Event Dynamic Systems, 23(3):307-339, 2013. URL: https://doi.org/10.1007/s10626-012-0145-z.
  44. Yi-Chin Wu, Vasumathi Raman, Blake C. Rawlings, Stéphane Lafortune, and Sanjit A. Seshia. Synthesis of obfuscation policies to ensure privacy and utility. Journal of Automated Reasoning, 60(1):107-131, 2018. URL: https://doi.org/10.1007/s10817-017-9420-x.
  45. Xiang Yin and Stéphane Lafortune. A new approach for the verification of infinite-step and K-step opacity using two-way observers. Automatica, 80:162-171, 2017. URL: https://doi.org/10.1016/j.automatica.2017.02.037.
  46. Aris Zakinthinos and E. Stewart Lee. A general theory of security properties. In IEEE Symposium on Security and Privacy, Oakland, CA, USA, May 4-7, 1997, pages 94-102. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/SECPRI.1997.601322.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact