Abstract
Recently, opacity has proved a promising technique for describing security properties. Much of the work has been couched in terms of Petri nets. Here, we extend the notion of opacity to the model of labelled transition systems and generalise opacity in order to better represent concepts from the literature on information flow. In particular, we establish links between opacity and the information flow concepts of anonymity and non-inference. We also investigate ways of verifying opacity when working with Petri nets. Our work is illustrated by an example modelling requirements upon a simple voting system.
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.
Similar content being viewed by others
References
Abadi, M., Cortier, V.: Deciding Knowledge in Security Protocols under Equational Theories. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 46–58. Springer, Heidelberg (2004)
Abadi, M., Rogaway, P.: Reconciling two Views of Cryptography (The computational soundness of formal encryption). In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, p. 3. Springer, Heidelberg (2000)
Bieber, P.: A Logic of Communication in a Hostile Environment. In: CSFW (1990)
Bryans, J.W., Koutny, M., Ryan, P.Y.A.: Modelling Opacity using Petri Nets. ENTCS 121 (2005)
Bryans, J.W., Koutny, M., Ryan, P.Y.A.: Modelling Dynamic Opacity using Petri Nets with Silent Actions. In: FAST (2004)
Bryans, J.W., Koutny, M., Mazaré, L., Ryan, P.Y.A.: Opacity Generalised to Transition Systems. CS-TR 868, University of Newcastle (2004), http://www.cs.ncl.ac.uk/research/pubs/trs/abstract.php?number=868
Dolev, D., Yao, A.C.: On the Security of Public Key Protocols. IEEE Transactions on Information Theory 29 (1983)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Finkel, A.: The Minimal Coverability Graph for Petri Nets. In: Rozenberg, G. (ed.) APN 1993. LNCS, vol. 674. Springer, Heidelberg (1993)
Focardi, R., Gorrieri, R.: A Taxonomy of Trace-Based Security Properties for CCS. In: CSFW (1994)
Focardi, R., Gorrieri, R.: Classification of Security Properties: Information flow. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, p. 331. Springer, Heidelberg (2001)
Glasgow, J., Macewen, G., Panangaden, P.: A Logic for Reasoning about Security. ACM Transactions on Computer Systems 10 (1992)
Lakhnech, Y., Mazaré, L.: Probabilistic Opacity for a Passive Adversary and its Application to Chaum’s Voting Scheme. Verimag Technical Report 2005-04 (2005)
Halpern, J.Y., O’Neill, K.: Anonymity and Information Hiding in Multiagent Systems. In: CSFW (2003)
Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and Verifying Security Protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 131–160. Springer, Heidelberg (2000)
Mazaré, L.: Using Unification For Opacity Properties. In: WITS (2004)
Moser, L.: A Logic of Knowledge and Belief for Reasoning about Security. In: CSFW (1989)
Nabialek, W., Niewiadomski, A., Penczek, W., Polórla, A., Szreter, M.: Verics 2004: A Model Checker of Real-Time and Multi-agent Systems. In: CS&P (2004)
O’Halloran, C.: A Calculus of Information Flow. In: ESORICS (1990)
Raimondi, F., Lomuscio, A.: Verification of Multiagent Systems via Ordered Binary Decision Diagrams: an Algorithm and its Implementation. TR-04-01, King’s College (2004)
Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol.1491,1492. Springer, Heidelberg (1998)
Ryan, P.Y.A.: Mathematical Models of Computer Security. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, p. 1. Springer, Heidelberg (2001)
Schneider, S., Sidiropoulos, A.: CSP and Anonymity. In: ESORICS (1996)
van Otterloo, S., van der Hoek, W., Woolridge, M.: Model Checking a Knowledge Exchange Scenario. In: IJCAI (2003)
Time Petri Net Analyzer (2004), http://www.laas.fr/tina/
van der Hoek, W., Lomuscio, A.: A Logic for Ignorance. ENTCS 85 (2004)
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
Bryans, J.W., Koutny, M., Mazaré, L., Ryan, P.Y.A. (2006). Opacity Generalised to Transition Systems. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds) Formal Aspects in Security and Trust. FAST 2005. Lecture Notes in Computer Science, vol 3866. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11679219_7
Download citation
DOI: https://doi.org/10.1007/11679219_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-32628-1
Online ISBN: 978-3-540-32629-8
eBook Packages: Computer ScienceComputer Science (R0)