Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic
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 base...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
MDPI AG
2020-09-01
|
Series: | Applied Sciences |
Subjects: | |
Online Access: | https://www.mdpi.com/2076-3417/10/18/6577 |
_version_ | 1797553081960890368 |
---|---|
author | Xiaojuan Chen Huiwen Deng |
author_facet | Xiaojuan Chen Huiwen Deng |
author_sort | Xiaojuan Chen |
collection | DOAJ |
description | 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. |
first_indexed | 2024-03-10T16:11:23Z |
format | Article |
id | doaj.art-21b621aa2d68474d8bcdf9c0a30a8ecd |
institution | Directory Open Access Journal |
issn | 2076-3417 |
language | English |
last_indexed | 2024-03-10T16:11:23Z |
publishDate | 2020-09-01 |
publisher | MDPI AG |
record_format | Article |
series | Applied Sciences |
spelling | doaj.art-21b621aa2d68474d8bcdf9c0a30a8ecd2023-11-20T14:26:27ZengMDPI AGApplied Sciences2076-34172020-09-011018657710.3390/app10186577Efficient Verification of Cryptographic Protocols with Dynamic Epistemic LogicXiaojuan Chen0Huiwen Deng1Business College, Southwest University, Chongqing 402460, ChinaSchool of Computer and Information Science, Southwest University, Chongqing 400715, ChinaThe 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.https://www.mdpi.com/2076-3417/10/18/6577cryptographic protocolsecurity verificationaction modeldynamic epistemic logic |
spellingShingle | Xiaojuan Chen Huiwen Deng Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic Applied Sciences cryptographic protocol security verification action model dynamic epistemic logic |
title | Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic |
title_full | Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic |
title_fullStr | Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic |
title_full_unstemmed | Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic |
title_short | Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic |
title_sort | efficient verification of cryptographic protocols with dynamic epistemic logic |
topic | cryptographic protocol security verification action model dynamic epistemic logic |
url | https://www.mdpi.com/2076-3417/10/18/6577 |
work_keys_str_mv | AT xiaojuanchen efficientverificationofcryptographicprotocolswithdynamicepistemiclogic AT huiwendeng efficientverificationofcryptographicprotocolswithdynamicepistemiclogic |