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...

Full description

Bibliographic Details
Main Authors: Xiaojuan Chen, Huiwen Deng
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