{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T22:10:04Z","timestamp":1745964604974,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642365621"},{"type":"electronic","value":"9783642365638"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36563-8_10","type":"book-chapter","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T06:32:47Z","timestamp":1361514767000},"page":"139-154","source":"Crossref","is-referenced-by-count":4,"title":["dkal \u2009\u22c6\u2009: Constructing Executable Specifications of Authorization Protocols"],"prefix":"10.1007","author":[{"given":"Jean-Baptiste","family":"Jeannin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guido","family":"de Caso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuri","family":"Gurevich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Prasad","family":"Naldurg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"9","key":"10_CR1","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/1160074.1159839","volume":"41","author":"M. Abadi","year":"2006","unstructured":"Abadi, M.: Access control in a core calculus of dependency. SIGPLAN Not.\u00a041(9), 263\u2013273 (2006)","journal-title":"SIGPLAN Not."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A., Felten, E.: Proof-carrying authentication. In: CCS 1999, pp. 52\u201362. ACM (1999)","DOI":"10.1145\/319709.319718"},{"issue":"4","key":"10_CR3","doi-asserted-by":"crossref","first-page":"619","DOI":"10.3233\/JCS-2009-0364","volume":"18","author":"M. Becker","year":"2010","unstructured":"Becker, M., Fournet, C., Gordon, A.: SecPAL: Design and semantics of a decentralized authorization language. Journal of Computer Security\u00a018(4), 619\u2013665 (2010)","journal-title":"Journal of Computer Security"},{"key":"10_CR4","unstructured":"Beklemishev, L., Blass, A., Gurevich, Y.: What is the logic of information? (in preparation, 2012)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: CSF (2008)","DOI":"10.1109\/CSF.2008.27"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically verified implementations for TLS. In: ACM Conference on Computer and Communications Security, pp. 459\u2013468 (2008)","DOI":"10.1145\/1455770.1455828"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-30743-0_6","volume-title":"Correct Reasoning","author":"N. Bj\u00f8rner","year":"2012","unstructured":"Bj\u00f8rner, N., de Caso, G., Gurevich, Y.: From Primal Infon Logic with Individual Variables to Datalog. In: Erdem, E., Lee, J., Lierler, Y., Pearce, D. (eds.) Correct Reasoning. LNCS, vol.\u00a07265, pp. 72\u201386. Springer, Heidelberg (2012)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-28641-4_2","volume-title":"Principles of Security and Trust","author":"B. Blanchet","year":"2012","unstructured":"Blanchet, B.: Security Protocol Verification: Symbolic and Computational Models. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol.\u00a07215, pp. 3\u201329. Springer, Heidelberg (2012)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Blass, A., Gurevich, Y., Moskal, M., Neeman, I.: Evidential authorization. In: Nanz, S. (ed.) The Future of Software Engineering, pp. 73\u201399. Springer (2011)","DOI":"10.1007\/978-3-642-15187-3_5"},{"issue":"7","key":"10_CR10","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/1965724.1965741","volume":"54","author":"CACM Staff","year":"2011","unstructured":"CACM Staff: Microsoft\u2019s protocol documentation program: interoperability testing at scale. Commun. ACM 54(7), 51\u201357 (2011), http:\/\/doi.acm.org\/10.1145\/1965724.1965741","journal-title":"Commun. ACM"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/1380584.1380587","volume":"40","author":"P. Chapin","year":"2008","unstructured":"Chapin, P., Skalka, C., Wang, X.: Authorization in trust management: Features and foundations. ACM Computing Surveys (CSUR)\u00a040(3), 9 (2008)","journal-title":"ACM Computing Surveys (CSUR)"},{"issue":"1-3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1016\/S0304-3975(02)00333-X","volume":"300","author":"A.D. Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.: Typing correspondence assertions for communication protocols. Theor. Comput. Sci.\u00a0300(1-3), 379\u2013409 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Gurevich, Y., Neeman, I.: DKAL: Distributed-knowledge authorization language. In: 21st IEEE Computer Security Foundations Symposium, pp. 149\u2013162. IEEE (2008)","DOI":"10.1109\/CSF.2008.8"},{"key":"10_CR14","unstructured":"Gurevich, Y.: Evolving algebra 1993: Lipari guide. Specification and Validation Methods (1995)"},{"issue":"3","key":"10_CR15","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1016\/j.tcs.2005.06.017","volume":"343","author":"Y. Gurevich","year":"2005","unstructured":"Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of AsmL. Theor. Comput. Sci.\u00a0343(3), 370\u2013412 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Jeannin, J.B., de Caso, G., Chen, J., Gurevich, Y., Naldurg, P., Swamy, N.: dkal*: Constructing executable specifications of authorization Protocols (extended version). Tech. rep., Microsoft Research (2012), http:\/\/research.microsoft.com\/fstar","DOI":"10.1007\/978-3-642-36563-8_10"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Jia, L., Vaughan, J., Mazurak, K., Zhao, J., Zarko, L., Schorr, J., Zdancewic, S.: Aura: A programming language for authorization and audit. In: ICFP (2008)","DOI":"10.1145\/1411204.1411212"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Jim, T.: SD3: A trust management system with certified evaluation. In: Proceedings of the 2001 IEEE Symposium on Security and Privacy, S&P 2001, pp. 106\u2013115. IEEE (2001)","DOI":"10.1109\/SECPRI.2001.924291"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/978-3-540-88313-5_36","volume-title":"Computer Security - ESORICS 2008","author":"S. Maffeis","year":"2008","unstructured":"Maffeis, S., Abadi, M., Fournet, C., Gordon, A.D.: Code-Carrying Authorization. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol.\u00a05283, pp. 563\u2013579. Springer, Heidelberg (2008)"},{"key":"10_CR20","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"POPL 1997: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Sheard, T., Jones, S.P.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, Haskell 2002. ACM (2002)","DOI":"10.1145\/581690.581691"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: ICFP, pp. 266\u2013278 (2011)","DOI":"10.1145\/2034574.2034811"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Vaughan, J., Jia, L., Mazurak, K., Zdancewic, S.: Evidence-based audit. In: CSF 2008, pp. 163\u2013176. IEEE (2008)","DOI":"10.1109\/CSF.2008.24"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Wang, R., Chen, S., Wang, X., Qadeer, S.: How to shop for free online - security analysis of cashier-as-a-service based web stores. In: IEEE Symposium on Security and Privacy, pp. 465\u2013480 (2011)","DOI":"10.1109\/SP.2011.26"},{"key":"10_CR25","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/RISP.1993.287633","volume-title":"Proceedings of the 1993 IEEE Symposium on Security and Privacy, SP 1993","author":"T.Y.C. Woo","year":"1993","unstructured":"Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: Proceedings of the 1993 IEEE Symposium on Security and Privacy, SP 1993, pp. 178\u2013194. IEEE Computer Society, Washington, DC (1993), http:\/\/dl.acm.org\/citation.cfm?id=882489.884188"}],"container-title":["Lecture Notes in Computer Science","Engineering Secure Software and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36563-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T21:57:59Z","timestamp":1745963879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36563-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642365621","9783642365638"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36563-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}