Formal modeling and security analysis method of security protocol based on CPN
To solve the problem of modeling and analyzing with colored Petri net (CPN), which was determining vulnerabilities in hole location but couldn’t identify any attack path, and the problem of when the introduction of the attacker model, the number of possible message paths in the CPN formal model of s...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Editorial Department of Journal on Communications
2021-09-01
|
| Series: | Tongxin xuebao |
| Subjects: | |
| Online Access: | http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2021175/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | To solve the problem of modeling and analyzing with colored Petri net (CPN), which was determining vulnerabilities in hole location but couldn’t identify any attack path, and the problem of when the introduction of the attacker model, the number of possible message paths in the CPN formal model of security protocol surges the state space prone to explosion, which made it difficult to extract accurate attack paths, the formal modeling method of security protocol was improved base on CPN, the attack paths were verified and extracted, further the fine-grained protocol modeling and control were adopted.As well as in the aspect of state-space convergence, and a waiting-sync method for different processes of CPN model in each hierarchy model was proposed, which effectively controlled the state-space scale of the model.Through the security evaluation and analysis of TMN protocol, 25 attack paths of the protocol are extracted successfully, the security of the protocol is evaluated, and the effectiveness of the proposed method is proved. |
|---|---|
| ISSN: | 1000-436X |