PORTO @ 
Archivio Istituzionale della Ricerca
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishLong Term Evolution (LTE) is the most recent standard in mobile communications, introduced by 3rd Generation Partnership Project (3GPP). Most of the formal security analysis works in literature about LTE analyze authentication procedures, while interoperability is far less considered. This paper presents a formal security analysis of the interoperability procedures between LTE and the older Universal Mobile Telecommunications System (UMTS) networks, when mobile devices seamlessly switch between the two technologies. The Proverif tool has been used to conduct the verification. The analysis shows that security properties (secrecy of keys, including backward/forward secrecy, immunity from off-line guessing attacks and network components authentication) hold almost as expected, if all the protections allowed by the LTE standard are adopted. If backhauling traffic is not protected with IPSec, which is a common scenario since the use of IPSec is not mandatory, some security properties still hold while others are compromised. Consequently, user's traffic and network's nodes are exposed to attacks in this scenario.
Formal Verification of LTE-UMTS Handover Procedures / Bettassa Copet, Piergiuseppe; Marchetto, Guido; Sisto, Riccardo; Costa, Luciana. - STAMPA. - (2015), pp. 738-744. ((Intervento presentato al convegno 20th IEEE Symposium on Computers and Communications (ISCC) tenutosi a Larnaca, Cyprus nel 6-9 July 2015 [10.1109/ISCC.2015.7405602].
| Titolo: | Formal Verification of LTE-UMTS Handover Procedures | |
| Autori: | ||
| Data di pubblicazione: | 2015 | |
| Abstract: | Long Term Evolution (LTE) is the most recent standard in mobile communications, introduced by 3rd... Generation Partnership Project (3GPP). Most of the formal security analysis works in literature about LTE analyze authentication procedures, while interoperability is far less considered. This paper presents a formal security analysis of the interoperability procedures between LTE and the older Universal Mobile Telecommunications System (UMTS) networks, when mobile devices seamlessly switch between the two technologies. The Proverif tool has been used to conduct the verification. The analysis shows that security properties (secrecy of keys, including backward/forward secrecy, immunity from off-line guessing attacks and network components authentication) hold almost as expected, if all the protections allowed by the LTE standard are adopted. If backhauling traffic is not protected with IPSec, which is a common scenario since the use of IPSec is not mandatory, some security properties still hold while others are compromised. Consequently, user's traffic and network's nodes are exposed to attacks in this scenario. | |
| ISBN: | 978-1-4673-7194-0 | |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| 07405602.pdf | Articolo, versione editoriale | 2. Post-print / Author's Accepted Manuscript | Non Pubblico - Accesso privato/ristretto | Administrator Richiedi una copia |
| 1570084757_author_postprint.pdf | File principale articolo. Author's version. | 2. Post-print / Author's Accepted Manuscript | PUBBLICO - Tutti i diritti riservati | Visibile a tuttiVisualizza/Apri |
http://hdl.handle.net/11583/2621605
Copyright © 2022