Formal Specification and Validation of Secure Connection Establishment in a Generic Access Network Scenario

  • Paul Fleischer
  • Lars M. Kristensen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5062)


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.


Mobile Station Internet Protocol Address Wireless Router Internet Protocol Packet Secure Connection 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)Google Scholar
  2. 2.
    3GPP. Website of 3GPP (May 2007),
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
  5. 5.
    TietoEnator Denmark,
  6. 6.
    Droms, R.: Dynamic Host Configuration Protocol. RFC2131 (March 1997)Google Scholar
  7. 7.
    Kaufman, C. (ed.): Internet Key Exchange Protocol. RFC4306 (December 2005)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Fleischer, P., Kristensen, L.M.: Modelling of the Configuration/Management API Middleware using Coloured Petri Nets. In: Proc. of PNTAP 2008 (2008)Google Scholar
  11. 11.
    Grimstrup, P.: Interworking Description for IKEv2 Library. Ericsson Internal. Document No. 155 10-FCP 101 4328 Uen (September 2006)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Kent, S.: IP Encapsulating Security Payload (ESP). RFC4303 (December 2005)Google Scholar
  14. 14.
    Kent, S., Seo, K.: Security Architecture for the Internet Protocol. RFC4301 (December 2005)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Paul Fleischer
    • 1
  • Lars M. Kristensen
    • 1
  1. 1.Department of Computer ScienceUniversity of AarhusAarhus NDenmark

Personalised recommendations