| Titre : | Specication and Verication of 5G protocols using mCRL2 |
| Auteurs : | HOSSEM EDDINE HAFIDI, Auteur ; Laïd Kahloul, Directeur de thèse |
| Type de document : | Monographie imprimée |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2021 |
| Format : | 1 vol. (59 p.) / ill. / 29 cm |
| Langues: | Anglais |
| Résumé : | Fifth generation (5G) standard is the last telecommunication technology, widely considered to be the most important characteristics to implement in future network industry. The 5G system infrastructure contains three principle interfaces, each one follows a set of protocols de?ned by The 3rd Generation Partnership Project group (3GPP). For the next generation network, 3GPP speci?ed two authentication methods systematized in two protocols namely 5G Authentication and Key Agreement (5GAKA) and Extensible Authentication Protocol (EAP). Such protocols are provided to ensure the authentication between system's entities. Researchers have addressed an additional di?culties in security of wireless communication systems whereas system interfaces are connected in a logical topology (air transmission). The mCRL2 language and its associated toolset are formal tools used for modelling, validation and veri?cation of concurrent systems and protocols. Our present work aims to formally re-examines as ?rst time 5G-AKA protocol using mCRL2 language to verify such a security protocols i.e., 5G-AKA protocol. The authentication protocol model is built using Algebra of Communication Process (ACP), its properties are build with Modal mu-Calculus and properties validation exploits formal veri?cation Model-Checking method. We designed an innovative mCRL2 model of 3GPP speci?cation considering 5G-AKA protocol and speci?ed some properties that represents its promised requirements to ?nally evaluate this protocol. |
| Sommaire : |
General Introduction 1
1 5G Background 4 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.1.1 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.1.2 Most concerned 5G features . . . . . . . . . . . . . . . . . . . . 6 1.2 5G architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.2 Three major components of 5G . . . . . . . . . . . . . . . . . . 7 1.2.3 SA architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2.4 NSA architecture . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2.5 SA and NSA di?erences . . . . . . . . . . . . . . . . . . . . . . 10 1.3 Home Network and Related Services . . . . . . . . . . . . . . . . . . . 11 1.3.1 Services and their Network Functions . . . . . . . . . . . . . . . 13 1.3.2 Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.4 Access Network and related Functions . . . . . . . . . . . . . . . . . . 16 1.4.1 AN Control Plane and User Plane . . . . . . . . . . . . . . . . . 18 1.4.2 Massive Multiple-input and multiple-output . . . . . . . . . . . 19 1.4.3 Beam Forming . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 1.5 Security Overall . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.5.1 Authentication . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.5.2 Other enhanced 5G security . . . . . . . . . . . . . . . . . . . . 21 1.6 Authentication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 1.6.1 Phase (i) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 1.6.2 Phase (ii) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 1.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 Formal Methods 30 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.2 Formal Speci?cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.2.2 Process Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2.2.3 Modal mu calculus . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.3 Formal Veri?cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2.3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2.3.2 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2.4 Formal language mCRL2 . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2.4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2.4.2 Formal mCRL2 Speci?cation Model . . . . . . . . . . . . . . . . 41 2.4.3 Formal mCRL2 Properties . . . . . . . . . . . . . . . . . . . . . 46 2.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3 Speci?cation and Veri?cation of 5G-AKA protocol using mCRL2 49 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 3.2 Data Speci?cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 3.3 Process Declaration and LTS Generation . . . . . . . . . . . . . . . . . 52 3.4 Properties Speci?cation and Veri?cation . . . . . . . . . . . . . . . . . 56 3.5 Conclusion and discussion . . . . . . . . . . . . . . . . . . . . . . . . . 58 General Discussion 59 Appendices i A Appendix for chapter 1 ii A.1 How and why did we choose 5G-AKA ? . . . . . . . . . . . . . . . . . . ii B Appendix for chapter 3 iii B.1 Details on how did we obtain our model . . . . . . . . . . . . . . . . . iii B.1.1 Data creation . . . . . . . . . . . . . . . . . . . . . . . . . . . . iv B.1.2 Functions expression mappings. . . . . . . . . . . . . . . . . . . v B.1.3 Declaration of variables . . . . . . . . . . . . . . . . . . . . . . . v B.1.4 De?nition of functions depending on mappings. . . . . . . . . . vi B.1.5 Actions declarations. . . . . . . . . . . . . . . . . . . . . . . . . vii B.1.6 Process declarations, UE, SN and HN. . . . . . . . . . . . . . . viii B.1.7 System initialisation . . . . . . . . . . . . . . . . . . . . . . . . xi B.2 Execution of model in mCRL2 GUI . . . . . . . . . . . . . . . . . . . . xii |
| Type de document : | Mémoire master |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| MINF/664 | Mémoire master | bibliothèque sciences exactes | Consultable |
