TY - JOUR
T1 - Formal analysis and automated validation of privacy-preserving AICE protocol in mobile edge computing
AU - Yin, Jiaqi
AU - Zhu, Huibiao
AU - Fei, Yuan
N1 - Publisher Copyright:
© 2021, The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature.
PY - 2021/12
Y1 - 2021/12
N2 - Mobile Edge Computing (MEC) is proposed to meet the requirements of mobile users for low latency and response time, and its edge nodes will download data from the cloud server in advance, which arouses researchers to pay attention to the privacy-preserving authentication of mobile users and edge nodes, as well as the data integrity verification of edge nodes. Therefore, it is essential and crucial to integrate the authentication methods into data integrity verification protocol. In this paper, we propose a new integrated protocol AICE, i.e., a uthentication and i ntegrity c hecking on e dges, and then formally analyze and automatically validate the correctness and authentication security of the protocol. We first give the information flows of the AICE protocol by combining the privacy-preserving authentication (PPA) protocol and integrity checking protocol for MEC (ICE) together. According to the features of the AICE protocol, we then select the SVO logic to conduct the formal analysis of the protocol from the perspective of theoretical analysis of modal logic. Furthermore, we employ the AVISPA tool to validate the correctness of the protocol from the perspective of mechanical automatic analysis. The theoretical analysis and mechanical results demonstrate that the integrated protocol AICE satisfies the correctness and authentication.
AB - Mobile Edge Computing (MEC) is proposed to meet the requirements of mobile users for low latency and response time, and its edge nodes will download data from the cloud server in advance, which arouses researchers to pay attention to the privacy-preserving authentication of mobile users and edge nodes, as well as the data integrity verification of edge nodes. Therefore, it is essential and crucial to integrate the authentication methods into data integrity verification protocol. In this paper, we propose a new integrated protocol AICE, i.e., a uthentication and i ntegrity c hecking on e dges, and then formally analyze and automatically validate the correctness and authentication security of the protocol. We first give the information flows of the AICE protocol by combining the privacy-preserving authentication (PPA) protocol and integrity checking protocol for MEC (ICE) together. According to the features of the AICE protocol, we then select the SVO logic to conduct the formal analysis of the protocol from the perspective of theoretical analysis of modal logic. Furthermore, we employ the AVISPA tool to validate the correctness of the protocol from the perspective of mechanical automatic analysis. The theoretical analysis and mechanical results demonstrate that the integrated protocol AICE satisfies the correctness and authentication.
KW - AICE protocol
KW - Automated validation
KW - AVISPA
KW - Formal analysis
KW - SVO logic
UR - http://www.scopus.com/inward/record.url?scp=85118689239&partnerID=8YFLogxK
U2 - 10.1007/s11036-021-01850-1
DO - 10.1007/s11036-021-01850-1
M3 - 文章
AN - SCOPUS:85118689239
SN - 1383-469X
VL - 26
SP - 2258
EP - 2271
JO - Mobile Networks and Applications
JF - Mobile Networks and Applications
IS - 6
ER -