A Calculus for Modeling Floating Authorizations

  • Jovanka Pantović
  • Ivan ProkićEmail author
  • Hugo Torres Vieira
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10854)


Controlling resource usage in distributed systems is a challenging task given the dynamics involved in access granting. Consider, e.g., the setting of floating licenses where access can be granted if the request originates in a licensed domain and if the number of active users is within the license limits. Access granting in such scenarios is given in terms of floating authorizations, addressed in this paper as first class entities of a process calculus model, encompassing the notions of domain, accounting and delegation. We present the operational semantics of the model in two equivalent alternative ways, each informing on the specific nature of authorizations. We also introduce a typing discipline to single out systems that never get stuck due to lacking authorizations, addressing configurations where authorization assignment is not statically prescribed in the system specification.



We thank anonymous reviewers for useful remarks and suggestions. This work has been partially supported by the Ministry of Education and Science of the Republic of Serbia, project ON174026, and EU COST Action IC1405 (Reversible Computation).


  1. 1.
    Acciai, L., Boreale, M.: Spatial and behavioral types in the pi-calculus. Inf. Comput. 208(10), 1118–1153 (2010). Scholar
  2. 2.
    Armstrong, W.J., Nayar, N., Stamschror, K.P.: Management of a concurrent use license in a logically-partitioned computer. US Patent 6,959,291 (2005)Google Scholar
  3. 3.
    Baratti, P., Squartini, P.: License management system. US Patent 6,574,612 (2003)Google Scholar
  4. 4.
    Bodei, C., Dinh, V.D., Ferrari, G.L.: Checking global usage of resources handled with local policies. Sci. Comput. Program. 133, 20–50 (2017). Scholar
  5. 5.
    Das, A., Hoffmann, J., Pfenning, F.: Work analysis with resource-aware sessiontypes. CoRR abs/1712.08310 (2017).
  6. 6.
    Ferris, J.M., Riveros, G.E.: Offering additional license terms during conversion of standard software licenses for use in cloud computing environments. US Patent 9,053,472 (2015)Google Scholar
  7. 7.
    Freeman, T.S., Pfenning, F.: Refinement types for ML. In: Wise, D.S. (ed.) Proceedings of the PLDI 1991, pp. 268–277. ACM (1991).
  8. 8.
    Ghilezan, S., Jakšić, S., Pantović, J., Pérez, J.A., Vieira, H.T.: Dynamic role authorization in multiparty conversations. Formal Asp. Comput. 28(4), 643–667 (2016). Scholar
  9. 9.
    Giunti, M., Palamidessi, C., Valencia, F.D.: Hide and new in the pi-calculus. In: Proceedings of EXPRESS/SOS 2012, EPTCS, vol. 89, pp. 65–79 (2012).
  10. 10.
    Gorla, D., Pugliese, R.: Dynamic management of capabilities in a network aware coordination language. J. Log. Algebr. Program. 78(8), 665–689 (2009). Scholar
  11. 11.
    Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deniélou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1–3:36 (2016). Scholar
  12. 12.
    Kobayashi, N., Suenaga, K., Wischik, L.: Resource usage analysis for the p-calculus. Log. Methods Comput. Sci. 2(3) (2006).
  13. 13.
    Pantovic, J., Prokic, I., Vieira, H.T.: A calculus for modeling floating authorizations. CoRR abs/1802.05863 (2018).
  14. 14.
    Sangiorgi, D., Walker, D.: The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  15. 15.
    Swamy, N., Chen, J., Chugh, R.: Enforcing stateful authorization and information flow policies in Fine. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 529–549. Springer, Heidelberg (2010). Scholar
  16. 16.
    Vivas, J., Yoshida, N.: Dynamic channel screening in the higher order pi-calculus. Electr. Notes Theor. Comput. Sci. 66(3), 170–184 (2002). Scholar

Copyright information

© IFIP International Federation for Information Processing 2018

Authors and Affiliations

  1. 1.Faculty of Technical SciencesUniversity of Novi SadNovi SadSerbia
  2. 2.IMT School for Advanced Studies LuccaLuccaItaly

Personalised recommendations