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!
|
| _version_ | 1841539247834660864 |
|---|---|
| author | Xiang GONG Tao FENG Jinze DU |
| author_facet | Xiang GONG Tao FENG Jinze DU |
| author_sort | Xiang GONG |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-3db7b8c7d66a42ce98b41f47d0edd2e3 |
| institution | Kabale University |
| issn | 1000-436X |
| language | zho |
| publishDate | 2021-09-01 |
| publisher | Editorial Department of Journal on Communications |
| record_format | Article |
| series | Tongxin xuebao |
| spelling | doaj-art-3db7b8c7d66a42ce98b41f47d0edd2e32025-01-14T07:22:50ZzhoEditorial Department of Journal on CommunicationsTongxin xuebao1000-436X2021-09-014224025359745040Formal modeling and security analysis method of security protocol based on CPNXiang GONGTao FENGJinze DUTo 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.http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2021175/colored Petri netsecurity protocolformal analysisstate spaceattack path |
| spellingShingle | Xiang GONG Tao FENG Jinze DU Formal modeling and security analysis method of security protocol based on CPN Tongxin xuebao colored Petri net security protocol formal analysis state space attack path |
| title | Formal modeling and security analysis method of security protocol based on CPN |
| title_full | Formal modeling and security analysis method of security protocol based on CPN |
| title_fullStr | Formal modeling and security analysis method of security protocol based on CPN |
| title_full_unstemmed | Formal modeling and security analysis method of security protocol based on CPN |
| title_short | Formal modeling and security analysis method of security protocol based on CPN |
| title_sort | formal modeling and security analysis method of security protocol based on cpn |
| topic | colored Petri net security protocol formal analysis state space attack path |
| url | http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2021175/ |
| work_keys_str_mv | AT xianggong formalmodelingandsecurityanalysismethodofsecurityprotocolbasedoncpn AT taofeng formalmodelingandsecurityanalysismethodofsecurityprotocolbasedoncpn AT jinzedu formalmodelingandsecurityanalysismethodofsecurityprotocolbasedoncpn |