Proof Search and Certificates for Evidential Transactions
<p dir="ltr">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 validit...
محفوظ في:
| المؤلف الرئيسي: | |
|---|---|
| مؤلفون آخرون: | , , |
| منشور في: |
2021
|
| الموضوعات: | |
| الوسوم: |
إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
|
| _version_ | 1864513522185011200 |
|---|---|
| author | Vivek Nigam (23276146) |
| author2 | Giselle Reis (23276149) Samar Rahmouni (23276152) Harald Ruess (23276155) |
| author2_role | author author author |
| author_facet | Vivek Nigam (23276146) Giselle Reis (23276149) Samar Rahmouni (23276152) Harald Ruess (23276155) |
| author_role | author |
| dc.creator.none.fl_str_mv | Vivek Nigam (23276146) Giselle Reis (23276149) Samar Rahmouni (23276152) Harald Ruess (23276155) |
| dc.date.none.fl_str_mv | 2021-07-05T03:00:00Z |
| dc.identifier.none.fl_str_mv | 10.1007/978-3-030-79876-5_14 |
| dc.relation.none.fl_str_mv | https://figshare.com/articles/chapter/Proof_Search_and_Certificates_for_Evidential_Transactions/31444708 |
| dc.rights.none.fl_str_mv | CC BY 4.0 info:eu-repo/semantics/openAccess |
| dc.subject.none.fl_str_mv | Information and computing sciences Theory of computation Attestation Logics Proof Search Sequent Calculus |
| dc.title.none.fl_str_mv | Proof Search and Certificates for Evidential Transactions |
| dc.type.none.fl_str_mv | Text Chapter info:eu-repo/semantics/publishedVersion text |
| description | <p dir="ltr">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 (e.g., 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.</p><h2 dir="ltr">Other Information</h2><p dir="ltr">Published in: Lecture Notes in Computer Science<br>License: <a href="https://creativecommons.org/licenses/by/4.0" target="_blank">https://creativecommons.org/licenses/by/4.0</a><br>See article on publisher's website: <a href="https://dx.doi.org/10.1007/978-3-030-79876-5_14" target="_blank">https://dx.doi.org/10.1007/978-3-030-79876-5_14</a></p> |
| eu_rights_str_mv | openAccess |
| id | Manara2_0371bb040d9deb599c0f05c37856422d |
| identifier_str_mv | 10.1007/978-3-030-79876-5_14 |
| network_acronym_str | Manara2 |
| network_name_str | Manara2 |
| oai_identifier_str | oai:figshare.com:article/31444708 |
| publishDate | 2021 |
| repository.mail.fl_str_mv | |
| repository.name.fl_str_mv | |
| repository_id_str | |
| rights_invalid_str_mv | CC BY 4.0 |
| spelling | Proof Search and Certificates for Evidential TransactionsVivek Nigam (23276146)Giselle Reis (23276149)Samar Rahmouni (23276152)Harald Ruess (23276155)Information and computing sciencesTheory of computationAttestation LogicsProof SearchSequent Calculus<p dir="ltr">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 (e.g., 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.</p><h2 dir="ltr">Other Information</h2><p dir="ltr">Published in: Lecture Notes in Computer Science<br>License: <a href="https://creativecommons.org/licenses/by/4.0" target="_blank">https://creativecommons.org/licenses/by/4.0</a><br>See article on publisher's website: <a href="https://dx.doi.org/10.1007/978-3-030-79876-5_14" target="_blank">https://dx.doi.org/10.1007/978-3-030-79876-5_14</a></p>2021-07-05T03:00:00ZTextChapterinfo:eu-repo/semantics/publishedVersiontext10.1007/978-3-030-79876-5_14https://figshare.com/articles/chapter/Proof_Search_and_Certificates_for_Evidential_Transactions/31444708CC BY 4.0info:eu-repo/semantics/openAccessoai:figshare.com:article/314447082021-07-05T03:00:00Z |
| spellingShingle | Proof Search and Certificates for Evidential Transactions Vivek Nigam (23276146) Information and computing sciences Theory of computation Attestation Logics Proof Search Sequent Calculus |
| status_str | publishedVersion |
| title | Proof Search and Certificates for Evidential Transactions |
| title_full | Proof Search and Certificates for Evidential Transactions |
| title_fullStr | Proof Search and Certificates for Evidential Transactions |
| title_full_unstemmed | Proof Search and Certificates for Evidential Transactions |
| title_short | Proof Search and Certificates for Evidential Transactions |
| title_sort | Proof Search and Certificates for Evidential Transactions |
| topic | Information and computing sciences Theory of computation Attestation Logics Proof Search Sequent Calculus |