Verifying Security Protocols using Dynamic Strategies
This work addresses the problem of automated security protocol verification for researchers and practitioners, offering a novel method to overcome state-space limitations.
The paper tackles the challenge of automatically verifying security protocols with large or infinite state spaces, proposing a novel framework that successfully verifies protocols unverifiable by existing approaches.
Current formal approaches have been successfully used to find design flaws in many security protocols. However, it is still challenging to automatically analyze protocols due to their large or infinite state spaces. In this paper, we propose a novel framework that can automatically verifying security protocols without any human intervention. Experimental results show that SmartVerif automatically verifies security protocols that cannot be automatically verified by existing approaches. The case study also validates the effectiveness of our dynamic strategy.