Abstract
The Generic Access Network (GAN) architecture is defined by the 3rd Generation Partnership Project (3GPP), and allows telephone services, such as SMS and voice-calls, to be accessed via generic IP networks. The main usage of this is to allow mobile phones to use WiFi in addition to the usual GSM network. The GAN specification relies on the Internet Protocol Security layer (IPSec) and the Internet Key Exchange protocol (IKEv2) to provide encryption across IP networks, and thus avoid compromising the security of the telephone networks. The detailed usage of these two Internet protocols (IPSec and IKEv2) is only roughly sketched in the GAN specification. As part of the process to develop solutions to support the GAN architecture, TietoEnator Denmark has developed a detailed GAN scenario which describes how IPsec and IKEv2 are to be used during the connection establishment procedure. This paper presents a CPN model developed to formally specify and validate the detailed GAN scenario considered by TietoEnator.
Supported by the Danish Research Council for Technology and Production and TietoEnator Denmark.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
3GPP. Digital cellular telecommunications system (Phase 2+); Generic access to the A/Gb interface; Stage 2. 3GPP TS 43.318 version 6.9.0 Release 6 (March 2007)
3GPP. Website of 3GPP (May 2007), http://www.3gpp.org
Billington, J., Han, B.: Modelling and Analysing the Functional Behaviour of TCP Connection Management Procedures. International Journal on Software Tools for Technology Transfer 9(3-4), 269–304 (2007)
CPN Tools, http://www.daimi.au.dk/CPNTools
TietoEnator Denmark, http://www.tietoenator.dk
Droms, R.: Dynamic Host Configuration Protocol. RFC2131 (March 1997)
Kaufman, C. (ed.): Internet Key Exchange Protocol. RFC4306 (December 2005)
Fleischer, P.: Towards a Formal Specification of a Generic Access Network Architeture using Coloured Petri Nets. In: Proc. of Workshop on Petri Nets and Software Engineering (PNSE 2007), pp. 231–232 (2007)
Fleischer, P., Kristensen, L.M.: Towards Formal Specification and Validation of Secure Connection Establishment in a Generic Access Network Scenario. In: Fleischer, P., Kristensen, L.M. (eds.) Eighth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, October 2007. DAIMI PB, vol. 584, pp. 9–28 (2007)
Fleischer, P., Kristensen, L.M.: Modelling of the Configuration/Management API Middleware using Coloured Petri Nets. In: Proc. of PNTAP 2008 (2008)
Grimstrup, P.: Interworking Description for IKEv2 Library. Ericsson Internal. Document No. 155 10-FCP 101 4328 Uen (September 2006)
Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. International Journal on Software Tools for Technology Transfer 9(3-4), 213–254 (2007)
Kent, S.: IP Encapsulating Security Payload (ESP). RFC4303 (December 2005)
Kent, S., Seo, K.: Security Architecture for the Internet Protocol. RFC4301 (December 2005)
Kristensen, L.M., Jensen, K.: Specification and Validation of an Edge Router Discovery Protocol for Mobile Ad Hoc Networks. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 248–269. Springer, Heidelberg (2004)
Vanit-Anunchai, S., Billington, J.: Modelling the Datagram Congestion Control Protocol’s Connection Management and Synchronization Procedures. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 423–444. Springer, Heidelberg (2007)
Westergaard, M., Lassen, K.B.: The BRITNeY Suite Animation Tool. In: Donatelli, S., Thiagarajan, P.S. (eds.) Petri Nets and Other Models of Concurrency - ICATPN 2006. LNCS, vol. 4024, pp. 431–440. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fleischer, P., Kristensen, L.M. (2008). Formal Specification and Validation of Secure Connection Establishment in a Generic Access Network Scenario. In: van Hee, K.M., Valk, R. (eds) Applications and Theory of Petri Nets. PETRI NETS 2008. Lecture Notes in Computer Science, vol 5062. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68746-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-68746-7_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68745-0
Online ISBN: 978-3-540-68746-7
eBook Packages: Computer ScienceComputer Science (R0)