Affiliations: Department of Computer Engineering, Bergen University
College, Nygaardsgaten 112, 5020 Bergen, Norway. E-mail: [email protected] | Computer Science Department, Aarhus University,
IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark. E-mail: [email protected]
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 Internet Protocol (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 not fully described 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 an industrial project where Coloured Petri Nets (CPNs) were used to
specify and validate the detailed GAN scenario considered by TietoEnator.
Keywords: Modelling and Validation, Coloured Petri Nets, State Space Methods, Model Checking, Protocol Engineering, Concurrrent Systems, Internet Protocols
