{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:11:22Z","timestamp":1742962282732,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Attestation logics have been used for specifying systems with policies involving different principals. Cyberlogic is an attestation logic used for the specification of Evidential Transactions (ETs). In such transactions, evidence has to be provided supporting its validity with respect to given policies. For example, visa applicants may be required to demonstrate that they have sufficient funds to visit a foreign country. Such evidence can be expressed as a Cyberlogic proof, possibly combined with non-logical data (<jats:italic>e.g.<\/jats:italic>, a digitally signed document). A key issue is how to construct and communicate such evidence\/proofs. It turns out that attestation modalities are challenging to use established proof-theoretic methods such as focusing. Our first contribution is the refinement of Cyberlogic proof theory with knowledge operators which can be used to represent knowledge bases local to one or more principals. Our second contribution is the identification of an executable fragment of Cyberlogic, called Cyberlogic programs, enabling the specification of ETs. Our third contribution is a sound and complete proof system for Cyberlogic programs enabling proof search similar to search in logic programming. Our final contribution is a proof certificate format for Cyberlogic programs inspired by Foundational Proof Certificates as a means to communicate evidence and check its validity.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_14","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"234-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proof Search and Certificates for Evidential Transactions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4089-1218","authenticated-orcid":false,"given":"Vivek","family":"Nigam","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5145-9829","authenticated-orcid":false,"given":"Giselle","family":"Reis","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1351-1515","authenticated-orcid":false,"given":"Samar","family":"Rahmouni","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1405-2990","authenticated-orcid":false,"given":"Harald","family":"Ruess","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M.: Logic in Access Control. In: 18th IEEE Symposium on Logic in Computer Science (LICS) Proceedings. pp. 228\u2013233. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/LICS.2003.1210062","DOI":"10.1109\/LICS.2003.1210062"},{"issue":"4","key":"14_CR2","doi-asserted-by":"publisher","first-page":"706","DOI":"10.1145\/155183.155225","volume":"15","author":"M Abadi","year":"1993","unstructured":"Abadi, M., Burrows, M., Lampson, B.W., Plotkin, G.D.: A Calculus for Access Control in Distributed Systems. ACM Trans. Program. Lang. Syst. 15(4), 706\u2013734 (1993). https:\/\/doi.org\/10.1145\/155183.155225","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"14_CR3","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"JM Andreoli","year":"1992","unstructured":"Andreoli, J.M.: Logic Programming with Focusing Proofs in Linear Logic. Joural of Logic and Computation 2(3), 297\u2013347 (1992). https:\/\/doi.org\/10.1093\/logcom\/2.3.297","journal-title":"Joural of Logic and Computation"},{"key":"14_CR4","unstructured":"Bernat, V.: First-Order Cyberlogic Hereditary Harrop Logic. Tech. rep., SRI International (2006), http:\/\/www.lsv.ens-cachan.fr\/Publis\/PAPERS\/PS\/Bernat-cyberlogic1.ps"},{"key":"14_CR5","unstructured":"Bernat, V., Ruess, H., Shankar, N.: First-order Cyberlogic. Technical Report CSL-SRI-04-03, SRI International Computer Science Laboratory (2004)"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Blass, A., Gurevich, Y., Moskal, M., Neeman, I.: Evidential Authorization. In: Nanz, S. (ed.) The Future of Software Engineering. pp. 73\u201399. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15187-3_5","DOI":"10.1007\/978-3-642-15187-3_5"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Chaudhuri, K., Pfenning, F., Price, G.: A Logical Characterization of Forward and Backward Chaining in the Inverse Method. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, Third International Joint Conference, IJCAR, Proceedings. pp. 97\u2013111. Springer, Berlin Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_9","DOI":"10.1007\/11814771_9"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Chihani, Z., Miller, D., Renaud, F.: Foundational Proof Certificates in First-Order Logic. In: Bonacina, M.P. (ed.) CADE-24 - 24th International Conference on Automated Deduction. Proceedings. Lecture Notes in Computer Science, vol. 7898, pp. 162\u2013177. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_11","DOI":"10.1007\/978-3-642-38574-2_11"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Chihani, Z., Miller, D., Renaud, F.: A Semantic Framework for Proof Evidence. J. Autom. Reasoning 59(3), 287\u2013330 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9380-6","DOI":"10.1007\/s10817-016-9380-6"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool Integration with the Evidential Tool Bus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI. Proceedings. pp. 275\u2013294. Springer Berlin Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_18","DOI":"10.1007\/978-3-642-35873-9_18"},{"key":"14_CR11","unstructured":"Dargaye, Z., Kirchner, F., Tucc\u0131-Piergiovanni, S., G\u00fcrcan, O.: Towards Secure and Trusted-by-Design Smart Contracts. In: JFLA (2018)"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"DeYoung, H., Garg, D., Pfenning, F.: An Authorization Logic With Explicit Time. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF. pp. 133\u2013145. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/CSF.2008.15","DOI":"10.1109\/CSF.2008.15"},{"issue":"1","key":"14_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M Fairtlough","year":"1997","unstructured":"Fairtlough, M., Mendler, M.: Propositional Lax Logic. Inf. Comput. 137(1), 1\u201333 (1997). https:\/\/doi.org\/10.1006\/inco.1997.2627","journal-title":"Inf. Comput."},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"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.) Computer Security - ESORICS 2006, 11th European Symposium on Research in Computer Security, Proceedings. pp. 297\u2013312. Springer Berlin Heidelberg (2006). https:\/\/doi.org\/10.1007\/11863908_19","DOI":"10.1007\/11863908_19"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Gurevich, Y., Neeman, I.: DKAL: Distributed-Knowledge Authorization Language. Tech. Rep. MSR-TR-2008-09, Microsoft Research (January 2008), https:\/\/www.microsoft.com\/en-us\/research\/publication\/191tr-dkal-distributed-knowledge-authorization-language\/","DOI":"10.1109\/CSF.2008.8"},{"key":"14_CR16","unstructured":"Gurevich, Y., Neeman, I.: DKAL 2 - A Simplified and Improved Authorization Language. Tech. Rep. MSR-TR-2009-11, Microsoft Research (2009), https:\/\/www.microsoft.com\/en-us\/research\/publication\/200-dkal-2-a-simplified-and-improved-authorization-language\/"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Gurevich, Y., Neeman, I.: Logic of infons: The propositional case. ACM Trans. Comput. Log. 12(2), 9:1\u20139:28 (2011). https:\/\/doi.org\/10.1145\/1877714.1877715","DOI":"10.1145\/1877714.1877715"},{"issue":"46","key":"14_CR18","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410(46), 4747\u20134768 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.07.041","journal-title":"Theor. Comput. Sci."},{"issue":"8","key":"14_CR19","doi-asserted-by":"publisher","first-page":"1344","DOI":"10.1017\/S0960129518000440","volume":"29","author":"T Libal","year":"2019","unstructured":"Libal, T., Volpe, M.: A general proof certification framework for modal logic. Math. Struct. Comput. Sci. 29(8), 1344\u20131378 (2019). https:\/\/doi.org\/10.1017\/S0960129518000440","journal-title":"Math. Struct. Comput. Sci."},{"key":"14_CR20","unstructured":"Miller, D.: Foundational Proof Certificates. In: Delahaye, D., Paleo, B.W. (eds.) All about Proofs, Proofs for All, All about Proofs, Proofs for All, vol. Mathematical Logic and Foundations, 55, pp. 150\u2013163. College Publications (2015), https:\/\/hal.inria.fr\/hal-01239733"},{"key":"14_CR21","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.tcs.2014.02.018","volume":"536","author":"V Nigam","year":"2014","unstructured":"Nigam, V.: A framework for linear authorization logics. Theor. Comput. Sci. 536, 21\u201341 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.02.018","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"14_CR22","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/j.cl.2012.02.001","volume":"38","author":"V Nigam","year":"2012","unstructured":"Nigam, V., Jia, L., Loo, B.T., Scedrov, A.: Maintaining distributed logic programs incrementally. Computer Languages, Systems & Structures 38(2), 158\u2013180 (2012). https:\/\/doi.org\/10.1016\/j.cl.2012.02.001","journal-title":"Computer Languages, Systems & Structures"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Nigam, V., Olarte, C., Pimentel, E.: A General Proof System for Modalities in Concurrent Constraint Programming. In: D\u2019Argenio, P.R., Melgratti, H.C. (eds.) CONCUR 2013 - Concurrency Theory - 24th International Conference. Proceedings. Lecture Notes in Computer Science, vol. 8052, pp. 410\u2013424. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_29","DOI":"10.1007\/978-3-642-40184-8_29"},{"issue":"2","key":"14_CR24","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1093\/logcom\/exu029","volume":"26","author":"V Nigam","year":"2016","unstructured":"Nigam, V., Pimentel, E., Reis, G.: An extended framework for specifying and reasoning about proof systems. J. Log. Comput. 26(2), 539\u2013576 (2016). https:\/\/doi.org\/10.1093\/logcom\/exu029","journal-title":"J. Log. Comput."},{"key":"14_CR25","unstructured":"Olarte, C.: L-framework. https:\/\/carlosolarte.github.io\/L-framework\/, accessed on 03-01-2021"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Olarte, C., Pimentel, E., Rocha, C.: Proving Structural Properties of Sequent Systems in Rewriting Logic. In: Rusu, V. (ed.) Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Proceedings. Lecture Notes in Computer Science, vol. 11152, pp. 115\u2013135. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-99840-4_7","DOI":"10.1007\/978-3-319-99840-4_7"},{"issue":"4","key":"14_CR27","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F Pfenning","year":"2001","unstructured":"Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11(4), 511\u2013540 (2001). https:\/\/doi.org\/10.1017\/S0960129501003322","journal-title":"Mathematical Structures in Computer Science"},{"key":"14_CR28","unstructured":"Reis, G.: Observations about the proof theory of cyberlogic. http:\/\/www.gisellereis.com\/papers\/cyberlogic-report.pdf (2019)"},{"key":"14_CR29","unstructured":"Ruess, H., Shankar, N.: Introducing Cyberlogic (2003)"},{"key":"14_CR30","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press (1996)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:29:18Z","timestamp":1625650158000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}