5G has been under standardization for over a decade and will
drive the world's mobile technologies in the decades to come. One
of the cornerstones of the 5G standard is its security, also for
devices that move frequently between networks, such as autonomous
vehicles, and must therefore be handed over from one network
operator to another.
We present a novel, comprehensive, formal analysis of the
security of the device handover protocols specified in the 5G
standard. Our analysis covers both handovers within the 5G core
network, as well as fallback methods for backwards compatibility
with 4G/LTE. We identify four main handover protocols and
formally model them in the security protocol verification tool
Tamarin. Using these models, we determine for each protocol the
minimal set of security assumptions required for its intended
security goals to be met. Understanding these requirements is
essential when designing devices and other protocols that depend
on the reliability and security of network handovers.