Document - A formal security analysis of an OSA/Parlay authentication interface

2005

Conference article Open Access

A formal security analysis of an OSA/Parlay authentication interface

Corin R., Di Caprio G., Etalle S., Gnesi S., Lenzini G., Moiso C.

OSA/Parlay API Formal verification of security Industrial Industrial test case Formal Verification of Security SCS-Cybersecurity D.2.4 Software/Program Verification

We report on an experience in analyzing the security of the Trust and Security Management (TSM) protocol, an authentication procedure within the OSA/Parlay Application Program Interfaces (APIs) of the Open Service Access and Parlay Group. The experience has been conducted jointly by research institutes experienced in security and industry experts in telecommunication networking. OSA/Parlay APIs are designed to enable the creation of telecommunication applications outside the traditional network space and business model. Network operators consider the OSA/Parlay a promising architecture to stimulate the development of web service applications by third party providers, which may not necessarily be experts in telecommunication and security. The TSM protocol is executed by the gateways to OSA/Parlay networks; its role is to authenticate client applications trying to access the interfaces of some object representing an offered network capability. For this reason, potential security flaws in the TSM authentication strategy can cause the unauthorized use of the network, with evident damages to the operator and the quality of services. We report a rigorous formal analysis of the TSM specification, which is originally given in UML. Furthermore, we illustrate our design choices to obtain the formal model, describe the tool-aided verification and finally expose the security flaws discovered.

Source: 7th International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 131–146, Athens, GREECE, JUN 15-17, 2005

Publisher: Springer Berlin / Heildelberg, Berlin, DEU

Citations

[1] Open Service Access (OSA) - Application Programming Interface (API) Mapping for OSA. http://www.3gpp.org/ftp/Specs/archive/29 series. Release 5.
[2] M. Abadi and A. D. Gordon. Reasoning about Cryptographic Protocols in the Spi Calculus. In A. W. Mazurkiewicz and J. Winkowski, editors, Proc. of 8th Int. Conf. on Concurrency Theory (CONCUR 97), Warsaw, Poland, July 1997, LNCS 1243, pages 59-73. Springer-Verlag, 1997.
[3] M. Abadi and A. D. Gordon. A Calculus for Cryptographic Protocols. The Spi Calculus. TR 149, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, USA 1998.
[4] M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6-15, 1996. IEEE Computer Society.
[5] E. M. Clarke, S. Jha, and W. Marrero. Verifying security protocols with Brutus. ACM Trans. Software Engineering and Methodology, 9(4):443-487, 2000. ACM .
[6] R. Corin and S. Etalle. An improved constraint-based system for the verification of security protocols. In M. Hermenegildo and G. Puebla, editors, Proc. of the International Static Analysis Symposium (SAS), Madrid, Spain, Sep. 2002, LNCS 2477, pages 326-341. Springer-Verlag, 2002.
[7] D. Dolev and A. Yao. On the security of public-key protocols. IEEE Trans. Information Theory, 29(2):198-208, 1983. IEEE Computer Society.
[8] R. Gorrieri, F. Martinelli, M. Petroocchi, and A. Vaccarelli. Formal analysis of some timed security properties in wireless protocols. In Proc. of the 6th IFIP WG 6.1 Formal Methods for Open Object-Based Distributed Systems (FMOODS 2003) Paris, France, Nov. 2003, LNCS 2884, pages 139-154. Springer Verlag, 2003.
[9] Parlay X Working Group. Parlay apis 4.0: Parlay x web services - white paper. The Parlay Group, 2002. http://www.parlay.org.
[10] G. Leduc. Verification of two versions of the challenge handshake authentication protocol (CHAP). Annals of Telecommunications, 55(1-2):18-30, 2000. HermesLavoisier.
[11] G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. Software Concepts and Tools, 3(17):93-102, 1997. Springer-Verlag.
[12] C. A. Meadows. Formal verification of cryptographic protocols: A survey. In J. Pieprzyk and R. Safavi-Naini, editors, Proc. of the Int. Conf. on the Theory and Application of Cryptology Advances in Cryptology and Information Security, (ASIACRYPT 94), LNCS 917, pages 135-150. Springer-Verlag, 1994.
[13] J. Millen and V. Shmatikov. Constraint Solving for Bounded-Process Cryptographic Protocol Analysis. In P. Samarati, editor, Proc. of the 8th ACM Conf. on Computer and Communication Security, pages 166-175. ACM , 2001.
[14] UML Resource Page. Unified Modeling Language. http://www.uml.org.
[15] A. W. Roscoe. Modelling and Verifying Key-Exchange Protocols using CSP and FDR. In Proc. of The 8th Computer Security Foundations Workshop (CSFW 95), Kenmare, Ireland, Mar. 1995, pages 98-107. IEEE Computer Society, 1995
[16] S. Schneider. Verifying Authentication Protocols in CSP. IEEE Trans. Sofware Engineering, 24(8):743-758, 1998. IEEE Computer Society .
[17] J. Thayer, J. Herzog, and J. Guttman. Strand spaces: Why is a security protocol correct? In Proc. of the 19th IEEE Computer Society Symposium on Research in Security and Privacy (SSP 98), Oakland, CA, USA, May 1998, pages 160-171. IEEE Computer Society, 1998.

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:179771,
	title = {A formal security analysis of an OSA/Parlay authentication interface},
	author = {Corin R. and Di Caprio G. and Etalle S. and Gnesi S. and Lenzini G. and Moiso C.},
	publisher = {Springer Berlin / Heildelberg, Berlin, DEU},
	doi = {10.1007/11494881_9},
	booktitle = {7th International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 131–146, Athens, GREECE, JUN 15-17, 2005},
	year = {2005}
}