Automatic Verification of Security of Identity Federation Security Protocol Based on SAML2.0 with ProVerif in the Symbolic Model

Jintian Lu ； Xudong He ； Yitong Yang ； Dejun Wang ； Bo Meng

《International Journal of Network Security》 22卷1期 (2020/01) Pp. 80-92

https://doi.org/10.6633/IJNS.202001_22(1).08

摘要

In recent years, several Identity Federation security protocols have been introduced to enhance the security of Identity authentication. Owning to the complexity, assessing security of Identity Federation security protocols has becoming a hot issue. Hence, in this study, we firstly review the development of formal methods on Identity Federation Security Protocol Based on SAML. And then, an Identity Federation Security Protocol Based on SAML is formalized with Applied PI calculus. After that, the formal model is translated into the inputs of ProVerif. Finally, we run ProVerif to analyze the security properties of Identity Federation Security Protocol Based on SAML. The result shows it has not secrecy, but it has some authentications. At the same time, we present a solution to address the security problems.

關鍵字

Applied PI Calculus ； Authentication ； Formal Method ； Security Protocol