Abstract
Refinement type systems have proved very effective for security policy verification in distributed authorization systems. In earlier work [12], we have proposed an extension of existing refinement typing techniques to exploit sub-structural logics and affine typing in the analysis of resource aware authorization, with policies predicating over access counts, usage bounds and resource consumption. In the present paper, we show that the invariants that we enforced by means of ad-hoc typing mechanisms in our initial proposal can be internalized, and expressed directly as proof obligations for the underlying affine logical system. The new characterization leads to a more general, modular design of the system, and is effective in the analysis of interesting classes of authentication protocols and authorization systems.
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.
References
Abadi, M.: Secrecy by typing in security protocols. Journal of the ACM 46(5), 749–786 (1999)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th Symposium on Principles of Programming Languages (POPL), pp. 104–115. ACM Press (2001)
Abadi, M.: Logic in access control. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 228–233. IEEE Computer Society Press (2003)
Backes, M., Hriţcu, C., Maffei, M.: Type-checking zero-knowledge. In: 15th ACM Conference on Computer and Communications Security (CCS 2008), pp. 357–370. ACM Press (2008)
Bauer, L., Jia, L., Sharma, D.: Constraining credential usage in logic-based access control. In: Proc. 23rd IEEE Symposium on Computer Security Foundations (CSF), pp. 154–168. IEEE Computer Society Press (2010)
Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: Proc. 21st IEEE Symposium on Computer Security Foundations (CSF), pp. 17–32. IEEE Computer Society Press (2008)
Bhargavan, K., Fournet, C., Gordon, A.D.: Modular verification of security protocol code by typing. In: Proc. 37th Symposium on Principles of Programming Languages (POPL), pp. 445–456. ACM (2010)
Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: Hermenegildo, M., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342–359. Springer, Heidelberg (2002)
Bugliesi, M., Focardi, R., Maffei, M.: Compositional analysis of authentication protocols. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 140–154. Springer, Heidelberg (2004)
Bugliesi, M., Focardi, R., Maffei, M.: Analysis of Typed Analyses of Authentication Protocols. In: Proc. 18th IEEE Computer Security Foundations Workshop (CSFW), pp. 112–125. IEEE Computer Society Press (2005)
Bugliesi, M., Focardi, R., Maffei, M.: Dynamic types for authentication. Journal of Computer Security 15(6), 563–617 (2007)
Bugliesi, M., Calzavara, S., Eigner, F., Maffei, M.: Resource-aware authorization policies for statically typed cryptographic protocols. In: Proc. 24th IEEE Computer Security Foundations Symposium (CSF), pp. 83–98 (2011)
Focardi, R., Maffei, M.: Types for security protocols. In: Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series, vol. 5, ch. 7, pp. 143–181. IOS Press (2011)
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 141–156. Springer, Heidelberg (2005)
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization in distributed systems. In: Proc. 20th IEEE Symposium on Computer Security Foundations (CSF), pp. 31–45. IEEE Computer Society Press (2007)
Freeman, T., Pfenning, F.: Refinement types for ML. In: Wise, D.S. (ed.) PLDI, pp. 268–277. ACM (1991)
Girard, J.Y.: Linear logic: its syntax and semantics. In: Advances in Linear Logic. London Mathematical Society Lecture Note Series, vol. 22, pp. 3–42 (1995)
Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. Journal of Computer Security 11(4), 451–519 (2003)
Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. Journal of Computer Security 12(3), 435–484 (2004)
Haack, C., Jeffrey, A.: Timed spi-calculus with types for secrecy and authenticity. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 202–216. Springer, Heidelberg (2005)
Haack, C., Jeffrey, A.: Pattern-matching spi-calculus. Information and Computation 204(8), 1195–1263 (2006)
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems 21(5), 914–947 (1999)
Lowe, G.: A Hierarchy of Authentication Specifications. In: Proc. 10th IEEE Computer Security Foundations Workshop (CSFW), pp. 31–44. IEEE Computer Society Press (1997)
Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proc. of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 213–225. ACM Press (2003)
Troelstra, A.S.: Lectures on linear logic. CSLI Stanford. Lecture Notes Series, vol. 29 (1992)
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
Bugliesi, M., Calzavara, S., Eigner, F., Maffei, M. (2013). Affine Refinement Types for Authentication and Authorization. In: Palamidessi, C., Ryan, M.D. (eds) Trustworthy Global Computing. TGC 2012. Lecture Notes in Computer Science, vol 8191. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41157-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-41157-1_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41156-4
Online ISBN: 978-3-642-41157-1
eBook Packages: Computer ScienceComputer Science (R0)