Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus
Analyzing security protocol web implementations is a crucial part of web security. Based on the model extraction technology, this paper first defines SubJavaScript and SubPython languages, and then establishes mapping models from SubPython and SubJavaScript to Applied PI Calculus respectively, after...
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2020-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/8981985/ |
| _version_ | 1818935301071962112 |
|---|---|
| author | Xudong He Qin Liu Shuang Chen Chin-Tser Huang Dejun Wang Bo Meng |
| author_facet | Xudong He Qin Liu Shuang Chen Chin-Tser Huang Dejun Wang Bo Meng |
| author_sort | Xudong He |
| collection | DOAJ |
| description | Analyzing security protocol web implementations is a crucial part of web security. Based on the model extraction technology, this paper first defines SubJavaScript and SubPython languages, and then establishes mapping models from SubPython and SubJavaScript to Applied PI Calculus respectively, after that, develops the semi-automatic model extraction tools SubPython2PV and SubJavaScript2PV to analyze the four widely used security protocol web implementations. The experiment shows that the four typical security protocol web implications have confidentiality, but lack of authentication. |
| first_indexed | 2024-12-20T05:17:59Z |
| format | Article |
| id | doaj.art-6e977717db6b4f6b92e4454ed73cda3c |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-20T05:17:59Z |
| publishDate | 2020-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-6e977717db6b4f6b92e4454ed73cda3c2022-12-21T19:52:06ZengIEEEIEEE Access2169-35362020-01-018266232663610.1109/ACCESS.2020.29716158981985Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI CalculusXudong He0https://orcid.org/0000-0002-2007-2576Qin Liu1https://orcid.org/0000-0002-8888-0211Shuang Chen2https://orcid.org/0000-0001-7717-9238Chin-Tser Huang3https://orcid.org/0000-0003-3983-972XDejun Wang4https://orcid.org/0000-0003-1370-8190Bo Meng5https://orcid.org/0000-0002-4377-0051School of Computer Science, South-Central University for Nationalities, Wuhan, ChinaSchool of Computer Science, South-Central University for Nationalities, Wuhan, ChinaSchool of Computer Science, South-Central University for Nationalities, Wuhan, ChinaDepartment of Computer Science and Engineering, University of South Carolina, Columbia, SC, USASchool of Computer Science, South-Central University for Nationalities, Wuhan, ChinaSchool of Computer Science, South-Central University for Nationalities, Wuhan, ChinaAnalyzing security protocol web implementations is a crucial part of web security. Based on the model extraction technology, this paper first defines SubJavaScript and SubPython languages, and then establishes mapping models from SubPython and SubJavaScript to Applied PI Calculus respectively, after that, develops the semi-automatic model extraction tools SubPython2PV and SubJavaScript2PV to analyze the four widely used security protocol web implementations. The experiment shows that the four typical security protocol web implications have confidentiality, but lack of authentication.https://ieeexplore.ieee.org/document/8981985/Security protocol implementationsmodel extractionSubJavaScriptSubPythonformal methodProVerif |
| spellingShingle | Xudong He Qin Liu Shuang Chen Chin-Tser Huang Dejun Wang Bo Meng Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus IEEE Access Security protocol implementations model extraction SubJavaScript SubPython formal method ProVerif |
| title | Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus |
| title_full | Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus |
| title_fullStr | Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus |
| title_full_unstemmed | Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus |
| title_short | Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus |
| title_sort | analyzing security protocol web implementations based on model extraction with applied pi calculus |
| topic | Security protocol implementations model extraction SubJavaScript SubPython formal method ProVerif |
| url | https://ieeexplore.ieee.org/document/8981985/ |
| work_keys_str_mv | AT xudonghe analyzingsecurityprotocolwebimplementationsbasedonmodelextractionwithappliedpicalculus AT qinliu analyzingsecurityprotocolwebimplementationsbasedonmodelextractionwithappliedpicalculus AT shuangchen analyzingsecurityprotocolwebimplementationsbasedonmodelextractionwithappliedpicalculus AT chintserhuang analyzingsecurityprotocolwebimplementationsbasedonmodelextractionwithappliedpicalculus AT dejunwang analyzingsecurityprotocolwebimplementationsbasedonmodelextractionwithappliedpicalculus AT bomeng analyzingsecurityprotocolwebimplementationsbasedonmodelextractionwithappliedpicalculus |