{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T16:29:13Z","timestamp":1791217753909,"version":"4.1.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2007,8,2]],"date-time":"2007-08-02T00:00:00Z","timestamp":1186012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2007,8,2]]},"abstract":"<jats:p>Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs in particular can express policies in a simple, abstract manner.<\/jats:p>\n          <jats:p>We consider the problem of checking whether a distributed implementation based on communication channels and cryptography complies with a logical authorization policy. We formalize authorization policies and their connection to code by embedding logical predicates and claims within a process calculus. We formulate policy compliance operationally by composing a process model of the distributed system with an arbitrary opponent process. Moreover, we propose a dependent type system for verifying policy compliance of implementation code. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.<\/jats:p>","DOI":"10.1145\/1275497.1275500","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T13:44:55Z","timestamp":1189777495000},"page":"25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["A type discipline for authorization policies"],"prefix":"10.1145","volume":"29","author":[{"given":"C\u00e9dric","family":"Fournet","sequence":"first","affiliation":[{"name":"Microsoft Research, Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sergio","family":"Maffeis","sequence":"additional","affiliation":[{"name":"Imperial College London, London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2007,8,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/324133.324266"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/353677.353678"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155225"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009672"},{"key":"e_1_2_1_6_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 9th International Static Analysis Symposium (SAS)","author":"Blanchet B.","unstructured":"Blanchet , B. 2002. From secrecy to authenticity in security protocols . In Proceedings of the 9th International Static Analysis Symposium (SAS) . Lecture Notes in Computer Science , vol. 2477 . Springer , 342--359. Blanchet, B. 2002. From secrecy to authenticity in security protocols. In Proceedings of the 9th International Static Analysis Symposium (SAS). Lecture Notes in Computer Science, vol. 2477. Springer, 342--359."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the IEEE 17th Symposium on Research in Security and Privacy. 164--173","author":"Blaze M.","unstructured":"Blaze , M. , Feigenbaum , J. , and Lacy , J . 1996. Decentralized trust management . In Proceedings of the IEEE 17th Symposium on Research in Security and Privacy. 164--173 . Blaze, M., Feigenbaum, J., and Lacy, J. 1996. Decentralized trust management. In Proceedings of the IEEE 17th Symposium on Research in Security and Privacy. 164--173."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009690"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/963778.963781"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science","volume":"3170","author":"Bugliesi M.","unstructured":"Bugliesi , M. , Colazzo , D. , and Crafa , S . 2004b. Type based discretionary access control . In Proceedings of the International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science , vol. 3170 . Springer, 225--239. Bugliesi, M., Colazzo, D., and Crafa, S. 2004b. Type based discretionary access control. In Proceedings of the International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 3170. Springer, 225--239."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.43410"},{"key":"e_1_2_1_12_1","unstructured":"ContentGuard. 2002. XrML 2.0 technical overview. http:\/\/www.xrml.org\/.  ContentGuard. 2002. XrML 2.0 technical overview. http:\/\/www.xrml.org\/."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science","volume":"1877","author":"De Nicola R.","unstructured":"De Nicola , R. , Ferrari , G. , and Pugliese , R . 2000. Programming access control: The KLAIM experience . In Proceedings of the International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science , vol. 1877 . Springer, 48--65. De Nicola, R., Ferrari, G., and Pugliese, R. 2000. Programming access control: The KLAIM experience. In Proceedings of the International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 1877. Springer, 48--65."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/829514.830540"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/794201.795162"},{"key":"e_1_2_1_17_1","volume-title":"Tech. Rep. MSR--TR--2005--01, Microsoft Research.","author":"Fournet C.","year":"2005","unstructured":"Fournet , C. , Gordon , A. D. , and Maffeis , S . 2005 a. A type discipline for authorization policies. Tech. Rep. MSR--TR--2005--01, Microsoft Research. Fournet, C., Gordon, A. D., and Maffeis, S. 2005a. A type discipline for authorization policies. Tech. Rep. MSR--TR--2005--01, Microsoft Research."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_11"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_17"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/959088.959090"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00333-X"},{"key":"e_1_2_1_22_1","volume-title":"Cryptyc: Cryptographic protocol type checker","author":"Gordon A. D.","year":"2002","unstructured":"Gordon , A. D. and Jeffrey , A . 2002 a. Cryptyc: Cryptographic protocol type checker . http:\/\/cryptyc.cs.depaul.edu\/. Gordon, A. D. and Jeffrey, A. 2002a. Cryptyc: Cryptographic protocol type checker. http:\/\/cryptyc.cs.depaul.edu\/."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Conference on Software Security, Theories and Systems. Lecture Notes in Computer Science","volume":"2609","author":"Gordon A. D.","unstructured":"Gordon , A. D. and Jeffrey , A . 2002b. Typing one-to-one and one-to-many correspondences in security protocols . In Proceedings of the Conference on Software Security, Theories and Systems. Lecture Notes in Computer Science , vol. 2609 . Springer, 270--282. Gordon, A. D. and Jeffrey, A. 2002b. Typing one-to-one and one-to-many correspondences in security protocols. In Proceedings of the Conference on Software Security, Theories and Systems. Lecture Notes in Computer Science, vol. 2609. Springer, 270--282."},{"key":"e_1_2_1_24_1","volume-title":"-Y","author":"Guelev D. P.","year":"2004","unstructured":"Guelev , D. P. , Ryan , M. D. , and Schobbens , P . -Y . 2004 . Model-Checking access control policies. In Proceedings of the 7th Information Security Conference (ISC). Lecture Notes in Computer Science, vol. 3225 . Springer . Guelev, D. P., Ryan, M. D., and Schobbens, P.-Y. 2004. Model-Checking access control policies. In Proceedings of the 7th Information Security Conference (ISC). Lecture Notes in Computer Science, vol. 3225. Springer."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 13th European Symposium on Programming (ESOP). Lecture Notes in Computer Science","volume":"2986","author":"Guttman J. D.","unstructured":"Guttman , J. D. , Thayer , F. J. , Carlson , J. A. , Herzog , J. C. , Ramsdell , J. D. , and Sniffen , B. T . 2004. Trust management in strand spaces: A rely-guarantee method . In Proceedings of the 13th European Symposium on Programming (ESOP). Lecture Notes in Computer Science , vol. 2986 . Springer, 340--354. Guttman, J. D., Thayer, F. J., Carlson, J. A., Herzog, J. C., Ramsdell, J. D., and Sniffen, B. T. 2004. Trust management in strand spaces: A rely-guarantee method. In Proceedings of the 13th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 2986. Springer, 340--354."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/882495.884431"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/359488.359493"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/775265.775268"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 16th IEEE Computer Security Foundation Workshop (CSFW). 89--103","author":"Li N.","unstructured":"Li , N. and Mitchell , J. C . 2003. Understanding SPKI\/SDSI using first-order logic . In Proceedings of the 16th IEEE Computer Security Foundation Workshop (CSFW). 89--103 . Li, N. and Mitchell, J. C. 2003. Understanding SPKI\/SDSI using first-order logic. In Proceedings of the 16th IEEE Computer Security Foundation Workshop (CSFW). 89--103."},{"key":"e_1_2_1_31_1","unstructured":"Martin-L\u00f6f P. 1984. Intuitionistic Type Theory. Bibliopolis.  Martin-L\u00f6f P. 1984. Intuitionistic Type Theory. Bibliopolis."},{"key":"e_1_2_1_32_1","volume-title":"Communicating and Mobile Systems: the &pi;-Calculus","author":"Milner R.","unstructured":"Milner , R. 1999. Communicating and Mobile Systems: the &pi;-Calculus . Cambridge University Press , New York . Milner, R. 1999. Communicating and Mobile Systems: the &pi;-Calculus. Cambridge University Press, New York."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363526"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950007002X"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW). IEEE Computer Society Press, 320--330","author":"Pottier F.","year":"2002","unstructured":"Pottier , F. 2002 . A simple view of type-secure information flow in the &pi;-calculus . In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW). IEEE Computer Society Press, 320--330 . Pottier, F. 2002. A simple view of type-secure information flow in the &pi;-calculus. In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW). IEEE Computer Society Press, 320--330."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/28659.28696"},{"key":"e_1_2_1_37_1","volume-title":"IFIP WG 107 International School on Foundations of Security Analysis and Design (FOSAD","author":"Samarati P.","year":"2000","unstructured":"Samarati , P. and de Capitani di Vimercati, S. 2001. Access control: Policies, models, and mechanisms . In IFIP WG 107 International School on Foundations of Security Analysis and Design (FOSAD 2000 ). Lecture Notes in Computer Science, vol. 2171 . Springer , 137--196. Samarati, P. and de Capitani di Vimercati, S. 2001. Access control: Policies, models, and mechanisms. In IFIP WG 107 International School on Foundations of Security Analysis and Design (FOSAD 2000). Lecture Notes in Computer Science, vol. 2171. Springer, 137--196."},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. 178--194","author":"Woo T.","unstructured":"Woo , T. and Lam , S . 1993. A semantic model for authentication protocols . In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. 178--194 . Woo, T. and Lam, S. 1993. A semantic model for authentication protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. 178--194."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275500","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1275497.1275500","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:30Z","timestamp":1750276830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275500"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8,2]]},"references-count":37,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,8,2]]}},"alternative-id":["10.1145\/1275497.1275500"],"URL":"https:\/\/doi.org\/10.1145\/1275497.1275500","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,8,2]]},"assertion":[{"value":"2007-08-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}