{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:44:13Z","timestamp":1725576253949},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540344513"},{"type":"electronic","value":"9783540344520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11759683_7","type":"book-chapter","created":{"date-parts":[[2006,6,1]],"date-time":"2006-06-01T18:03:34Z","timestamp":1149185014000},"page":"106-124","source":"Crossref","is-referenced-by-count":15,"title":["Security Protocols Verification in Abductive Logic Programming: A Case Study"],"prefix":"10.1007","author":[{"given":"Marco","family":"Alberti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Federico","family":"Chesani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Gavanelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Evelina","family":"Lamma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paola","family":"Mello","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Torroni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45584-1_1","volume-title":"Engineering Societies in the Agents World II","author":"P. Davidsson","year":"2002","unstructured":"Davidsson, P.: Categories of artificial societies. In: Omicini, A., Petta, P., Tolksdorf, R. (eds.) ESAW 2001. LNCS (LNAI), vol.\u00a02203, pp. 1\u20139. Springer, Heidelberg (2002)"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1145\/544862.544873","volume-title":"Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), Part II","author":"F. Guerin","year":"2002","unstructured":"Guerin, F., Pitt, J.: Proving properties of open agent systems. In: Castelfranchi, C., Lewis Johnson, W. (eds.) Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), Part II, Bologna, Italy, pp. 557\u2013558. ACM Press, New York (2002)"},{"key":"7_CR3","unstructured":"Societies Of ComputeeS (SOCS): a computational logic model for the description, analysis and verification of global and open societies of heterogeneous computees. IST-2001-32530 (2001), Home Page: http:\/\/lia.deis.unibo.it\/Research\/SOCS\/"},{"key":"7_CR4","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-45023-8_20","volume-title":"Multi-Agent Systems and Applications III","author":"M. Alberti","year":"2003","unstructured":"Alberti, M., Ciampolini, A., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: A social ACL semantics by deontic constraints. In: Ma\u0159\u00edk, V., M\u00fcller, J.P., P\u011bchou\u010dek, M. (eds.) CEEMAS 2003. LNCS (LNAI), vol.\u00a02691, pp. 204\u2013213. Springer, Heidelberg (2003)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Specification and verification of agent interactions using social integrity constraints. Electronic Notes in Theoretical Computer Science\u00a085 (2003)","DOI":"10.1016\/S1571-0661(05)82605-2"},{"key":"7_CR6","unstructured":"The socs protocol repository (2005) Available at: http:\/\/lia.deis.unibo.it\/research\/socs\/partners\/societies\/protocols.html"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. Needham","year":"1978","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM\u00a021, 993\u2013999 (1978)","journal-title":"Communications of the ACM"},{"key":"7_CR8","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Shroeder public-key protocol using CSP and FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS (LNAI), vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"D.E. Denning","year":"1981","unstructured":"Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM\u00a024, 533\u2013536 (1981)","journal-title":"Communications of the ACM"},{"key":"7_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-39853-0_24","volume-title":"AI*IA 2003: Advances in Artificial Intelligence","author":"M. Alberti","year":"2003","unstructured":"Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: An Abductive Interpretation for Open Societies. In: Cappelli, A., Turini, F. (eds.) AI*IA 2003. LNCS (LNAI), vol.\u00a02829, pp. 287\u2013299. Springer, Heidelberg (2003)"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19-20","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint logic programming: a survey. Journal of Logic Programming\u00a019-20, 503\u2013582 (1994)","journal-title":"Journal of Logic Programming"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"719","DOI":"10.1093\/logcom\/2.6.719","volume":"2","author":"A.C. Kakas","year":"1993","unstructured":"Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive Logic Programming. Journal of Logic and Computation\u00a02, 719\u2013770 (1993)","journal-title":"Journal of Logic and Computation"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a029, 198\u2013207 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"7_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/11558590_14","volume-title":"AI*IA 2005: Advances in Artificial Intelligence","author":"M. Alberti","year":"2005","unstructured":"Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: The SCIFF abductive proof-procedure. In: Bandini, S., Manzoni, S. (eds.) AI*IA 2005. LNCS (LNAI), vol.\u00a03673, pp. 135\u2013147. Springer, Heidelberg (2005)"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0743-1066(97)00026-5","volume":"33","author":"T.H. Fung","year":"1997","unstructured":"Fung, T.H., Kowalski, R.A.: The IFF proof procedure for abductive logic programming. Journal of Logic Programming\u00a033, 151\u2013165 (1997)","journal-title":"Journal of Logic Programming"},{"key":"7_CR16","unstructured":"Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: On the automatic verification of interaction protocols using g-SCIFF. Technical Report DEIS-LIA-04-004, University of Bologna (Italy), LIA Series no.\u00a072 (2005)"},{"key":"7_CR17","unstructured":"Cox, B., Tygar, J., Sirbu, M.: Netbill security and transaction protocol. In: Proceedings of the First USENIX Workshop on Electronic Commerce, New York (1995)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-45619-8_3","volume-title":"Logic Programming","author":"A. Russo","year":"2002","unstructured":"Russo, A., Miller, R., Nuseibeh, B., Kramer, J.: An abductive approach for analysing event-based requirements specifications. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol.\u00a02401, pp. 22\u201337. Springer, Heidelberg (2002)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-39650-5_15","volume-title":"Computer Security \u2013 ESORICS 2003","author":"D.A. Basin","year":"2003","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f2, L.: An on-the-fly model-checker for security protocol analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol.\u00a02808, pp. 253\u2013270. Springer, Heidelberg (2003)"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/888251.888252","volume-title":"PPDP 2003: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B.: Automatic verification of cryptographic protocols: a logic programming approach. In: PPDP 2003: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pp. 1\u20133. ACM Press, New York (2003)"},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/1044731.1044735","volume":"52","author":"M. Abadi","year":"2005","unstructured":"Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM\u00a052, 102\u2013146 (2005)","journal-title":"J. ACM"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45789-5_25","volume-title":"Static Analysis","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B.: From secrecy to authenticity in security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 342\u2013359. Springer, Heidelberg (2002)"},{"key":"7_CR23","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/978-3-540-30227-8_51","volume-title":"Logics in Artificial Intelligence","author":"A. Armando","year":"2004","unstructured":"Armando, A., Compagna, L., Lierler, Y.: Automatic compilation of protocol insecurity problems into logic programming. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 617\u2013627. Springer, Heidelberg (2004)"},{"key":"7_CR24","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"7_CR25","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/501983.502007","volume-title":"CCS 2001, Proceedings of the 8th ACM Conference on Computer and Communications Security","author":"J.K. Millen","year":"2001","unstructured":"Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: CCS 2001, Proceedings of the 8th ACM Conference on Computer and Communications Security, pp. 166\u2013175. ACM press, New York (2001)"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/3-540-45789-5_24","volume-title":"Static Analysis","author":"R. Corin","year":"2002","unstructured":"Corin, R., Etalle, S.: An improved constraint-based system for the verification of security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 326\u2013341. Springer, Berlin (2002)"},{"key":"7_CR27","first-page":"192","volume-title":"CSFW 1999: Proceedings of the 1999 IEEE Computer Security Foundations Workshop","author":"D.X. Song","year":"1999","unstructured":"Song, D.X.: Athena: a new efficient automatic checker for security protocol analysis. In: CSFW 1999: Proceedings of the 1999 IEEE Computer Security Foundations Workshop, Washington, DC, USA, p. 192. IEEE Computer Society, Los Alamitos (1999)"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/11759683_11","volume-title":"Engineering Societies in the Agents World VI","author":"A. \u00d6zkohen","year":"2006","unstructured":"\u00d6zkohen, A., Yolum, P.: Predicting exceptions in agent-based supply-chains. In: Dikenelli, O., Gleizes, M.-P., Ricci, A. (eds.) ESAW 2005. LNCS, vol.\u00a03963, pp. 168\u2013183. Springer, Heidelberg (2006)"},{"key":"7_CR29","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/544862.544867","volume-title":"Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), Part II","author":"P. Yolum","year":"2002","unstructured":"Yolum, P., Singh, M.: Flexible protocol specification and execution: applying event calculus planning using commitments. In: Castelfranchi, C., Lewis Johnson, W. (eds.) Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), Part II, Bologna, Italy, pp. 527\u2013534. ACM Press, New York (2002)"},{"key":"7_CR30","first-page":"3902","volume":"E74","author":"S. Yamaguchi","year":"1991","unstructured":"Yamaguchi, S., Okayama, K., Miyahara, H.: The design and implementation of an authentication system for the wide area distributed environment. IEICE Transactions on Information and Systems\u00a0E74, 3902\u20133909 (1991)","journal-title":"IEICE Transactions on Information and Systems"}],"container-title":["Lecture Notes in Computer Science","Engineering Societies in the Agents World VI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11759683_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:04:38Z","timestamp":1619507078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11759683_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540344513","9783540344520"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/11759683_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}