Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic
Open Access
- 21 September 2020
- journal article
- research article
- Published by MDPI AG in Applied Sciences
- Vol. 10 (18), 6577
- https://doi.org/10.3390/app10186577
Abstract
The security of cryptographic protocols has always been an important issue. Although there are various verification schemes of protocols in the literature, efficiently and accurately verifying cryptographic protocols is still a challenging research task. In this work, we develop a formal method based on dynamic epistemic logic to analyze and describe cryptographic protocols. In particular, we adopt the action model to depict the execution process of the protocol. To verify the security, the intruder’s actions are analyzed. We model exactly the protocol applying our formal language and give the verification models according to the security requirements of this cryptographic protocol. With analysis and proof on a selected example, we show the usefulness of our method. The result indicates that the selected protocol meets the security requirements.Funding Information
- Fundamental Research Funds for Central Universities of the Central South University (XDJK2020B035)
This publication has 29 references indexed in Scilit:
- Protocol Composition Logic (PCL)Electronic Notes in Theoretical Computer Science, 2007
- Analyzing security protocols with secrecy types and logic programsJournal of the ACM, 2005
- Secrecy types for asymmetric communicationTheoretical Computer Science, 2003
- Specifying Authentication Protocols Using Rewriting and StrategiesLecture Notes in Computer Science, 2001
- Proving security protocols with model checkers by data independence techniquesJournal of Computer Security, 1999
- The inductive approach to verifying cryptographic protocolsJournal of Computer Security, 1998
- A calculus of mobile processes, IInformation and Computation, 1992
- A logic of authenticationACM Transactions on Computer Systems, 1990
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983
- Communicating sequential processesCommunications of the ACM, 1978