SAT-based lazy formal analysis method for security protocols
A SAT-based security protocol formalization analysis method named SAT-LMC is proposed.The method introduces optimized the initial state and transformational rules with “lazy” idea.The efficiency of detection is significantly improved.Moreover，by adding support for strong type flaw attack defect，the...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Editorial Department of Journal on Communications
2014-11-01
|
| Series: | Tongxin xuebao |
| Subjects: | |
| Online Access: | http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2014.11.013/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841539764877000704 |
|---|---|
| author | Chun-xiang GU Huan-xiao WANG Yong-hui ZHENG Dan XIN Nan LIU |
| author_facet | Chun-xiang GU Huan-xiao WANG Yong-hui ZHENG Dan XIN Nan LIU |
| author_sort | Chun-xiang GU |
| collection | DOAJ |
| description | A SAT-based security protocol formalization analysis method named SAT-LMC is proposed.The method introduces optimized the initial state and transformational rules with “lazy” idea.The efficiency of detection is significantly improved.Moreover，by adding support for strong type flaw attack defect，the attack detection becomes more comprehensive.A security protocol analysis tool is implemented based on the method; a type flaw attack is detected for protocol Otway-Rees.For OAuth2.0 protocol，analysis shows that there is a kind of man-in-the-middle attack of the authorization code in some application scenarios. |
| format | Article |
| id | doaj-art-ca5a6bd655044d588b7c3e73997e3b6c |
| institution | Kabale University |
| issn | 1000-436X |
| language | zho |
| publishDate | 2014-11-01 |
| publisher | Editorial Department of Journal on Communications |
| record_format | Article |
| series | Tongxin xuebao |
| spelling | doaj-art-ca5a6bd655044d588b7c3e73997e3b6c2025-01-14T06:44:12ZzhoEditorial Department of Journal on CommunicationsTongxin xuebao1000-436X2014-11-013511712559686370SAT-based lazy formal analysis method for security protocolsChun-xiang GUHuan-xiao WANGYong-hui ZHENGDan XINNan LIUA SAT-based security protocol formalization analysis method named SAT-LMC is proposed.The method introduces optimized the initial state and transformational rules with “lazy” idea.The efficiency of detection is significantly improved.Moreover，by adding support for strong type flaw attack defect，the attack detection becomes more comprehensive.A security protocol analysis tool is implemented based on the method; a type flaw attack is detected for protocol Otway-Rees.For OAuth2.0 protocol，analysis shows that there is a kind of man-in-the-middle attack of the authorization code in some application scenarios.http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2014.11.013/security protocolsformalization analysisBoolean satisfiability problemlazy analyzetype flaw attack |
| spellingShingle | Chun-xiang GU Huan-xiao WANG Yong-hui ZHENG Dan XIN Nan LIU SAT-based lazy formal analysis method for security protocols Tongxin xuebao security protocols formalization analysis Boolean satisfiability problem lazy analyze type flaw attack |
| title | SAT-based lazy formal analysis method for security protocols |
| title_full | SAT-based lazy formal analysis method for security protocols |
| title_fullStr | SAT-based lazy formal analysis method for security protocols |
| title_full_unstemmed | SAT-based lazy formal analysis method for security protocols |
| title_short | SAT-based lazy formal analysis method for security protocols |
| title_sort | sat based lazy formal analysis method for security protocols |
| topic | security protocols formalization analysis Boolean satisfiability problem lazy analyze type flaw attack |
| url | http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2014.11.013/ |
| work_keys_str_mv | AT chunxianggu satbasedlazyformalanalysismethodforsecurityprotocols AT huanxiaowang satbasedlazyformalanalysismethodforsecurityprotocols AT yonghuizheng satbasedlazyformalanalysismethodforsecurityprotocols AT danxin satbasedlazyformalanalysismethodforsecurityprotocols AT nanliu satbasedlazyformalanalysismethodforsecurityprotocols |