Abstract
Recent research has shown that it is possible to leverage general-purpose theorem proving techniques to develop powerful type systems for the verification of a wide range of security properties on application code. Although successful in many respects, these type systems fall short of capturing resource-conscious properties that are crucial in large classes of modern distributed applications. In this paper, we propose the first type system that statically enforces the safety of cryptographic protocol implementations with respect to authorization policies expressed in affine logic. Our type system draws on a novel notion of “exponential serialization” of affine formulas, a general technique to protect affine formulas from the effect of duplication. This technique allows to formulate an expressive logical encoding of the authentication mechanisms underpinning distributed resource-aware authorization policies. We further devise a sound and complete type checking algorithm. We discuss the effectiveness of our approach on a case study from the world of e-commerce protocols.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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 (2001)
Backes, M., Hriţcu, C., Maffei, M.: Union and Intersection Types for Secure Protocol Implementations. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 1–28. Springer, Heidelberg (2012)
Baillot, P., Hofmann, M.: Type Inference in Intuitionistic Linear Logic. In: PPDP 2010, pp. 219–230. ACM (2010)
Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement Types for Secure Implementations. TOPLAS 33(2), 8 (2011)
Bhargavan, K., Corin, R., Deniélou, P.M., Fournet, C., Leifer, J.J.: Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. In: CSF 2009, pp. 124–140. IEEE (2009)
Bhargavan, K., Fournet, C., Gordon, A.D.: Modular Verification of Security Protocol Code by Typing. In: POPL 2010, pp. 445–456. ACM (2010)
Bhargavan, K., Fournet, C., Gordon, A.D., Tse, S.: Verified Interoperable Implementations of Security Protocols. TOPLAS 31(1) (2008)
Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: OOPSLA 2007, pp. 301–320. ACM (2007)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: CSFW 2001, pp. 82–96. IEEE (2001)
Bowers, K.D., Bauer, L., Garg, D., Pfenning, F., Reiter, M.K.: Consumable Credentials in Linear-Logic-Based Access-Control Systems. In: NDSS 2007. Internet Society (2007)
Bugliesi, M., Focardi, R., Maffei, M.: Dynamic Types for Authentication. JCS 15(6), 563–617 (2007)
Bugliesi, M., Calzavara, S., Eigner, F., Maffei, M.: Logical Foundations of Secure Resource Management in Protocol Implementations (Long Version), http://www.lbs.cs.uni-saarland.de/affine-rcf/
Bugliesi, M., Calzavara, S., Eigner, F., Maffei, M.: Resource-Aware Authorization Policies for Statically Typed Cryptographic Protocols. In: CSF 2011, pp. 83–98. IEEE (2011)
Chapin, P.C., Skalka, C., Wang, X.S.: Authorization in Trust Management: Features and Foundations. ACM Computing Surveys 40(3) (2008)
Fournet, C., Kohlweiss, M., Strub, P.Y.: Modular Code-Based Cryptographic Verification. In: CCS 2011, pp. 341–350. ACM (2011)
Garg, D., Bauer, L., Bowers, K.D., Pfenning, F., Reiter, M.K.: A Linear Logic of Authorization and Knowledge. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 297–312. Springer, Heidelberg (2006)
Girard, J.Y.: Linear Logic: Its Syntax and Semantics. In: Advances in Linear Logic. London Mathematical Society LNS, vol. 22, pp. 1–42. Cambridge University Press (1995)
Gordon, A.D., Jeffrey, A.: Authenticity by Typing for Security Protocols. JCS 11(4), 451–519 (2003)
Gordon, A.D., Jeffrey, A.: Types and Effects for Asymmetric Cryptographic Protocols. JCS 12(3), 435–484 (2004)
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)
Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: ICFP 2003, pp. 213–225. ACM (2003)
Morris, J.: Protection in Programming Languages. CACM 16(1), 15–21 (1973)
Naden, K., Bocchino, R., Aldrich, J., Bierhoff, K.: A Type System for Borrowing Permissions. In: POPL 2012, pp. 557–570. ACM (2012)
Sumii, E., Pierce, B.: A Bisimulation for Dynamic Sealing. TCS 375(1-3), 169–192 (2007)
Sunshine, J., Naden, K., Stork, S., Aldrich, J., Tanter, E.: First-Class State Change in Plaid. In: OOPSLA 2011, pp. 713–732. ACM (2011)
Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure Distributed Programming with Value-Dependent Types. In: ICFP 2011, pp. 266–278. ACM (2011)
Tomura, N.: llprover - A Linear Logic Prover, http://bach.istc.kobe-u.ac.jp/llprover/
Tov, J.A., Pucella, R.: Stateful Contracts for Affine Types. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 550–569. Springer, Heidelberg (2010)
Troelstra, A.S.: Lectures on Linear Logic. CSLI Stanford, LNS, 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). Logical Foundations of Secure Resource Management in Protocol Implementations. In: Basin, D., Mitchell, J.C. (eds) Principles of Security and Trust. POST 2013. Lecture Notes in Computer Science, vol 7796. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36830-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-36830-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36829-5
Online ISBN: 978-3-642-36830-1
eBook Packages: Computer ScienceComputer Science (R0)