Abstract
We present a formal language for specifying distributed authorization policies that communicate through insecure asynchronous media. The language allows us to write declarative authorization policies; the interface between policy decisions and communication events can be specified using guards and policy updates. The attacker, who controls the communication media, is modeled as a message deduction engine. We give trace semantics to communicating authorization policies, and formulate a generic reachability problem. We show that the reachability problem is decidable for a large class of practically-relevant policies specified in our formal language.
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., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Trans. Program. Lang. Syst. 15(4), 706–734 (1993)
Blaze, M., Feigenbaum, J., Lacy, J.: Decentralized trust management. In: IEEE Symposium on Security and Privacy, pp. 164–173. IEEE CS (1996)
DeTreville, J.: Binder, a logic-based security language. In: IEEE S&P, p. 105 (2002)
Becker, M., Fournet, C., Gordon, A.: Design and semantics of a decentralized authorization language. In: CSF 2007, pp. 3–15. IEEE Computer Society (2007)
Gurevich, Y., Neeman, I.: DKAL: Distributed-knowledge authorization language. In: CSF 2008, pp. 149–162. IEEE Computer Society (2008)
Hammer, E., et al.: The OAuth 2.0 authorization framework (2012); IETF
Frau, S., Torabi Dashti, M.: Integrated specification and verification of security protocols and policies. In: CSF, pp. 18–32. IEEE CS (2011)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. on Information Theory IT-29(2), 198–208 (1983)
Frau, S.: Analysis of Reachability Properties in Communicating Authorization Policies. PhD Thesis, ETH Zürich (November 2012)
Krishnan, R., Niu, J., Sandhu, R.S., Winsborough, W.H.: Stale-safe security properties for group-based secure information sharing. In: FMSE 2008, pp. 53–62 (2008)
Bertino, E., Samarati, P., Jajodia, S.: An extended authorization model for relational databases. IEEE Trans. Knowl. Data Eng. 9(1), 85–101 (1997)
Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cuéllar, J., Erzse, G., Frau, S., Minea, M., Mödersheim, S., von Oheimb, D., Pellegrino, G., Ponta, S.E., Rocchetto, M., Rusinowitch, M., Torabi Dashti, M., Turuani, M., Viganò, L.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012)
Griffiths, P., Wade, B.: An authorization mechanism for a relational database system. ACM Trans. Database Syst. 1(3), 242–255 (1976)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: CSFW 2001, p. 174. IEEE CS (2001)
Chaudhuri, A., Naldurg, P., Rajamani, S., Ramalingam, G., Velaga, L.: EON: modeling and analyzing dynamic access control systems with logic programs. In: ACM CCS 2008, pp. 381–390. ACM (2008)
Dougherty, D., Fisler, K., Krishnamurthi, S.: Specifying and reasoning about dynamic access-control policies. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 632–646. Springer, Heidelberg (2006)
Garg, D., Pfenning, F.: Stateful authorization logic: In: Cuellar, J., Lopez, J., Barthe, G., Pretschner, A. (eds.) STM 2010. LNCS, vol. 6710, pp. 210–225. Springer, Heidelberg (2011)
Li, N., Tripunitara, M.V.: Security analysis in role-based access control. ACM Trans. Inf. Syst. Secur. 9(4), 391–420 (2006)
Becker, M., Nanz, S.: A logic for state-modifying authorization policies. ACM Trans. Inf. Syst. Secur. 13(3) (2010)
Becker, M.Y.: Specification and analysis of dynamic authorisation policies. In: CSF, pp. 203–217. IEEE Computer Society (2009)
Guttman, J.D., Thayer, F.J., Carlson, J.A., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Trust management in strand spaces: A rely-guarantee method. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 325–339. Springer, Heidelberg (2004)
Fournet, C., Gordon, A., Maffeis, S.: A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29(5) (2007)
Barletta, M., Ranise, S., Viganò, L.: A declarative two-level framework to specify and verify workflow and authorization policies in service-oriented architectures. Service Oriented Computing and Applications 5(2), 105–137 (2011)
Bansal, C., Bhargavan, K., Maffeis, S.: Discovering concrete attacks on website authorization by formal analysis (2012); to appear in CSF 2012
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Frau, S., Torabi Dashti, M. (2013). Analysis of Communicating Authorization Policies. In: Jøsang, A., Samarati, P., Petrocchi, M. (eds) Security and Trust Management. STM 2012. Lecture Notes in Computer Science, vol 7783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38004-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-38004-4_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38003-7
Online ISBN: 978-3-642-38004-4
eBook Packages: Computer ScienceComputer Science (R0)