.png){kind=icon}
Return
A formal analysis method for composition protocol based on model checking
.png){kind=icon}
OA
AI
DOI：10.1038/s41598-022-12448-2.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Protocol security in a composition protocol environment has always been an open problem in the field of formal analysis and verification of security protocols. As a well-known tool to analyze and verify the logical consistency of concurrent systems, SPIN (Simple Promela Interpreter) has been widely used in the analysis and verification of the security of a single protocol. There is no special research on the verification of protocol security in a composition protocol environment. To solve this problem, firstly, a formal analysis method for composition protocol based on SPIN is proposed, and a formal description of protocol operation semantics is given. Then the attacker model is formalized, and a message specification method based on field detection and component recognition is presented to alleviate the state explosion problem. Finally, the NSB protocol and the NSL protocol are used as examples for compositional analysis. It is demonstrated that the proposed method can effectively verify the security of the protocol in a composition protocol environment and enhance the efficiency of composition protocol verification.
Keywords:
AUTHENTICATION
VERIFICATION
SECURITY
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
3.9
Papers:
27.9W
Citations:
83.5W
Organization
Cited Papers
ShareSaveShareSaveModeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B.png)
SCIENTIFIC REPORTSOAAI
SCIENTIFIC REPORTSIF3.9
OAAIShareSaveShareSaveStructural and Electronic Characteristics of Endohedral Metallofullerenes: Y2C2@C82and Y2@C84Isomers
PREAI
ShareSaveShareSave
View more