Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus

Abstract

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.

Keywords

• Security protocol implementations
• model extraction
• SubJavaScript
• SubPython
• formal method
• ProVerif