A Tableaux System for Dolev-Yao Multi-Agent Epistemic Logic
Resumo
Given the increasing importance of security protocols in our daily activities and communication via internet, the efforts to develop mechanisms and models for verification of such protocols are always relevant. In this work, we explore the Dolev-Yao Multi-Agent Epistemic Logic by providing a tableaux method for it. This logic is an extension of Multi-Agent Epistemic Logic, aimed to verify authenticity and safety in communication protocols and inspired by the Dolev-Yao model, a seminal work in formal cryptography.
Referências
Benevides, M. R. F., Fernandez, L. C. F., and de Oliveira, A. C. C. M. (2018). Dolev-Yao Multi-Agent Epistemic Logic. SAJL, 4(2):281–312.
Boureanu, I., Cohen, M., and Lomuscio, A. (2009). Automatic verification of temporal-epistemic prop. of cryptographic protocols. J. of Applied Non-Classical Logics, 19(4):463–487.
Burrows, M., Abadi, M., and Needham, R. (1990). A Logic of Authentication. ACM Trans. on Computer Systems, 8(1):18–36.
Cohen, M. and Dam, M. (2007). A Complete Axiomatization of Knowledge and Cryptography. In 22nd Annual IEEE Symp. on LICS, pages 77–88.
Diffie, W. and Hellman, M. E. (1976). New Directions in Cryptography. IEEE Trans. on Information Theory, IT-22(6):644–654.
Dolev, D. and Yao, A. C. (1983). On the Security of Public Key Protocols. IEEE Trans. on Information Theory, 29(2):198–208.
Fagin, R., Halpern, J. Y., Moses, Y., and Vardi, M. Y. (2004). Reasoning About Knowledge. The MIT Press.
Fernandez, L. C. F. and Benevides, M. R. F. (2023). A Tableaux System for S5DY - Soundness, Completeness and Termination Argument. [link].
Fitting, M. (1983). Proof Methods for Modal and Intuitionistic Logics. Springer.
Kramer, S. (2008). Cryptographic protocol logic: Satisfaction for (timed) Dolev-Yao cryptography. J. of Logic and Algebraic Programming, 77(1–2):60–91.
Kripke, S. (1959). A Completeness Theorem in Modal Logic. J. Symbolic Logic, 24(1):1–14.
Massacci, F. (2000). Single Step Tableaux for Modal Logics. J. of Automated Reasoning, 24(3):319–364.
Needham, R. M. and Schroeder, M. D. (1978). Using Encryption for Authentication in Large Networks of Computers. Comms. of the ACM, 21(12):993–999.
Rivest, R. L., Shamir, A., and Adleman, L. (1978). A Method for Obtaining Digital Signatures and Public-Key Cryptosystems. Comms. of the ACM, 21(2):120–126.
Syverson, P. (1991). The Use of Logic in the Analysis of Cryptographic Protocols. In 1991 IEEE Computer Society Symp. on Research in Secur. Priv., pages 156–170.
van Ditmarsch, H., van der Hoek, W., and Kooi, B. (2007). Dynamic Epistemic Logic. Springer.
Boureanu, I., Cohen, M., and Lomuscio, A. (2009). Automatic verification of temporal-epistemic prop. of cryptographic protocols. J. of Applied Non-Classical Logics, 19(4):463–487.
Burrows, M., Abadi, M., and Needham, R. (1990). A Logic of Authentication. ACM Trans. on Computer Systems, 8(1):18–36.
Cohen, M. and Dam, M. (2007). A Complete Axiomatization of Knowledge and Cryptography. In 22nd Annual IEEE Symp. on LICS, pages 77–88.
Diffie, W. and Hellman, M. E. (1976). New Directions in Cryptography. IEEE Trans. on Information Theory, IT-22(6):644–654.
Dolev, D. and Yao, A. C. (1983). On the Security of Public Key Protocols. IEEE Trans. on Information Theory, 29(2):198–208.
Fagin, R., Halpern, J. Y., Moses, Y., and Vardi, M. Y. (2004). Reasoning About Knowledge. The MIT Press.
Fernandez, L. C. F. and Benevides, M. R. F. (2023). A Tableaux System for S5DY - Soundness, Completeness and Termination Argument. [link].
Fitting, M. (1983). Proof Methods for Modal and Intuitionistic Logics. Springer.
Kramer, S. (2008). Cryptographic protocol logic: Satisfaction for (timed) Dolev-Yao cryptography. J. of Logic and Algebraic Programming, 77(1–2):60–91.
Kripke, S. (1959). A Completeness Theorem in Modal Logic. J. Symbolic Logic, 24(1):1–14.
Massacci, F. (2000). Single Step Tableaux for Modal Logics. J. of Automated Reasoning, 24(3):319–364.
Needham, R. M. and Schroeder, M. D. (1978). Using Encryption for Authentication in Large Networks of Computers. Comms. of the ACM, 21(12):993–999.
Rivest, R. L., Shamir, A., and Adleman, L. (1978). A Method for Obtaining Digital Signatures and Public-Key Cryptosystems. Comms. of the ACM, 21(2):120–126.
Syverson, P. (1991). The Use of Logic in the Analysis of Cryptographic Protocols. In 1991 IEEE Computer Society Symp. on Research in Secur. Priv., pages 156–170.
van Ditmarsch, H., van der Hoek, W., and Kooi, B. (2007). Dynamic Epistemic Logic. Springer.
Publicado
06/08/2023
Como Citar
FERNANDEZ, Luiz C. F.; BENEVIDES, Mario R. F..
A Tableaux System for Dolev-Yao Multi-Agent Epistemic Logic. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 4. , 2023, João Pessoa/PB.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2023
.
p. 9-16.
ISSN 2763-8731.
DOI: https://doi.org/10.5753/wbl.2023.230019.
