Formal Analysis of Information Card Federated Identity-Management Protocol

WANG Juan; HU Hongxin; ZHAO Bo; YAN Fei; ZHANG Huanguo; WU Qianhong

Article Contents

Article Navigation > Chinese Journal of Electronics > 2013 > 22(1): 83-88

WANG Juan, HU Hongxin, ZHAO Bo, et al., “Formal Analysis of Information Card Federated Identity-Management Protocol,” Chinese Journal of Electronics, vol. 22, no. 1, pp. 83-88, 2013,

Citation:

WANG Juan, HU Hongxin, ZHAO Bo, et al., “Formal Analysis of Information Card Federated Identity-Management Protocol,” Chinese Journal of Electronics, vol. 22, no. 1, pp. 83-88, 2013,

WANG Juan, HU Hongxin, ZHAO Bo, et al., “Formal Analysis of Information Card Federated Identity-Management Protocol,” Chinese Journal of Electronics, vol. 22, no. 1, pp. 83-88, 2013,

Citation:

WANG Juan, HU Hongxin, ZHAO Bo, et al., “Formal Analysis of Information Card Federated Identity-Management Protocol,” Chinese Journal of Electronics, vol. 22, no. 1, pp. 83-88, 2013,

PDF( 424 KB)

Formal Analysis of Information Card Federated Identity-Management Protocol

1.
Computer School, Wuhan University, Wuhan 430072, China;
2.
Key Laboratory of Aerospace Information Security and Trusted Computing Ministry of Education, Wuhan 430072, China;
3.
SEFCOM, Arizona State University, AZ 85287, USA

Funds: This work is supported by the National Natural Science Foundation of China (No.61003268, No.61173138) the Fundamental Research Funds for the Central Universities (No.211274629).

Received Date: 2011-10-01
Rev Recd Date: 2012-04-01
Publish Date: 2013-01-05

Abstract

Abstract

Information Card (InfoCard) is a usercentric identity management metasystem. It has been accepted as a standard of OASIS Identity Metasystem Interoperability Technical Committee. However, there is currently a lack of security analysis to InfoCard protocol, especially, with formal methods. In this paper, we accommodate such a requirement by analyzing security properties of InfoCard protocol adopting a formal protocol analysis tool. Our analysis result discovers that current InfoCard protocol is vulnerable against the session replay attack. Furthermore, we reveal the importance of two optional elements in InfoCard metasystem, token scope and proof key, and found that InfoCard protocol will be susceptible to manin- the-middle attack and token replay attack if these two optional elements lack.
- Information card,
- User-centric,
- Identity,
- Automated validation of Internet security protocols and applications (AVISPA)

FullText(HTML)

References(18)

References

Identity Metasystem Interoperability Version 1.0. OASIS Standard.http://docs. oasis-open. org/imi/identity/v1.0/ identity.html.

Higgins Open Source Identity Framework, http: //www.eclipse. org/ higgins/.

Information Card Foundation, http://informationcard. net/.

G. Lowe, “Breaking and fixing the Needham-Schroeder publickeyprotocol using FDR”, Software-Concept and Tools, Vol.17,pp.93-102, 1996.

AVISPA. The AVISPA User Manual. http://avispa-project.org/publications.

A. Armando et al., “The AVISPA tool for the automated validationof Internet security protocols and applications”, Proc.of the 17th International Conference on Computer Aided Verification(CAV’05), Scotland, UK, Springer-Verlag. 2005.

A. Nanda, “A technical reference for the information card profileV1.0”, Technical Report, Microsoft Corporation, 2006.

K. Bhargavan, C. Fournet, A.D. Gordon and N. Swamy, “Verifiedimplementations of the information card federated identitymanagementprotocol”, Proc. of ASIACCS ’08, AkihabaraConvention Hall, Tokyo, ACM, pp.123-135, 2008.

Y. Chevalier, L. Compagna et al., “A high level protocol specificationlanguage for industrial security sensitive protocols”,Proc. of SAPS’04, Austrian Computer Society, pp.1-13, 2004.

Yannick Chevalier and Laurent Vigneron, “Rule-based programsdescribing Internet security protocols”, Electronic Notesin Theoretical Computer Science, Vol.124, No.1, pp.113-132,2005.

Dolev, A. Yao, “On the security of public-key protocols”, IEEETransactions on Information Theory, Vol.29, No.2, pp.198-208,1983.

D. Basin, S. Mödersheim, L. Vigan‘o., “OFMC: A symbolicmodel-checker for security protocols”, International Journal ofInformation Security, No.4, pp.181-208, 2005.

Sebastian Gajek, Jörg Schwenk and Xuan Chen, “On the insecurityof microsoft’s identity metasystem cardspace”, TechnicalReport, Ruhr University, Bochum, Germany, 2008.

L.N. Hoang, P. Laitinen and N. Asokan, “Secure roaming withidentity metasystems”, Proc. of IDtrust ’08, New York, USA,ACM, pp.36-47, 2008.

Waleed A. Alrodhan and Chris J. Mitchell, “Improving the securityof cardspace”, EURASIP Journal on Information Security,Vol.2009, Article ID 167216, pp.1-8, 2009.

GailJoon Ahn, John Lam, “Managing privacy preferences forfederated identity management”, Proc. of DIM’05, Fairfax, Virginia,USA, pp.28-36, 2005.

Gail-Joon Ahn, Moonam Ko, Mohamed Shehab, “Privacyenhanceduser-centric identity management”, Proc. of IEEE InternationalConference on Communication, Dresden, Germany,pp.1-, 2009.

C. Karlof, J. Tygar, D. Wagner, and U. Shankar, “Dynamicpharming attacks and locked same-origin policies for web browsers”, Proc. of the 14th ACM Conference on Computerand Communications Security (CCS), Virginia, USA, pp.58-71, 2007.

Relative Articles

Supplements(0)

Cited By

Proportional views