Authentication 2G 3G 4G

Analysis of authentication and key establishment in
inter-generational mobile telephony

(with appendix July 31, 2013)
Chunyu Tang, David A. Naumann, and Susanne Wetzel

Stevens Institute of Technology
AbstractSecond (GSM), third (UMTS), and fourthgeneration (LTE) mobile telephony protocols are all in active use,
giving rise to a number of interoperation situations. Although the
standards address roaming by specifying switching and mapping
of established security context, there is not a comprehensive
specification of which are the possible interoperation cases.
Nor is there comprehensive specification of the procedures to
establish security context (authentication and short-term keys) in
the various interoperation scenarios. This paper systematically
enumerates the cases, classifying them as allowed, disallowed,
or uncertain with rationale based on detailed analysis of the
specifications. We identify the authentication and key agreement
procedure for each of the possible cases. We formally model these
scenarios and analyze their security, in the symbolic model, using
the tool ProVerif. We find two scenarios that inherit a known false
base station attack. We find an attack on the CMC message of
another scenario.
I.
I NTRODUCTION
Mobile telephony has become an integral part of our daily

activities, in part due to the tremendous success and market
penetration of smartphones and tablets. In many locations
around the world, mobile communication is already facilitated
through the fourth generation (4G) technology called Long
Term Evolution (LTE)which evolved from the third generation (3G) technology, Universal Mobile Telecommunications
System (UMTS). Along with the opportunities created by
technology evolution there are challenges. One challenge is
the interoperation of different generations of technologies, i.e.,
communication involving mixed network components. Past
experience has shown that such interoperation may introduce
unexpected security vulnerabilities [1], [2].
The specifications promulgated by the 3GPP organization
for UMTS [3] and LTE [4] do address interoperation between
the different generations of technologies. The specification
for UMTS systematically studies all possible combinations
of interoperation between UMTS and second generation (2G)
GSM. The LTE specification details the mechanisms for security context switching and mapping to facilitate interoperation
between LTE, UMTS, and GSM. However, this applies to
maintaining context during handover and idle mode mobility.
To the best of our knowledge, the specification for LTE does
not explicitly address establishing of an initial security context
for interoperation. In particular, to date there is no comprehensive enumeration of all interoperation cases and their respective
procedures for authentication and key agreement (AKA). In
this paper we close this gap.
The first contribution of this paper is to systematically
enumerate of all possible interoperation cases between LTE,
UMTS, and GSM. We classify these cases as allowed, disallowed, or uncertain, with explicit rationale making detailed
reference to the specifications. Of the 243 cases identified,

19 cases involve GSM and UMTS technologies only, and as
such are fully treated by the UMTS specification [3]. For
cases involving LTE components, 138 cases are clearly ruled
out somewhere in the specification and 38 cases are clearly
allowed. For the remaining 48 cases the specifications and
documentation based on the specifications do not provide a
clear indication whether these cases are allowed.
As a second contribution of this paper, we provide details
on what we call the AKA scenarios,1 i.e., the specific protocol
steps for authentication and key agreement, in each allowed or
uncertain case. For each uncertain case we identify conditions
under which the case could occur. For all of the 19+38+48
cases we identify the corresponding AKA scenario. It turns
out that there are only 10 distinct AKA scenarios, including
the pure GSM, pure UMTS, and pure LTE scenarios which
apply in some interoperation cases. Although the GSM/UMTS
scenarios are described in the specifications, that is not the
case for 86 roaming cases involving LTE. For three of those
scenarios we identify two variations which are both consistent
with the specifications and which have different authenticity
properties.
As a third contribution, we provide formal models for all
10 of the AKA scenarios, including variations, in the symbolic
(Dolev-Yao) model of cryptography and using the ProVerif tool
[5]. We provide a security analysis based on these models.
The models are composed in a modular fashion from the
basic protocol models for GSM, UMTS, and LTE. This will
facilitate adding or modifying scenarios, in case of changes to
the specifications or the conditions for the uncertain cases to
occur.
Our security analysis addresses authentication properties
and secrecy. We show that two of the LTE interoperation
scenarios inherit an attack, known from GSM and the interoperation between UMTS and GSM [6], in which a false base
station can eavesdrop and modify data traffic. We show how
the attack can be prevented in one scenario. We also show that
one scenario is prone to an attack against the Cipher Mode
Command (CMC) message.
Outline: Sect. II surveys related work and Sect. III is
an overview of the GSM, UMTS, and LTE AKA protocols.
Sect. IV presents the first of our main contributions, the
systematic enumeration of possible cases and classification
of what is (dis)allowed or uncertain according to the 3GPP.
Sect. V presents our second contribution, the AKA scenarios
for each allowed or uncertain case, justified with reference to
1 In some standards, AKA has more specific meaning and varying terminology is used, e.g., depending on whether authentication is mutual.
the specifications. Sect. VI describes our ProVerif models for

GSM, UMTS, and LTE, and the specifications of desired security properties. Sect. VII presents our third contribution, the
ProVerif models for AKA scenarios involving interoperation
between technologies, and analysis results for those models.
categorizing them in terms of secrecy, integrity, or authenticity

properties. Possible security improvements are also discussed.
For reasons of space, we cannot present the complete

classification of cases, scenarios, and analysis results; instead
we present excerpts and highlights. A long version online
includes full details [7].
In GSM, UMTS, and LTE, the network architecture includes three main elements: the Mobile Station (MS), the
Serving Network (SN), and the Home Network (HN).
II.
III.
OVERVIEW OF GSM, UMTS, AND LTE SECURITY

MECHANISMS
The MS is the combination of the Mobile Equipment (ME)

and an identity module. The ME is the user device that
contains the radio functionality and the encryption/integrity
mechanisms used to protect the traffic between the MS and the
network. A 4G ME also includes the functionality to derive an
LTE master secret key KASME . In GSM, the identity module of
the Subscriber Identity Module (SIM) contains the unique International Mobile Subscriber Identity (IMSI), the subscribers
permanent secret key Ki, as well as the mechanisms used
for GSM AKA and GSM session key derivation. The UMTS
identity module (USIM) includes the IMSI, Ki, and the UMTS
AKA and session key derivation functionality. It furthermore
may contain the SIM functionality, i.e., the GSM AKA and
key derivation functionality. In contrast to a 3G USIM, an
LTE USIM (also refered to as enhanced USIM) provides for
additional functionality including enhanced capability for the
storing of a security context.
R ELATED WORK
Several attacks have been found against the GSM encryption algorithms [8], [9], [10], [11], [12]. Ahmadian et al. [13]
show attacks which exploit weakness of one GSM cipher
to eavesdrop or impersonate a UMTS subscriber in a mixed
network. In this paper we focus on protocol flaws rather than
cryptographic weaknesses.
Fox [14] finds the false base station attack on the GSM
AKA due to the lack of authentication of the network. Meyer
and Wetzel [1], [2], [15] show that a man-in-the-middle attack
can be performed on one of the cases of interoperation between
GSM and UMTS. In prior work [16], we use the ProVerif (PV)
tool to analyze GSM, UMTS, and roaming cases between GSM
and UMTS. The false base station attack [14] and the man-inthe-middle attack [1] were confirmed by the PV models.
The SN typically consists of the Base Station (BS) and either the Visitor Location Register/Serving GPRS Support Node
(VLR/SGSN) in GSM and UMTS, or the Mobile Management
Entity (MME) in LTE. The BS is the network access point
which manages the radio resources and establishes the connection to the MS. In GSM, the BS includes the Base Transceiver
Station (BTS) which connects to the Base Station Controller
(BSC). In GSM, encryption terminates at the BTS or at the
SGSN in GPRS. In UMTS, the BS includes the NodeB which
connects to the Radio Network Controller (RNC). Encryption
and integrity protection in UMTS terminates in the RNC. In
LTE, BS is the evolved NodeB (eNodeB). LTE distinguishes
the protection of the connection between the MS and the
eNodeBthe so-called Access Stratum (AS) and the connection between the MS and MMEthe so-called Non-Access
Stratum (NAS). In LTE, the MME is the end-point for the
NAS and the respective protection mechanisms.
PV is an automatic protocol verifier that can verify authentication, secrecy, and other properties, in the symbolic (DolevYao) model, considering an unbounded number of sessions
and unbounded message space. Quite a few protocols have
been analyzed using PV. For example, Chang and Shmatikov
[17] use PV to analyze the Bluetooth device pairing protocols;
they rediscover an offline guessing attack [18] as well as a
new attack. Blanchet and Chaudhuri [19] find an integrity
attack against a file sharing protocol. Chen and Ryan analyze
TPM authorization [20]. Kremer and Ryan use PV to verify
an electronic voting protocol [21]. Arapinis et al. [22] find two
attacks against anonymity in UMTS, using PV.
Han and Choi [23] demonstrate a threat against the LTE
handover key management, involving a compromised base
station. This is concerned with maintaining security context,
whereas our work addresses establishing such context. Tsay
and Mjlsnes [24] find an attack on the UMTS and LTE AKA
protocols using CryptoVerif, an automated protocol analyzer
based on a computational model. In fact the attack lives at
the symbolic level. It depends on insecurity of the connection
between the serving network and the home network. In our
work we assume the connection between serving network and
home network is secure. (Although the standard specifies the
protocols, their implementations are operator-specific.)
The HN includes the Home Location Register (HLR) and

the Authentication Center (AuC) in GSM and UMTS, respectively the Home Subscriber Server (HSS) in LTE. The HN
stores all subscriber data including the IMSI and permanent
shared secret key Ki. It furthermore, holds its (own) algorithms
for deriving session keys as well as generating authentication
vectors. A 4G HN also includes the functionality for deriving
an LTE master secret key KASME .
Lee et al. [25] analyze the anonymity property of the

UMTS and LTE AKA and connection establishment protocols
using formal security (computational) models. The assumption
in this work is that the attacker is not capable of impersonating any network devices and the underlying cryptographic
system is perfect. They manually prove the protocols meet the
anonymity requirement, under these assumptions.
Overview of GSM Security Mechanisms. Fig. 1 shows

the GSM AKA procedure. The goal of the GSM AKA is to
authenticate the MS and to establish an encryption key that
can then be used to protect the user data exchange between
the MS and BS. The GSM AKA procedure can be triggered
by the initial network attach request [27], the Routing Area
Update (RAU) request [28], or the service request [29]. The
service request happens after a dedicated channel has been
established between the MS and the SN [29], which means
Mobarhan et al. [26] evaluate the publically known attacks

on GSM and UMTS (and the related technology GPRS),
2
BS
MS
HN
VLR/SGSN
MS
1. CAP
MME
BS
HN
GSM I
1. CAP
2. GUTI
LTE I
2. TMSI
3. User ID Request
4. IMSI
3. Identity Request
4. IMSI
5. IMSI, SNid,
Network Type
5. IMSI
GSM II
6. RAND, XRES, KC
.
GSM III
Generate RAND & SQN

MAC = f1(Ki, AMF, SQN, RAND)
XRES = f2(Ki, RAND), CK = f3(Ki, RAND)
IK = f4(Ki, RAND), AK = f5(Ki, RAND)
AUTN=SQNAK || AMF || MAC
KASME= KDF(CK, IK, SNid, SQNAK)
6. RAND, AUTN,
XRES, KASME
LTE II
Generate RAND
XRES = A3(Ki, RAND)
KC = A8(Ki, RAND)
7. RAND
RES = A3(Ki, RAND)
KC = A8(Ki, RAND)
7. RAND, AUTN
8. RES
Verify RES = XRES
GSM IV
LTE III
9. KC
Decide algorithms
9. Selected algorithms
10. CMComplete
AK = f5(Ki, RAND), SQN = 1st(AUTN)AK

Verify SQN in correct range
XMAC = f1(Ki, 2nd(AUTN), SQN, RAND)
Verify 3rd(AUTN) = XMAC,
RES = f2(Ki, RAND)
CK = f3(Ki, RAND), IK = f4(Ki, RAND)
KASME = KDF(CK, IK, SNid, 1st(AUTN))
8. RES
Verify RES = XRES
Fig. 1.
KNASenc = KDF (KASME, NAS-enc-alg, Alg-ID)

KNASint = KDF(KASME, NAS-int-alg, Alg-ID)
Decide NAS-Algs,
NAS-MAC = EIA(KNASint, (CAP, Algs))
9. CAP, NAS-Algs, [Nonces], NAS-MAC
GSM message sequence diagram [29], [15]

VLR/SGSN
BS
LTE IV
MS
HN
1. CAP
UMTS I
2. TMSI
3. User ID Request
4. IMSI
5. IMSI
UMTS II
Generate RAND & SQN

MAC = f1(Ki, AMF, SQN, RAND)
AUTN = SQNAK || AMF || MAC
KNASenc = KDF (KASME, NAS-enc-alg, Alg-ID)

KNASint = KDF(KASME, NAS-int-alg, Alg-ID)
XNAS-MAC = EIA(KNASint, (CAP, Algs))
Verify XNAS-MAC = NAS-MAC
Start ciphering/deciphering
and integrity protection
10. NAS SMComplete
ciphered , integrity protected
KeNB = KDF(KASME)
11. CAP, KeNB
6. RAND, XRES,
CK, IK, AUTN
UMTS III
LTE V
7. RAND, AUTN
RES = f2(Ki, RAND), CK = f3(Ki, RAND)
SQN = 1st(AUTN) AK
XMAC = f1(Ki, 2nd(AUTN), SQN, RAND)
Verify 3rd(AUTN) = XMAC
Verify SQN is in correct range
8. RES
Verify RES = XRES
10. CK, IK
UMTS IV
Decide algorithms ALG, Generate FRESH

MAC-I = f9((ALG, CAP FRESH), IK)
KeNB = KDF (KASME)

KRRCenc = KDF (KeNB, RRC-enc-alg, Alg-ID)
KRRCint = KDF(KeNB, RRC-int-alg, Alg-ID)
KUPenc = KDF (KeNB, UP-enc-alg, Alg-ID)
Decide AS-Algs, AS-MAC = EIA(KRRCint, Algs)
12. AS-Algs,
AS-MAC
KeNB = KDF (KASME)
KRRCenc = KDF (KeNB, RRC-enc-alg, Alg-ID)
KRRCint = KDF(KeNB, RRC-int-alg, Alg-ID)
KUPenc = KDF (KeNB, UP-enc-alg, Alg-ID)
XAS-MAC = EIA(KRRCint, Algs)
Verify XAS-MAC = AS-MAC
13. AS SMComplete
Integrity protected
Fig. 3.
LTE message sequence diagram [4]
9. ALG, CAP,
FRESH, MAC-I
XMAC-I = f9((ALG, CAP FRESH), IK)
Verify MAC-I = XMAC-I, Verify CAP
messages are transmitted as in GSM I. In comparison to

GSM, UMTS includes mechanisms for integrity protection.
Specifically, as part of block UMTS II (see Fig. 2), the HN
derives session keys for both encryption and integrity protection based on MSs long-term secret key Ki. Like in GSM, MS
authenticates to the VLR/SGSN through a challenge-response
protocol using the authentication vector that the VLR/SGSN
obtained from HN. The authentication of the network to MS
is achieved indirectly, as the BS integrity protects the sending
of CAP which it can only do if it has received key IK from
HN via VLR/SGSN. This prevents a false base station attack.
10. SMComplete
Fig. 2.
UMTS message sequence diagram [3], [15]
that the attach request must have been executed previously.

The identity and CAPabilities (CAP) in the attach request or
the RAU request are used in the AKA procedure. Therefore,
in GSM I, the MS sends the identity and the CAP to the SN.
In GSM block II, the SN obtains authentication vectors from
the HN. In GSM III a typical challenge-response procedure is
carried out to authenticate the MS to SN. Then, in GSM IV,
the VLR/SGSN provides the BS with the session key Kc. BS
selects the encryption algorithm based on MSs capabilities
and informs MS.
Overview of LTE Security Mechanisms. The LTE AKA

(Fig. 3) is built on the UMTS AKA. In contrast to UMTS
security, LTE introduces an enhanced key derivation hierarchy
that allows the distinguishing of protection mechanisms on
NAS and AS. Furthermore, inclusion of the id of SN as part of
the key derivation enables the MS to indirectly authenticate the
MME (through the successful use of derived keys). In addition,
LTE defines a comprehensive security context framework,
including native vs. mapped security contexts, full vs. partial
security contexts, and current vs. non-current contexts [4].
A security context typically consists of a set of security
parameters including cryptography keys and identifiers for
respective cryptographic mechanisms.
GSM is prone to a false base station attack [14] as the

GSM AKA only authenticates the MS to the SN. Since a false
BS can intercept and modify the sending of MSs capabilities,
a false BS may force the use of no encryption thus enabling the
false BS to control all traffic between the MS and the network.
Overview of UMTS Security Mechanisms. Similar to
GSM, the UMTS AKA procedure can be triggered by the
attach request or the RAU request. In UMTS I, the same
3
TABLE I.
The LTE AKA can be triggered by the initial network

attach request, the Tracking Area Update (TAU) request or
the service request [28]. When a NAS signalling connection
exists, the network can initiate an authentication procedure at
any time [28]. Before the service request or the NAS signalling
connection establishing, the attach request must have already
been executed [28]. Therefore, the first block of the LTE AKA
can contain an attach request or a TAU request. If the AKA
starts with an attach request, the first block (LTE I) contains
the transmission of the identity and the security capabilities of
the MS. If the AKA starts with a TAU request, in the first block
(LTE I), an additional nonce NONCEMS is sent to the MME.
The nonce in the TAU request is only used when mapping
an UMTS to an EPS security context. However, since the MS
does not know when the mapping will happen, the nonce is
always included in the TAU request message 2 [30]. In LTE, the
master key KASME is derived and provided to MME together
with the respective authentication vector. Unlike in GSM and
UMTS, the id of the SN is an input to the key derivation,
i.e., the derived key is bound to a specific MME. In block
LTE IV, MME derives the keys which are used to protect NAS,
while in LTE V the BS derives the keys to protect AS as well
as user data. The MS does the corresponding key derivations
in LTE IV and LTE V. Furthermore, the proper use of keys
derived from KASME indirectly authenticates the MME to MS.
Given that LTE distinguishes between the protection of NAS
and AS, MME selects the respective algorithms to protect NAS
(based on MSs capabilities) and announces the choice to MS
in LTE IV as part of the NAS Security Mode Command (SMC).
Similarly, BS announces its choice of algorithms in LTE V as
part of the AS SMC.
IV.
ID
1
2
3
4
...
122
...
Identity
Module
4G
...
3G
...
E XCERPT OF CLASSIFYING THE 243 INTEROPERATION

CASES ( THE FULL TABLE IS IN [7])
Components
VLR/SGSN
ME
BS
/MME
4G
4G
4G
3G
4G
4G
2G
3G
4G
...
...
...
3G
3G
3G
...
...
...
HN
4G
4G
4G
4G
...
3G
...
Condition
to support
Occurrence
Reasons for
Disallowance
A1
A1
R5
the table, we have adopted a color/font scheme: Rows in

normal font with no color indicate cases which are explicitly
allowed based on the 3GPP specifications (e.g., the case with
ID 1). Green color and bold font indicates uncertain cases
(e.g., cases 2 and 3). Grey color and italic font indicates cases
which are ruled out by the specifications (e.g., case 4). The
cases involving only 2G/3G components are marked with blue
color and in bold italic font (e.g., case 122). There are 19 such
cases which are not further detailed in this paper as they have
been analyzed previously [6], [16]. For the disallowed and
uncertain cases the table includes the details for the reasoning
to determine the respective classification.
Allowed Interoperation Cases. For cases involving a mix
of 4G, 3G, and 2G network components, we have identified 38
cases which are explicitly allowed by the 3GPP specifications.
For the identity module, the SIM supports 2G AKA only
[6]. A USIM supports both 2G and 3G AKA [6]. Similarly, a
4G USIM supports 2G, 3G, and 4G AKA [30]. Since a large
number of USIMs is in current use, a 4G ME with the USIM is
allowed to access the 4G network. Since the 4G ME is capable
of deriving LTE keys and storing security contexts [31], the
combination of a 4G ME with a USIM supports 4G AKA.
E STABLISHING A NATIVE SECURITY CONTEXT IN

INTEROPERATION
As mentioned previously, LTE introduces a comprehensive

framework for handling security contexts [4]. In particular,
this includes the mapping of security contexts in the case of
interoperation of LTE with GSM or UMTS. The specification
defines the use of existing native or mapped security contexts
and recommends the performing of an AKA procedure once a
mapped security context is used. However, to the best of our
knowledge, the specification to date does not include details on
what this AKA is to entail in case of interoperation of LTE,
UMTS, and GSM, i.e., if the network components are from
different generations of technologies.
For the ME, it is possible to use a SIM or a USIM with

a 2G ME [6]. Since the 4G USIM is an enhanced version of
the USIM, this implies that it is possible to also use a 4G
USIM with a 2G ME. Similarly, since a SIM or USIM can
be used with a 3G ME, [6], it is also possible to use a 4G
USIM with a 3G ME. A 4G ME can be used with a SIM
[30] or USIM [4] and certainly with a 4G USIM. A 2G ME
only supports GERAN [6]. A 3G ME supports GERAN and
UTRAN [6], and a 4G ME supports GERAN, UTRAN, and
E-UTRAN [30].
In the following, we systematically enumerate all possible

interoperation cases and classify them as allowed, disallowed,
or uncertain based on various information in the 3GPP specifications for GSM, UMTS, and LTE. In Sect. V we then focus on
the allowed and uncertain cases only determining the specific
AKA scenarios for each one of these cases.
For the BS, a 2G BS is only capable of handling a GSM

session key Kc [6], which means a 2G BS only supports a 2G
ciphering mode setting [29]. Similarly, a 3G BS requires the
UMTS cipher key CK and the UMTS integrity key IK [6]
supporting only the 3G security mode set-up and operation [3].
A 4G BS requires KeNB and only supports the 4G AS security
mode command procedure and operation [4].
Enumeration of Interoperation Cases. As discussed in

Sect. III, there are five main system components: the identity
module, the ME, the BS, the VLR/SGSN/MME and the HN.
Each one of those components can be 2G, 3G, or 4Gthus
resulting in 35 = 243 possible combinations. Table I shows
the details for five cases. In order to improve readability of
For the VLR/SGSN/MME, a 2G VLR/SGSN can only

control a 2G BS and only supports 2G AKA [6]. A 3G
VLR/SGSN can control both a 2G BS and a 3G BS and can
support both 2G and 3G AKA [6]. An MME can control a 4G
BS and can support the 4G AKA [4].
For the HN, a 2G HN can maintain 2G and 3G subscriptions [6]. A 3G HN can maintain 2G and 3G subscriptions [6].
A 4G HN can maintain 3G and 4G subscriptions [4].
2 In
LTE AKA, the nonce is never used. So the first block is always LTE I.
LTE I will be used in one interoperation scenario (S8).
TABLE III.
E XCERPT OF DETERMINING AKA SCENARIOS AND

RESPECTIVE REASONING ( FULL TABLE IN [7])
Disallowed Interoperation Cases. We found that the

3GPP specifications rule out 138 cases which include some
4G components. Table I refers to the following reasons for
disallowing various cases:
R1 Use of SIMs to access the 4G network is not allowed [4].
R2 A 2G ME cannot interoperate with a 3G or 4G BS [6].
R3 A 3G ME does not support the 4G radio access interface
[6].
R4 A 2G VLR/SGSN cannot control a 3G or 4G BS [6].
R5 A 3G VLR/SGSN cannot control a 4G BS [6].
R6 An MME refuses to convert a GSM security context
to 4G security context. Consequently, this rules out all
interoperation cases which would require the deriving of
the master key KASME from the GSM cipher key Kc [4].
R7 A 3G ME with USIM attaching to a 3G BS shall only
participate in 3G AKA and shall not participate in 2G
AKA [3]. This rules out the case in which a USIM
subscribed to a 2G HN is used in a 3G ME that connects
to a 3G BS, as the 2G HN can only support 2G AKA.
1
2
3
...
91
...
ME
4G
4G
...
3G
...
...
4G
...
BS
4G
3G
2G
...
4G
...
VLR/
SGSN/
MME
4G
4G
4G
...
4G
...
Scenario
HN
4G
4G
4G
...
HN
...
S3
S10
S9
...
S7,S8
...
Reason
Stated
in spec
Interpretation
AGKW
BHV
BINV
...
GKWX
...
T
T
...
QU
...
Using this approach, we categorize the 105 allowable and

uncertain interoperation cases into 10 distinct scenarios:
An MME can control a 3G BS or a 2G BS.

A 3G HN or 2G HN can maintain 4G subscriptions.
A 4G HN can maintain 2G subscriptions.
An MME can support the 2G or 3G AKA.
V.
Identity
Module
vector is generated by the HN depends on HNs capabilities, the type of VLR/SGSN/MME requesting/receiving the
authentication vector, the type of BS, and the type of the
identity module. Table II provides the details for the eleven
distinct instances for obtaining an authentication vector. While
the first six (A, B, C, D, E, F) are based on methods
described in the 3GPP specifications (mostly w.r.t. security
context switching and mapping in LTE), the latter ones are
interpretations derived from specified methods. Second, we
consider the type of the BS, which determines the type of
the security mode setup procedure. Third, depending on the
type of BS it controls, the VLR/SGSN/MME might have to
convert the encryption/integrity keys.
Uncertain Interoperation Cases. The remaining 48 cases

involving 4G components are classified as uncertain. This is
due to the fact that the specifications do not provide clear
indication as to whether or not these cases are allowable. For
those cases, Table I refers to these conditions under which they
could occur:
A1
A2
A3
A4
Components
ID
S1
S2
S3
S4
S5
S6
S7
GSM IIV.
UMTS IIV.
LTE IV.
GSM IIV, conv(3G AV 2G AV).
GSM IIII k UMTS IV, conv(Kc CK IK, VLR/SGSN).
UMTS IIII k GSM IV, conv(CK IK Kc, VLR/SGSN).
LTE I k UMTS IIIII k [optionally, LTE IV] k LTE V,
conv(CK IK KASME , MME).
S8 LTE I k UMTS IIIII k LTE IVV, conv(CK IK nonces
KASME , MME).
S9 GSM I k LTE IIIII k [optionally, LTE IV] k GSM IV,
conv(CK IK Kc, MME), AV = 4G AV + CK + IK.
S10 UMTS I k LTE IIIII k [optionally, LTE IV] k UMTS IV,
AV = 4G AV + CK + IK.
AKA SCENARIOS
Focusing on the allowable and uncertain interoperation

cases determined in the previous section, we now detail the
respective AKA for each of these cases. Specifically, based on
the 3GPP specifications for GSM, UMTS, and LTE we have
determined which of the building blocks GSM IIV, UMTS I
IV, and LTE IV need to be combined in what fashion to
comprise a suitable AKA for the respective interoperation case.
For each case we provide the rationale based on which the
building blocks are combined.
The blocks are as introduced in Figs. 1, 2, and 3. With notation

a k b we indicate that block b follows after block a. Scenarios
S7, S9, and S10 have blocks marked in brackets as optional.
It is consistent with the specifications to either include or omit
these blocks, so we analyze versions with and without the
block. The notation conv(K1 K2, C) denotes that network
component C converts key K1 into K2. Furthermore, AV =
4G AV + CK + IK indicates that the 4G HN provides not only
the 4G authentication vector to the MME but also includes the
UMTS encryption key CK and integrity key IK.
Overall, this approach allowed us to categorize all allowable and uncertain interoperation cases into 10 distinct scenarios. For five of the scenarios, the respective AKA was already
specified by 3GPP in the context of enabling interoperation
between GSM and UMTS (including the two native 2G and
3G scenarios as outlined in Sect. III). One of the remaining
five scenarios is the native 4G AKA (see Sect. III). To the best
of our knowledge, the other four are new and are specified for
the first time in this paper.
Determining the Scenarios. In order to determine a
suitable AKA for a specific interoperation case, first we
consider which message might trigger the AKA to determine
the messages transmitted in the first block. Then, we consider
the authentication vector that is generated in the HN and
subsequently provided to the VLR/SGSN/MME. In particular,
the authentication vector determines what kind of challengeresponse procedure is carried out, i.e., whether GSM III,
UMTS III, or LTE III. How and what kind of authentication
Table III shows an excerpt of determining and categorizing

the AKA for all of the 105 allowed and uncertain cases
including the respective reasoning to obtain the categorization
(with reference to Table II).
In the following we focus on detailing Scenarios S7S10.
Scenarios S1S3 are discussed in Sect. III and Scenarios S4
S6 coincide with scenarios described in the 3GPP specifications as well as prior work [1], [2], [15], [16].
5
TABLE II.
A
B
Type of AV
Type of BS
Type of ME
Conversion
First Block
C
D
E
F
O
P
Q
R
S
G
H
I
J
K
L
T
M
N
U
V
W
X
4G ME with USIM
R EASONS USED FOR DETERMINING AKA SCENARIOS
Upon request by an MME with network type equals E-UTRAN, the 4G HN generates and delivers the 4G AVs (separation bit = 1) [4].
Upon request by an MME with network type equals UTRAN or GERAN, the 4G HN generates and delivers the 4G AVs, plus CK and IK (separation
bit = 0) [4].
Upon request by a 3G VLR/SGSN, the 3G HN generates and sends out 3G AVs [3].
Upon request by a 2G VLR/SGSN with a 3G IMSI, the 3G HN generates 2G AVs from 3G AVs [6].
2G HN only supports to generate 2G AVs [6].
Upon request by a VLR/SGSN/MME with a 2G IMSI, the 3G HN always generates and delivers the 2G AVs [6].
Upon request by a 3G VLR/SGSN, the 4G HN generates 3G AVs [4] [or derived from D].
Upon request by a 2G VLR/SGSN with 3G/4G IMSI, the 4G HN generates 2G AVs from UMTS AVs [Derived from D].
Upon request by an MME, the 3G HN generates 3G AVs [Derived from E and [6]].
Upon request by a 2G VLR/SGSN with a 4G IMSI, the 3G HN generates 2G AVs from 3G AVs [Derived from D].
Upon request by a VLR/SGSN/MME with a 2G IMSI, the 4G HN always generates and delivers the 2G AVs [Derived from F].
4G BS only supports 4G SMC [4].
The 4G ME supports to derive KASME and store the security contexts. [31]
XG ME supports XG SMC [4], [3]
3G ME supports 2G SMC [6].
4G ME supports 2G/3G SMC [Derived from L]
The 3G BS requires CK and IK, the VLR/SGSN/MME generates them from Kc by applying conversion function c3 [6].
2G BS is not capable of handling of cipher and integrity keys. The VLR/SGSN/MME converts the CK and IK into Kc [6].
Because the 4G BS requires KeNB , which is derived from the KASME , the VLR/SGSN/MME generates KASME from the CK, IK and sends it to the
BS [Derived from M or [4]].
Triggered by attach request or RAU request, the first block is GSM I or UMTS I [27], [28]
Triggered by LTE attach request or TAU request in which the nonce is never used, the first block is LTE I [4].
Triggered by TAU request and the nonce is used in latter blocks, the first block is LTE I [28], [30].
4G BS
MME
3G HN
uses it with the CK, IK, and NONCEMS as input parameters

to derive the KASME . The MME sends the integrity protected
SMC message containing the nonce NONCEMS received from
the MS and the nonce NONCEMME . Upon receiving the SMC
message, the MS checks whether the NONCEMS and the
capabilities match what it originally sent in LTE I. If the
check successes, the MS uses the same key derivation function
as in the MME to derive the KASME and sends out the SMC
complete message. Subsequently, LTE V is executed.
UMTS I
UMTS II
UMTS III
KASME = KDF(CK, IK)
KASME = KDF(CK, IK)
LTE V
Fig. 4. AKA scenario S7; in alternate version, LTE IV added before LTE V
S9. This scenario is characterized by a mixed SN including

a 2G BS and a 4G MME as well as an MS that is subscribed
to a 4G HN where either the identity module is a 4G USIM
or it is a 4G ME, i.e., the MS supports 4G AKA. Four of
the allowable/uncertain cases fall into this category. Because
the 2G BS covers routing areas, the initial message can be
the attach request or the RAU request. So the transmitting
of the identity and the capabilities is as in GSM I (Fig. 1).
When the MME requests the authentication vector from the
HN by sending the IMSI and the network type, because the
network type is GERAN (because of the 2G BS), the 4G HN
generates and delivers the 4G authentication vector with the
UMTS cipher key CK and integrity key IK. Because the NAS
signaling is transparent to the BS, the LTE challenge-response
procedure LTE III (Fig. 3) is executed between the MS and
the MME. In this interoperation scenario, we consider the two
variations with and without LTE IV (Fig. 3). The first variation
sticks to the LTE AKA as long as possible (i.e., until executing
LTE IV before setting up the cipher between the MS and the
BS). The other one goes to set the cipher between MS and
the BS as soon as finishing the challenge-response procedure
(without executing LTE IV). Later we show that the AKA
without LTE IV is prone to a false base station attack and
the AKA with LTE IV is prone to an attack against the CMC
message between the 2G BS and the MS. Because the 2G
BS requires the GSM session key Kc, the MME derives the
encryption key Kc from the UMTS cipher key CK and integrity
key IK. Since only the 2G cipher mode setting is supported
by the 2G BS, the 2G cipher mode setting procedure GSM IV
(Fig. 1) is executed between the 2G BS and the MSwhich
S7. This scenario is characterized by a 4G ME, a 4G SN

(i.e., 4G BS and 4G MME) and a USIM or 4G USIM identity
module subscribed to a 3G HN. Two of the allowable/uncertain
cases fall into this category. The AKA is triggered by the attach
request. The identity request and response procedure is the
same as in LTE I (Fig. 3). The 3G HN can generate 2G or 3G
authentication vectors, but cannot generate 4G authentication
vectors. Upon request by the MME, the 3G HN therefore
generates and delivers a 3G authentication vector which thus
is identical to UMTS II. Upon receiving the authentication
vector, the MME communicates with the MS as in UMTS III.
The 4G BS requires 4G AS keys, which are derived from the
intermediate key KeNB . Because the intermediate key KeNB is
derived from the local master key KASME , the MME applies a
key derivation function to generate the local master key KASME
from the UMTS encryption key CK and integrity key IK.
Including LTE IV is optional in this scenario. Later, we analyze
both variations and show that the AKA without LTE IV is
prone to an attack in which a false base station can both
eavesdrop and modify the messages between the MS and the
SN. Executing both LTE IV and V prevents this attack. LTE V
(Fig. 3) is executed which includes the deriving of KeNB . Fig. 4
shows this AKA scenario without LTE IV.
S8. This scenario is characterized by the same cases as in
S7. The difference to S7 is that this scenario is triggered by the
TAU request and the NONCEMS in the TAU request is used
in LTE IV. The retrieving and generating of the authentication
vector and the challenge-response procedure are the same as in
S7. In LTE IV, the MME generates a nonce NONCEMME and
6
LTE III
XMAC = f1(Ki, RAND)

MAC = XMAC, RES = f2(Ki, RAND)
KASME = KDF(CK, IK, SNid,)
8. RES
Verify RES = XRES
KNASenc = KDF (KASME,), KNASint = KDF(KASME,)
Decide enableEnc?,
NAS-MAC = EIA(KNASint, (CAP, enableEnc))
event begMS(imsi_sn, snid_sn, kasme_sn, cap_sn)
9. CAP, enableEnc, NAS-MAC
event endMS(imsi_ms, snid_ms, kasme_ms, cap_ms)
LTE IV
KNASenc = KDF (KASME), KNASint = KDF(KASME)

XNAS-MAC = EIA(KNASint, (CAP, enableEnc))
event begSN(imsi_ms, snid_ms, kasme_ms)
10. NAS SMComplete
If enableEnb then ciphered , integrity protected
otherwise integrity protected
event endSN(imsi_sn, snid_sn, kasme_sn)
Fig. 5.
model
Part of the 4G AKA scenario (Fig. 3) annotated in accord with our
long version of the paper we consider integrity of data traffic,

which is also specified using this message.
The 4G model in ProVerif. There are four main processes
in our PV model, representing the behavior of the MS, the
eNB, the MME and the HN respectively. Fig. 5 shows the
details of part of the model, specifically Blocks III and IV from
Fig. 3. Fig. 5 shows the events for correspondence assertions.
It also shows the name of the variables which are used in our
model, which facilitates checking that the models accurately
reflect the protocol diagrams.
M ODELING AND ANALYZING THE PURE PROTOCOLS

IN P ROV ERIF
The ProVerif (PV) tool has been described well elsewhere,

and we use standard idioms in our modeling. We give here
a brief overview of our design decisions followed by a few
details concerning the LTE model. Details of the GSM and
UMTS models can be found in [16]. The roaming models are
discussed in Sect. VII, together with our analysis results. The
complete models are available with the long version of the
paper [7].
In the LTE protocol, the MS already has the SN id before

starting the AKA shown in Fig. 3. In our model, we add the SN
id to the authentication challenge (message 7). In addition,our
model omits sequence numbering and the key AK, so they
do not appear in Fig. 5. Sequence numbers aid in preventing
re-use of authentication vectors. Instead of modeling sequence
numbers, our models simply do not re-use AVs.
In PV, protocols are defined using process algebra. Properties are specified as correspondence assertions [32] that
refer to events. Events are instrumentation that mark important points reached by the principals and have no effect on
protocol behavior. For example, the correspondence assertion
event(e1(M)) event(e2(M)) says that if event e1 occurs, with
argument value M, then event e2 must have happened previously with the same argument M. In checking an assertion, PV
may terminate having successfully proved the property, with
respect to unbounded message space and number of sessions,
or having found a possible or definite attack.
Here are some design decisions that apply to all of our
models. Each message has a header to indicate the type of
the message content. The secure communications between SN
and HN are modeled as private channels. Registration of the
MS, i.e., pre-sharing of each long-term credential pair (IMSI,
Ki), is modeled using PVs table construct. We do not model
details of algorithm capabilities/selection. The capability is a
nondeterministically chosen boolean value interpreted to mean
whether the MS has encryption capability. (Integrity protection
is mandatory in 3G/4G, and absent in 2G.) Because the value is
nondeterministically chosen, our analysis considers all cases.
Following authentication, a single data message is included,
which suffices to specify the secrecy of data traffic. In the
MME
7. RAND, AUTN, SNid
S10. This scenario is characterized by a 4G HN, a mixed

SN consisting of a 3G BS and a 4G MME, as well as an
MS that is subscribed to a 4G HN where either the identity
module is a 4G USIM or it is a 4G ME with a 3G USIM, i.e.,
the MS supports 4G AKA. Three of the allowable/uncertain
cases fall into this category. The 3G BS covers routing areas,
so the initial message can be the attach request or a RAU
request. Thus, the transmitting of identity and capabilities is
as in UMTS I (Fig. 2). In order to obtain an authentication
vector, the MME sends the authentication data request with
the IMSI and the network type to the 4G HN. Because the
access network is UTRAN, the 4G HN generates and delivers
the 4G authentication vector as well as the UMTS encryption
key CK and integrity key IK. Subsequently, the LTE challengeresponse procedure LTE III (Fig. 3) is executed between the
MS and the MME. As in scenarios S7 and S9, the LTE IV is
optional. Later we show that the authentication properties hold
in both variations. The 3G BS obtains the UMTS encryption
key CK, the UMTS integrity key IK, as well as the capabilities
as part of UMTS IV (Fig. 2)which also includes the UMTS
security mode set-up procedure between the 3G BS and the
MS.
VI.
BS
MS
also includes the MME sending the GSM session key to the
2G BS.
Fig. 6 shows the code of the MS process. The registration

process of the MS device is in lines 2224. Lines 2829
model that the MS receives and checks the authentication
challenge message. The process awaits a message on the public
channel, with designated format and particular values: the
format must be (msgHdr, nonce, mac, ident) where msgHdr is the
literal CHALLENGE and the mac must equal f1( ki , rand ms). In
lines 3839, the MS receives the NAS SMC message and
verifies the integrity and the received capabilities. The MS then
sends out the SMC complete message which is ciphered if the
encryption is enabled and integrity protected (lines 4351).
Lines 46 and 52 call a parameterized process which specifies
the AS SMC procedure in lines 311 and receives the data
message in lines 1819. The other three processes representing
the BS, the MME, and the HN are similar to this (see [7]).
The secrecy and authentication properties are specified as
follows.
1
2
3
4
5
6
query a t t a c k e r ( payload ) .
query a t t a c k e r ( payload )
event ( d i s a b l e E n c ) .
query a t t a c k e r ( s e c r e t ) .
query x1 : i d e n t , x2 : i d e n t , x3 : asmeKey ;
event ( endSN ( x1 , x2 , x3 ) )
event ( begSN ( x1 , x2 , x3 ) ) .
query x1 : i d e n t , x2 : i d e n t , x3 : asmeKey , x4 : bool ;
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
challenge and successful use of the keys derived from KASME .

Authentication of the MME to MS is specified in query lines
67; it includes authenticity of the security capabilities. The
authentication of the eNB to the MS is specified in query lines
89. The encryption capability is included in the parameters
of the events to specify that the events should agree on the
encryption option. These authentication properties are proved
successfully.
l e t pMSAS( kasme ms : asmeKey , imsi ms : i d e n t , cap ms : bool ) =

l e t kenb ms : enbKey = kdf enb ( kasme ms ) i n
l e t kasenc ms : asEncKey = kdf as enc ( kenb ms ) i n
l e t kasint ms : a s I n t K e y = k d f a s i n t ( kenb ms ) i n
l e t kupenc ms : upEncKey = kdf up enc ( kenb ms ) i n
i n ( pubChannel , (=ASSMC, enableEnc as ms : bool ,
= f i n t e g a s ( b o o l 2 b i t s t r i n g ( enableEnc as ms ) , kasint ms ) ) ) ;
event begENB ( imsi ms , kenb ms ) ;
out ( pubChannel , ( ASSMComplete , as smcomplete msg ,
f i n t e g a s ( as smcomplete msg , kasint ms ) ) ) ;
event endMS ENB( imsi ms , kenb ms , cap ms ) ;
i n ( pubChannel , (=MSG, datamsg : b i t s t r i n g ,
= f i n t e g a s ( datamsg , kasint ms ) ) ) ;
out ( pubChannel , s e n c r y p t a s ( s e c r e t , kasenc ms ) ) ;
out ( pubChannel , s e n c i n t a s ( s e c r e t , kasint ms ) ) ;
out ( pubChannel , senc up ( s e c r e t , kupenc ms ) ) ;
i f enableEnc as ms = t r u e then
l e t msgcontent : b i t s t r i n g = s d e c r y p t a s ( datamsg ,
kasenc ms ) i n 0 .
Because communication between eNB and MME is assumed secure, it is authentication of MS to MME implies
authentication to eNB as well. However, as a sanity check
on the model, query line 10 says that if eNB believes that
it has established the KeNB associated with an MS using the
particular IMSI, then indeed there is an MS that reached that
stage of its protocol role, for that IMSI and KeNB .
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
l e t processMS =
new imsi ms : i d e n t ;
new k i : key ;
i n s e r t keys ( imsi ms , k i ) ;
l e t cap ms : bool = e n c C a p a b i l i t y ( ) i n
out ( pubChannel , (CAP, cap ms ) ) ;
out ( pubChannel , ( ID , imsi ms ) ) ;
i n ( pubChannel , (=CHALLENGE, rand ms : nonce ,
= f 1 ( k i , rand ms ) , snid ms : i d e n t ) ) ;
l e t res ms : resp = f 2 ( k i , rand ms ) i n
l e t ck ms : cipherKey = f 3 ( k i , rand ms ) i n
l e t ik ms : i n t e g K e y = f 4 ( k i , rand ms ) i n
l e t kasme ms : asmeKey = kdf asme ( ck ms , ik ms , snid ms ) i n
event begSN ( imsi ms , snid ms , kasme ms ) ;
out ( pubChannel , (RES, res ms ) ) ;
l e t knasenc ms = kdf nas enc ( kasme ms ) i n
l e t knasint ms = k d f n a s i n t ( kasme ms ) i n
i n ( pubChannel , (=NASSMC, enableEnc nas ms : bool , =cap ms ,
= f i n t e g n a s ( ( enableEnc nas ms , cap ms ) , knasint ms ) ) ) ;
event endMS ( imsi ms , snid ms , kasme ms , cap ms ) ;
out ( pubChannel , sencrypt nas ( s e c r e t , knasenc ms ) ) ;
out ( pubChannel , s e n c i n t n a s ( s e c r e t , knasint ms ) ) ;
i f enableEnc nas ms = f a l s e then
out ( pubChannel , ( NASSMComplete , nas smcomplete msg ,
f i n t e g n a s ( nas smcomplete msg , knasint ms ) ) ) ;
pMSAS( kasme ms , imsi ms , cap ms )
else
out ( pubChannel ,
( NASSMComplete , sencrypt nas ( nas smcomplete msg ,
knasenc ms ) , f i n t e g n a s ( sencrypt nas (
nas smcomplete msg , knasenc ms ) , knasint ms ) ) ) ;
pMSAS( kasme ms , imsi ms , cap ms ) .
Fig. 6.
7
8
9
10
VII.
In Sect. III we annotate the protocol diagrams to mark

blocks of message exchanges, which are composed to form
the interoperation scenarios in Sect. V. Where it is convenient,
we use sub-processes in our PV models to express this structure. To make the PV model for an interoperation scenario,
we can easily combine these sub-processes and other code
fragments that correspond to blocks, with minor modifications
(adding conversion functions that enable a BS to perform a
particular SMC procedure, and adding keys to the AV in S9
and S10).
For example, for the MS in LTE we factor out a process
that models the first four blocks of LTE. This
process is reused in the models for scenarios S9 and S10. If
the assumptions that underly our scenarios for uncertain cases
turn out to be wrong, we expect to be able to easily model
the corrected scenarios as well. For security specifications, the
blocks already include events and the queries are easily adapted
from queries for the pure protocols.
processMS
Of the 10 AKA scenarios, 5 of them are the same scenarios

as in the roaming cases of GSM and UMTS, for which the
models and analysis appears in [16]. One of them is the pure
4G AKA, which is modeled and analyzed in Sect. VI. In this
section, we discuss the models of the 4 new scenarios, and
then summarize results for all 10 scenarios.
MS process for LTE
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
query x1 : i d e n t , x2 : enbKey , x3 : bool ;
event (endMS ENB( x1 , x2 , x3 ) )
event (begMS ENB( x1 , x2 , x3 ) ) .
query x1 : i d e n t , x2 : enbKey ; event ( endENB ( x1 , x2 ) )
event ( begENB ( x1 , x2 ) ) .
The payload can be learned by the attacker when the MS is not

capable of encryption, and indeed PV finds violations of the
secrecy property in query line 1. Conditional secrecy, query
line 2, says that if the attacker obtains the secret payload then
the event disableEnc must have previously taken place this is
proved by PV. To test the secrecy of the keys, the MS encrypts
a fresh secret (a private free name in the code, not shown in
Fig. 6) under each of the keys and sends the ciphertexts on the
public channel (lines 4344 and 1719), and query line 3 tests
the secrecy. PV proves conditional secrecy and key secrecy.
M ODELING AND ANALYZING INTEROPERATION IN

P ROV ERIF
Scenario S7: LTE I k UMTS IIIII k [LTE IV] k LTE V,

conv(CK IK KASME , MME). Fig. 7 elaborates the scenario
in Fig. 4 with details of the PV model and shows the locations
of the events which are used to specify authentication and
conditional payload secrecy. Most of the code in this model
is inherited from the 4G model and the UMTS model. The
secrecy and authentication properties are specified similar to
the ones in the 4G model:
1
2
3
4
5
6
query x1 : i d e n t , x2 : cipherKey , x3 : i n t e g K e y ;
event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 , x3 ) )
event ( begMS ( x1 , x2 , x3 ) ) .
As in pure 4G, plain secrecy of the message payload does not

hold because the attacker can always learn the payload if the
MS is not capable of encryption. Conditional secrecy (query
Authentication of the MS to the MME is specified in

query lines 45. This refers to event endSN placed following
message 10 (Fig. 5) so that it follows both verification of the
8
MME
4G BS
4G ME with USIM
TABLE IV.
3G HN
LTE I
1.CAP
2. IMSI
3. IMSI
UMTS II
Auth. of
MS to
VLR/
SGSN/MME
Auth. of
VLR/
SGSN/MME
to MS
Scenario
Conditional
secrecy
Key
secrecy
S1
Proved
Proved
Proved
N/A
S2
S3
Proved
Proved
Proved
Proved
Proved
Proved
N/A
Proved
S4
Proved
Proved
Proved
N/A
S5
Proved
Proved
Proved
N/A
S6
Proved
Proved
Proved
N/A
S7 w/o
LTE IV
Proved
Proved
Proved
N/A
Proved
Proved
Proved
Proved
Proved
Proved
Proved
Proved
Proved
Proved
Proved
Proved
Proved
CMC attack
Proved
Proved
Proved
N/A
known false
base station
attack
Proved
Proved
Proved
Proved
Proved
Proved
Proved
Proved
N/A
Proved
Generate RAND ,MAC = f1(Ki, RAND)

IK = f4(Ki, RAND), AUTN=MAC
4. IMSI, RAND, AUTN,
A NALYSIS RESULTS
XRES, CK, IK
5. RAND, AUTN
UMTS III
XMAC = f1(Ki, RAND)

event begSN(imsi_ms, ck_ms, ik_ms)
6. RES
Verify RES = XRES
event endSN(imsi_sn, ck_sn, ik_sn)
KASME = KDF(CK, IK)
KASME = KDF(CK, IK)

7. CAP, KeNB
KeNB = KDF(KASME)
LTE V
KeNB = KDF (KASME), KRRCenc = KDF (KeNB)

KRRCint = KDF(KeNB), KUPenc = KDF (KeNB)
Decide enableENC,
AS-MAC = EIA(enableEnc, KRRCint)
event begMS(imsi_sn, kenb_sn, cap_sn)
S7 w/
LTE IV
S8
S9 w/
LTE IV
8. enableEnc,
AS-MAC
XAS-MAC = EIA(enableEnc, KRRCint)
S9 w/o
LTE IV
S10 w/
LTE IV
S10
w/o
LTE IV
event endMS(imsi_ms, kenb_ms, cap_ms)

9. AS SMComplete
Integrity protected
10. payload, if no encryption
{payload}_KRRCenc, otherwise
Auth. of BS
to MS
known false
base station
attack
Proved
Proved
known false
base station
attack
Proved
known false
base station
attack
false base
station
attack
Proved
Decrypt message
if enableEnc_ms is true
violated because the BS could choose to disable encryption

when communicating with the MS.
Fig. 7. Authentication scenario S7, version without LTE IV, annotated in

accord with our model
Scenario S10: UMTS I k LTE IIIII k [LTE IV] k

UMTS IV, AV = 4G AV + CK + IK. ProVerif proves all the
properties except the payload secrecy.
line 1) does hold. Secrecy of keys (line 2) is also proved.

Authentication of the MS to the SN is specified in lines 34
and is proved. Authentication of the SN to the MS is specified
in lines 56. For the version without LTE IV, PV finds an
attack that violates the property. The attacker intercepts the
capability message sent by the MS and replaces the capabilities
with different ones. The event endMS is executed after the MS
receives the SMC message. Because the SMC message does
not contain the received MSs capabilities, the MS has no way
to confirm whether the SN receives the correct capabilities.
PV detects the violation because, although there was a begMS
event, it has a different value for capabilities. For the version
with LTE IV, the property is proved.
Analysis Results.
Table IV gives results for all the 10
scenarios. In the model of scenario S9 without LTE IV, we
find the known false base station attack [1] which has the same
attack scenario as in the native GSM AKA, i.e., in S1 and S4.
In this attack, the attacker intercepts the CAP message and
modifies the capabilities of the MS as no-encryption. When the
BS decides which algorithm to use, the BS has to choose not
to enable encryption. Because the subsequent traffic between
the MS and the 2G BS is not encrypted nor integrity protected,
the attacker can both eavesdrop and modify the messages.
The attack found in scenario S7 without LTE IV is similar.
The attacker intercepts and modifies the capabilities of MS
to no-encryption to force the 4G BS to choose not to use
encryption. Although integrity protection is mandatory for the
signaling traffic of 4G BS, there is no integrity protection on
the user plane traffic, so the attack can both eavesdrop and
modify the data traffic.
Scenario S8: LTE I k UMTS IIIII k LTE IVV,

conv(CK IK nonces KASME , MME). ProVerif proves all
the properties except the payload secrecy.
Scenario S9: GSM I k LTE IIIII k [LTE IV] k
GSM IV, conv(CK IK Kc, MME), AV = 4G AV +
CK + IK. In the models (with or without LTE IV) of
this scenario, the MME uses the key conversion function
fun c3(cipherKey, integKey): gsmKey to derive the GSM session
key from the UMTS cipher and integrity keys. Because the
BS is the GSM BS, the false base station attack on the AKA
without LTE IV is found when checking the authentication of
the BS to the MS. In the model with LTE IV, an attack is found
when checking the authentication of the BS to the MS. In the
attack, the attacker modifies the CMC message (which is not
integrity protected) to tell the MS to use no encryption. This
attack will be detected by the BS once the MS sends messages
to the BS. As in other scenarios, the payload secrecy could be
In the model of scenario S9 with LTE IV, we find an attack

in which the attacker simply modifies the CMC message to tell
the MS to use no encryption. This attack would be detected
once the MS sends unencrypted messages to the BS.
VIII.
C ONCLUSION
In this paper we study authentication and key agreement

(AKA) for interoperation among GSM, UMTS and LTE. To
determine the AKA procedures in each interoperation case,
we consider all combinations of the five relevant system
9
components. We classify some cases as allowed or disallowed,

based on information about component compatibility gleaned
from the standards documents. Some cases are classified as
uncertain, for lack of definite information in the standards.
For each possible (allowed or uncertain) interoperation case,
we identify and justify a particular AKA scenario built from
elements (blocks) of the pure GSM, UMTS, and LTE
protocols.
[10]
[11]
[12]
[13]
It turns out that 10 scenarios are needed to cover all the 105
possible interoperation cases. Of these scenarios, 5 involve just
GSM and UMTS and were identified previously (see Sect. II);
one is the pure LTE; the remaining 4 are new. In most cases,
the AKA scenario is completely determined by the components
involved. However, a few cases have two feasible versions of
the scenarios which differ by whether block LTE IV is included
or whether the nonce in TAU request is used.
[14]
[15]
[16]
We model and analyze pure LTE and the 4 new AKA

scenarios involving LTE components, using ProVerif, focusing
in this paper on authentication and secrecy properties. For the
scenarios involving LTE, we find three attacks. One is the false
base station attack which is inherited from the GSM system
and is also found in GSM-UMTS interoperation. Another
attack, on one version of scenario S7, is a similar false base
station attack but with a 4G BS. The attack is prevented by
including block LTE IV. In the third attack on the AKA of
scenario S9 with LTE IV, the CMC message is modified. Aside
from these attacks, the desired authentication and secrecy
properties are proved (in the symbolic model of perfect crypto,
with unbounded sessions) for all other cases.
[17]
[18]
[19]
[20]
[21]
For further work, we would like to analyze the handover

in GSM, UMTS, and LTE, as well as across the technologies.
We also are interested in exploring the interworking between
4G and non-3GPP networks.
[22]
[23]
[24]
R EFERENCES
[1]
[2]
[3]
[4]
[5]
[6]
[7]
[8]
[9]
U. Meyer and S. Wetzel, A man-in-the-middle attack on UMTS, in

ACM WiSec, 2004, pp. 9097.
, On the impact of GSM encryption and man-in-the-middle attacks
on the security of interoperating GSM/UMTS networks, in IEEE
Symposium on Personal, Indoor and Mobile Radio Communications,
2004.
3GPP TS 33.102 version 11.4.0 Release 11 Digital cellular telecommunications system (Phase 2+); Universal Mobile Telecommunications
System (UMTS); LTE; 3G security; Security architecture , http://www.
3gpp.org/ftp/Specs/html-info/33102.htm.
3GPP TS 33.401 v10.0.0; Digital cellular telecommunications system
(Phase 2+); Universal Mobile Telecommunications System (UMTS);
LTE; 3gpp System Architecture Evolution (SAE); Security architecture, http://www.3gpp.org/ftp/Specs/html-info/33401.htm.
B. Blanchet, Automatic verification of correspondences for security
protocols, Journal of Computer Security, vol. 17, no. 4, pp. 363434,
Jul. 2009.
3GPP TR 31.900 v11.0.0 Release 11; Universal Mobile Telecommunications System (UMTS); LTE; SIM/USIM internal and external interworking aspects, http://www.3gpp.org/ftp/Specs/html-info/31900.htm.
C. Tang, D. A. Naumann, and S. Wetzel, Analysis of authentication and key establishment in inter-generational mobile telephony (long version), 2013, http://www.cs.stevens.edu/naumann/pub/
TangNaumannWetzel2013.pdf.
J. D. Golic, Cryptanalysis of alleged a5 stream cipher, in EUROCRYPT, 1997.
L. G. I. Goldberg, D. Wagner, The real-time cryptanalysis of A5/2,
Rumpsession of CRYPTO, 1999.
[25]
[26]
[27]
[28]
[29]
[30]
[31]
[32]
10
S. Petrovic and A. Fster-Sabater, Cryptanalysis of the A5/2 algorithm,

Cryptology ePrint Archive, Report 2000/052, 2000, http://eprint.iacr.
org/.
E. Barkan, E. Biham, and N. Keller, Instant ciphertext-only cryptanalysis of GSM encrypted communication, J. Cryptol., vol. 21, pp.
392429, March 2008.
O. Dunkelman, N. Keller, and A. Shamir, A practical-time related-key
attack on the KASUMI cryptosystem used in GSM and 3G telephony,
in CRYPTO, 2010.
Z. Ahmadian, S. Salimi, and A. Salahi, New attacks on UMTS network
access, in Wireless Telecommunications Symposium, 2009. WTS 2009.
IEEE, 2009, pp. 16.
D. Fox, Der IMSI catcher, in DuD Datenschutz und Datensicherheit,
2002.
U. Meyer, Secure roaming and handover procedures in wireless access
networks, Ph.D. dissertation, Darmstadt University of Technology,
Germany, 2005.
C. Tang, D. A. Naumann, and S. Wetzel, Symbolic analysis for security
of roaming protocols in mobile networks, in SecureComm 2011 :
Seventh International ICST Conference on Security and Privacy in
Communication Networks, 2011.
R. Chang and V. Shmatikov, Formal analysis of authentication in
Bluetooth device pairing, in FCS-ARSPA, 2007.
M. Jakobsson and S. Wetzel, Security weaknesses in Bluetooth, in
Cryptographers Track at the RSA Conference (CT-RSA), 2001, pp. 176
191.
B. Blanchet and A. Chaudhuri, Automated formal analysis of a
protocol for secure file sharing on untrusted storage, in IEEE Symp.
on Sec. and Priv., 2008.
L. Chen and M. Ryan, Attack, solution and verification for shared
authorisation data in TCG TPM, in Formal Aspects in Security and
Trust, 2009, pp. 201216.
S. Kremer and M. Ryan, Analysis of an electronic voting protocol in
the applied pi calculus, in ESOP, 2005, pp. 186200.
M. Arapinis, L. Mancini, E. Ritter, M. Ryan, N. Golde, K. Redon,
and R. Borgaonkar, New privacy issues in mobile telephony: fix and
verification, in ACM CCS. ACM, 2012, pp. 205216.
C. Han and H. Choi, Security analysis of handover key management
in 4G LTE/SAE network, 2012.
J.-K. Tsay and S. F. Mjlsnes, A vulnerability in the UMTS and
LTE authentication and key agreement protocols, in Computer Network
Security. Springer, 2012, pp. 6576.
M.-F. Lee, N. P. Smart, B. Warinschi, and G. J. Watson, Anonymity
guarantees of the UMTS/LTE authentication and connection protocol,
IACR Cryptology ePrint Archive, vol. 2013, p. 27.
M. A. Mobarhan, M. A. Mobarhan, and A. Shahbahrami, Evaluation
of security attacks on UMTS authentication mechanism, International
Journal of Network Security & Its Applications, vol. 4, no. 4, 2012.
TS 23.060 version 11.5.0 Release 11; Digital cellular telecommunications system (Phase 2+); Universal Mobile Telecommunications System
(UMTS); General Packet Radio Service (GPRS); Service description;
Stage 2, http://www.3gpp.org/ftp/Specs/html-info/23060.htm.
3GPP TS 23.401 version 11.4.0 Release 11; LTE; General Packet
Radio Service (GPRS) enhancements for Evolved Universal Terrestrial
Radio Access Network (E-UTRAN) access, http://www.3gpp.org/ftp/
Specs/html-info/23401.htm.
Digital cellular telecommunications system (Phase 2+); Mobile radio
interface layer 3 specification (GSM 04.08 version 7.8.0 Release 1998),
1998.
D. Forsberg, G. Horn, W.-D. Moeller, and V. Niemi, LTE Security.
John Wiley and Sons, Ltd, 2010.
3GPP TS 24.301 version 11.4.0 Release 11; Universal Mobile Telecommunications System (UMTS); LTE; Non-Access-Stratum
(NAS) protocol for Evolved Packet System (EPS); Stage 3, http:
//www.3gpp.org/ftp/Specs/html-info/24301.htm.
A. D. Gordon and A. Jeffrey, Authenticity by typing for security
protocols. Journal of Computer Security, pp. 451520, 2003.
A PPENDICES
Sect. A gives the complete table of cases and Sect. B gives
the complete table of scenarios. Sect. C presents the models
of the scenarios and Sect. D gives the complete code.
A PPENDIX A
TABLE OF CASES
Figures 8 14 show the classification the 243 interoperation cases. The table makes reference to the list of reasons
R1R7 in Sect. IV and the list of conditions A1A4 at the end
of Sect. IV.
Components
ID
As stated in the main body of the paper, rows in normal

font with no color indicate the allowed cases. Green color and
bold font indicates the uncertain cases. Grey color and italic
font indicates the disallowed cases. Blue color and bold italic
font indicates the cases involving only 2G/3G components.
Components
ID
Identity
Module
1
2
3
4
5
6
7
8
9
10
11
12
13
14 4G
USIM
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
4G
34
USIM
35
36
37
38
39
40
Fig. 8.
ME
4G
3G
BS
VLR/SG
SN/
MME
HN
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
Condition to
support
Occurrence
Identity
Module
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67 4G
68 USIM
69
70
71
72
73
74
75
76
77
78
79
80
Reasons for
Disallowance
A1, A4
A1, A4
R5
R4
R4
A2, A4
A1, A2, A4
A1, A2, A4
R5
A2
A2
R4
R4
A2
R6
A1, A2, A3, A4
A1, A2, A3, A4
R5
A2, A3
A2, A3
R4
R4
A2, A3
R3
A1, A4
A1, A4
ME
3G
2G
BS
VLR/SG
SN/
MME
HN
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
2G
2G
R3, R5
Fig. 9.
R3, R4
R4
R3
A1, A2, A4
A1, A2, A4
R3, R5
Table of cases, part 1 of 7
11
Table of cases, part 2
Condition to
support
Occurrence
Reasons for
Disallowance
A2
A2
R3, R4
R4
A2
R3
A1, A2, A3, A4
A1, A2, A3, A4
R3, R5
A2, A3
A2, A3
R3, R4
R4
A2, A3
R2
R2
A1, A4
R2, R5
R2
R2, R4
R2, R4
R2
R2
A1, A2, A4
R2, R5
R2
A2
R2, R4
R2, R4
A2
R2
R2
A1, A2, A3, A4
R2, R5
R2
A2, A3
R2, R4
R2, R4
Components
ID
Identity
Module
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95 USIM
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
USIM
115
116
117
118
119
120
Fig. 10.
ME
BS
VLR/SG
SN/
MME
2G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
4G
3G
HN
2G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
3G
Condition to
support
Occurrence
Components
Reasons for
Disallowance
ID
Identity
Module
121
122
123
124
125
126
127
128 USIM
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148 USIM
149
150
151
152
153
154
155
156
157
158
159
160
A2, A3
A1, A4
A1, A4
R5
R4
R4
A1, A4
A1, A4
A1, A4
R5
A2
A2
R4
R4
A2
R6
A1, A4
A1, A4
R5
A2
A2
R4
R4
A2
R3
A1, A4
A1, A4
R3, R5
R3, R4
R4
R3
A1, A4
A1, A4
Fig. 11.
12
ME
3G
2G
BS
VLR/SG
SN/
MME
HN
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
2G
Condition to
support
Occurrence
Reasons for
Disallowance
R3, R5
R3, R4
R4
R3
A1, A4
A1, A4
R3, R5
R7
R3, R4
R4
R2
R2
A1, A4
R2, R5
R2
R2, R4
R2, R4
R2
R2
A1, A4
R2, R5
R2
R2, R4
R2, R4
R2
R2
A1, A4
R2, R5
R2
R2, R4
Components
ID
Components
ID
Identity
Module
161
USIM
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176 SIM
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195 SIM
196
197
198
199
200
Fig. 12.
ME
2G
4G
3G
BS
VLR/SG
SN/
MME
HN
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
2G
2G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
Condition to
support
Occurrence
Identity
Module
201
202
203
204
205
206
207
208
SIM
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
SIM
229
230
231
232
233
234
235
236
237
238
239
240
Reasons for
Disallowance
R2, R4
R1
R1
R1
R1, R5
R1, R4
R1, R4
R1
R1
R1
R1, R5
R1, R4
R4
R1
R1
R1
R1, R5
R1, R4
R4
R1, R3
R1
R1
R1, R3, R5
Fig. 13.
ME
3G
2G
BS
VLR/SG
SN/
MME
HN
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
3G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
4G
4G
4G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
2G
Condition to
support
Occurrence
Reasons for
Disallowance
R1
R1, R3, R5
R1, R3, R4
R4
R1, R3
R1
R1
R1, R3, R5
R1, R3, R4
R4
R1, R2
R1, R2
R1
R1, R2, R5
R1, R2
R1, R2, R4
R1, R2, R4
R1, R2
R1, R2
R1
R1, R2, R5
R2
R1, R2, R4
R2, R4
R1, R2
R1, R2
R1
R1, R5
R1, R2
R1, R3, R4
R1, R4
R1, R3
R1
Components

ID
Identity
Module
241
242 SIM
243
Fig. 14.
13
ME
BS
VLR/SG
SN/
MME
2G
4G
3G
2G
2G
2G
2G
HN
2G
2G
2G
Condition to
support
Occurrence
Reasons for
Disallowance
R1, R2, R4
R2, R4
A PPENDIX B
TABLE OF SCENARIOS
Components
ID
Figure 15 17 show the determination of the AKA

scenarios and respective reasoning, with reference to the list
AX in Table II.
Components
ID
Identity
Module
1
2
3
5
6
9
10
11
4G
12
USIM
14
15
18
20
21
23
24
27
29
30
32
33
36
38
39
41
42
45
47
48
50
51
54
57
60
63
66
69
72
75
78
ME
4G
3G
2G
81
82
83
84
86
87
90
91
92
93 USIM
95
96
99
101
102
104
105
108
110
111
113
114
117
119
120
USIM
122
123
126
128
129
132
135
138
141
144
147
USIM
150
153
156
159
Reason
Scenarios
BS
VLR/SG
SN/
MME
HN
4G
3G
2G
3G
2G
2G
4G
3G
2G
3G
2G
2G
3G
2G
3G
2G
2G
3G
2G
3G
2G
2G
3G
2G
3G
2G
2G
3G
2G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
2G
4G
4G
4G
3G
3G
2G
4G
4G
4G
3G
3G
2G
4G
4G
3G
3G
2G
4G
4G
3G
3G
2G
4G
4G
3G
3G
2G
4G
4G
3G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
S3
S10
S9
S2
S6
S4
S7/S8
S2
S6
S2
S6
S4
S5
S1
S5
S1
S1
S10
S9
S2
S6
S4
S2
S6
S2
S6
S4
S5
S1
S5
S1
S1
S9
S6
S4
S6
S6
S4
S1
S1
Stated in
Spec
A, G, K, W
B, H, V
B, I, N, V
H, V
I, N, V
I, V
G, K, W, X
H, V
I, N, V
C, H, V
C, I, N, V
I, V
E, H, M, V
E, I, V
E, H, M, V
E, I, V
E, I, V
B, H, K, V
B, I, L, N, V
H, K, V
I, L, N, V
I, L, V
H, K, V
I, L, N, V
C, H, K, V
C, I, L, N, V
I, L, V
E, H, K, M, V
E, I, L, V
E, H, K, M, V
E, I, L, V
E, I, L, V
B, I, K, N, V
I, K, N, V
I, K, V
I, K, N, V
C, I, K, N, V
I, K, V
E, I, K, V
E, I, K, V
Identity
Module
Interpretation
T
T
O, T
O, T
P, T
Q, U
Q, T
Q, T
T
T
R, T
T
T
T
T
T
O
O
P
Q
Q
O
P
Q
Fig. 16.
ME
BS
VLR/SG
SN/
MME
2G
2G
4G
3G
2G
3G
2G
2G
4G
3G
2G
3G
2G
2G
3G
2G
3G
2G
2G
3G
2G
3G
2G
2G
3G
2G
3G
2G
2G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
2G
2G
2G
4G
4G
4G
3G
3G
2G
4G
4G
4G
3G
3G
2G
4G
4G
3G
3G
2G
4G
4G
3G
3G
2G
4G
4G
3G
3G
2G
4G
4G
3G
2G
4G
3G
2G
4G
3G
2G
4G
3G
4G
3G
2G
Reason
Scenarios
HN
2G
4G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
3G
2G
2G
2G
2G
2G
4G
4G
4G
4G
4G
3G
3G
3G
3G
3G
2G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
S1
S3
S10
S9
S2
S6
S4
S7/S8
S2
S6
S2
S6
S4
S5
S1
S5
S1
S1
S2
S6
S2
S6
S4
S2
S6
S2
S6
S4
S5
S1
S1
S1
S6
S6
S4
S6
S6
S4
S1
S1
Stated in
Spec
E, I, K, V
A, G, J, K, W
B, H, V
B, I, N, V
H, V
I, N, V
I, V
G, K, W, X
H, V
I, N, V
C, H, V
C, I, N, V
D, I, V
E, H, M, V
E, I, V
E, H, M, V
E, I, V
E, I, V
B, H, K, V
B, I, L, N, V
H, K, V
I, L, N, V
I, L, V
H, K, V
I, L, N, V
C, H, K, V
C, I, L, N, V
D, I, L, V
E, H, K, M, V
E, I, L, V
E, I, L, V
E, I, L, V
B, I, K, N, V
I, K, N, V
I, K, V
I, K, N, V
C, I, K, N, V
D, I, K, V
E, I, K, V
E, I, K, V
T
T
O, T
O, T
P, T
Q, U
Q, T
Q, T
T
T
T
T
T
T
T
T
O
O
P
Q
Q
O
P
Q
Table of scenarios, part 2
Components
ID
Fig. 15.
Interpretation
Table of scenarios, part 1 of 3

162
167
168
171
176
177
180
185
186
189
194
195
198
203
204
207
212
213
216
222
225
231
234
240
243
Fig. 17.
14
Identity
Module
ME
USIM
2G
SIM
4G
SIM
3G
SIM
2G
Reason
Scenarios
BS
VLR/SG
SN/
MME
HN
2G
3G
2G
2G
3G
2G
2G
3G
2G
2G
3G
2G
2G
3G
2G
2G
3G
2G
2G
2G
2G
2G
2G
2G
2G
2G
3G
3G
2G
3G
3G
2G
3G
3G
2G
3G
3G
2G
3G
3G
2G
3G
3G
2G
3G
2G
3G
2G
3G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
4G
3G
3G
3G
2G
2G
2G
4G
4G
3G
3G
2G
2G
Table of scenarios, part 3
S1
S5
S1
S1
S5
S1
S1
S5
S1
S1
S5
S1
S1
S5
S1
S1
S5
S1
S1
S1
S1
S1
S1
S1
S1
Stated in
Spec
E, I, K, V
H, M, V
I, V
I, V
F, H, M, V
F, I, V
F, I, V
E, H, M, V
E, I, V
E, I, V
H, K, M, V
I, L, V
I, L, V
F, H, K, M, V
F, I, L, V
F, I, L, V
E, H, K, M, V
E, I, L, V
E, I, L, V
I, K, V
I, K, V
F, I, K, V
F, I, K, V
E, I, K, V
E, I, K, V
Interpretation
S, T
S, T
S, T
T
T
T
T
T
T
S
S
S
S
S
A PPENDIX C
MODELS OF THE SCENARIOS
This section presents scenarios S7 (without LTE IV), S8,
S9+ (with LTE IV) and S10+ (with LTE IV) with some
explanation. The pure 4G model is discussed in Sect. VI.
The other pure models and scenarios are presented in [16].
Appendix D gives the complete code files for all models.
58
59
60
61
62
63
64
65
66
67
68
S7. LTE I k UMTS IIIII k LTE V, conv(CK IK KASME ,

MME)
69
70
71
72
Most of the code in this model is inherited from the 4G

model and the UMTS model. The key derivation function used
by the MME and the MS to generate the local master key
KASME is declared as:
fun kdf asme ( cipherKey , i n t e g K e y ) : asmeKey .
73
74
75
76
77
78
79
80
81
There are three main processes in our model representing the

behavior of the MS, the SN and the HN respectively.
82
83
84
85
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
(MS nond e t e r m i n i s t i c a l l y choose

t h e c a p a b i l i t y o f e n c r y p t i o n )
( Send o u t cap ms t o SN )
( Send o u t permanent ID )
( I n p u t c h a l l e n g e message from SN )
i n ( pubChannel , (=CHALLENGE, rand ms : nonce , mac ms : mac ) ) ;
i f f 1 ( k i , rand ms ) = mac ms then
( Compute response and e n c r y p t i o n key )
(MS i s a u t h e n t i c a t i n g i t s e l f t o SN)
event begSN ( imsi ms , ck ms , ik ms ) ;
( Send o u t response t o SN )
l e t kasme ms = kdf asme ( ck ms , ik ms ) i n
( Receive GSM c i p h e r mode command )
= f i n t e g a s ( b o o l 2 b i t s t r i n g ( enableEnc as ms ) ,
kasint ms ) ) ) ;
event endMS ( imsi ms , kenb ms , cap ms ) ;
out ( pubChannel , s e n c r y p t ( s e c r e t , ck ms ) ) ;
out ( pubChannel , s e n c r y p t I n t e g ( s e c r e t , ik ms ) ) ;
kasenc ms ) i n 0 .
86
87
88
89
90
39
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
l e t processSN =
( Receive MS s c a p a b i l i t y )
i n ( pubChannel , (=CAP, cap sn : bool ) ) ;
( Receive permanent ID )
i n ( pubChannel , (= ID , i m s i s n : i d e n t ) ) ;
( Send o u t a u t h e n t i c a t i o n v e c t o r r e q u e s t )
out ( secureChannel , (AV REQ, i m s i s n ) ) ;
( Receive a u t h e n t i c a t i o n v e c t o r )
i n ( secureChannel , (=AV, =imsi sn , rand sn : nonce ,
xres sn : resp , ck sn : cipherKey , i k s n : integKey ,
mac sn : mac ) ) ;
( Send a u t h e n t i c a t i o n c h a l l e n g e t o MS )
out ( pubChannel , (CHALLENGE, rand sn , mac sn ) ) ;
( Receive response )
i n ( pubChannel , (=RES, res sn : resp ) ) ;
( Check whether r e c e i v e d response equal t o XRES)
i f res sn = xres sn then
( At t h i s p o i n t , SN a u t h e n t i c a t e d MS)
event endSN ( imsi sn , ck sn , i k s n ) ;
l e t processHN =
( Receive a u t h e n t i c a t i o n v e c t o r r e q u e s t )
i n ( secureChannel , (=AV REQ, imsi hn : i d e n t ) ) ;
( Generate a f r e s h random number )
new rand hn : nonce ;
( Computes expected response and Kc )
get keys (= imsi hn , k i h n ) i n
l e t mac hn : mac = f 1 ( ki hn , rand hn ) i n
l e t xres hn : resp = f 2 ( ki hn , rand hn ) i n
l e t ck hn : cipherKey = f 3 ( ki hn , rand hn ) i n
l e t i k h n : i n t e g K e y = f 4 ( ki hn , rand hn ) i n
( Send o u t a u t h e n t i c a t i o n v e c t o r )
out ( secureChannel , ( AV, imsi hn , rand hn ,
xres hn , ck hn , ik hn , mac hn ) ) .
The HN process is the same as the one in the UMTS model.

In line 19 and line 58, the MS and the SN derive the local
master key KASME from the cipher key and the integrity key.
Security Property Specifications and Findings The
events used in the correspondence assertions to specify the
authentication properties are declared as:
1
2
3
4
event
event
event
event
begSN ( i d e n t
endSN ( i d e n t
begMS ( i d e n t
endMS ( i d e n t
,
,
,
,
cipherKey , i n t e g K e y ) .
cipherKey , i n t e g K e y ) .
enbKey , bool ) .
enbKey , bool ) .
The secrecy and authentication properties are specified as:

1
2
3
4
5
6
7
event ( begSN ( x1 , x2 , x3 ) ) .
event ( begMS ( x1 , x2 , x3 ) ) .
The secrecy property of the message payload does not hold,

because the attacker can always learn the payload if the MS
is not capable of encryption. The conditional secrecy (line 2)
holds. That means if the encryption is enabled, the attacker can
never learn the message payload. The property specified in line
3 is used to test the secrecy of the keys. ProVerif proves the key
secrecy. The authentication of the MS to the SN is specified
in lines 45. ProVerif proves this authentication property. The
authentication of the SN to the MS is specified in lines 67.
Proverif finds a attack trace that violates the property:
38
40
l e t kasme sn = kdf asme ( ck sn , i k s n ) i n

l e t kenb sn : enbKey = kdf enb ( kasme sn ) i n
l e t kasenc sn : asEncKey = kdf as enc ( kenb sn ) i n
l e t k a s i n t s n : a s I n t K e y = k d f a s i n t ( kenb sn ) i n
l e t kupenc sn : upEncKey = kdf up enc ( kenb sn ) i n
event begMS ( imsi sn , kenb sn , cap sn ) ;
out ( pubChannel , (ASSMC, cap sn ,
f i n t e g a s ( b o o l 2 b i t s t r i n g ( cap sn ) , k a s i n t s n ) ) ) ;
i n ( pubChannel , (= ASSMComplete , =as smcomplete msg ,
= f i n t e g a s ( as smcomplete msg , k a s i n t s n ) ) ) ;
i f cap sn = f a l s e then
event d i s a b l e E n c ;
out ( pubChannel , (MSG, payload ,
f i n t e g a s ( payload , k a s i n t s n ) ) )
else
out ( pubChannel , (MSG, s e n c r y p t a s ( payload ,
kasenc sn ) , f i n t e g a s ( s e n c r y p t as ( payload ,
kasenc sn ) , k a s i n t s n ) ) ) .
1
2
3
4
5
6
7
8
9
15
new imsi ms c r e a t i n g imsi ms 5870 a t {2} i n copy a

new k i c r e a t i n g ki 5871 a t {3} i n copy a
i n s e r t keys ( imsi ms 5870 , ki 5871 ) a t {4} i n copy a
out ( pubChannel , (CAP, t r u e ) ) a t {6} i n copy a
out ( pubChannel , ( ID , imsi ms 5870 ) ) a t {7} i n copy a
i n ( pubChannel , (CAP, a 5860 ) ) a t {31} i n copy a 5861
i n ( pubChannel , ( ID , imsi ms 5870 ) ) a t {32} i n copy a 5861
i n ( pubChannel , (CAP, as smcomplete msg ) ) a t {31} i n copy a 5862
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

i n ( pubChannel , (CAP, as smcomplete msg ) ) a t {31} i n copy a 5865
out ( secureChannel , (AV REQ, imsi ms 5870 ) ) a t {33} i n
copy a 5865 r e c e i v e d a t {55} i n copy a 5859
new rand hn c r e a t i n g rand hn 5872 a t {56} i n copy a 5859
get keys ( imsi ms 5870 , ki 5871 ) a t {57} i n copy a 5859
out ( secureChannel , ( AV, imsi ms 5870 , rand hn 5872 ,
f 2 ( ki 5871 , rand hn 5872 ) , f 3 ( ki 5871 , rand hn 5872 ) ,
f 4 ( ki 5871 , rand hn 5872 ) , f 1 ( ki 5871 , rand hn 5872 ) ) )
a t {62} i n copy a 5859 r e c e i v e d a t {34} i n copy a 5865
out ( pubChannel , (CHALLENGE, rand hn 5872 , f 1 ( ki 5871 ,
rand hn 5872 ) ) ) a t {35} i n copy a 5865
i n ( pubChannel , (CHALLENGE, rand hn 5872 , f 1 ( ki 5871 ,
1
rand hn 5872 ) ) ) a t {8} i n copy a
2
event ( begSN ( imsi ms 5870 , f 3 ( ki 5871 , rand hn 5872 ) ,
3
f 4 ( ki 5871 , rand hn 5872 ) ) ) a t {13} i n copy a
4
out ( pubChannel , (RES, f 2 ( ki 5871 , rand hn 5872 ) ) )
5
a t {14} i n copy a
6
i n ( pubChannel , (RES, f 2 ( ki 5871 , rand hn 5872 ) ) )
7
a t {36} i n copy a 5865
8
event ( endSN ( imsi ms 5870 , f 3 ( ki 5871 , rand hn 5872 ) ,
9
f 4 ( ki 5871 , rand hn 5872 ) ) ) a t {38} i n copy a 5865
10
event ( begMS ( imsi ms 5870 , kdf enb ( kdf asme ( f 3 ( ki 5871 ,
11
rand hn 5872 ) , f 4 ( ki 5871 , rand hn 5872 ) ) ) ,
12
as smcomplete msg ) ) a t {44} i n copy a 5865
13
out ( pubChannel , (ASSMC, as smcomplete msg ,
f i n t e g a s ( as smcomplete msg , k d f a s i n t ( kdf enb ( kdf asme ( 14
15
f 3 ( ki 5871 , rand hn 5872 ) , f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) ) )
16
a t {46} i n copy a 5865
17
i n ( pubChannel , ( ASSMComplete , as smcomplete msg ,
f i n t e g a s ( as smcomplete msg , k d f a s i n t ( kdf enb ( kdf asme ( 18
19
f 3 ( ki 5871 , rand hn 5872 ) , f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) ) )
20
a t {47} i n copy a 5865
21
22
kdf as enc ( kdf enb ( kdf asme ( f 3 ( ki 5871 , rand hn 5872 ) ,
f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) , f i n t e g a s ( s e n c r y p t a s ( payload , 23
24
25
f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) ,
26
k d f a s i n t ( kdf enb ( kdf asme ( f 3 ( ki 5871 , rand hn 5872 ) ,
27
f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) ) )
28
a t {53} i n copy a 5865
29
i n ( pubChannel , (ASSMC, s e n c r y p t a s ( payload ,
30
f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) , f i n t e g a s ( s e n c r y p t a s ( payload , 31
32
33
f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) ,
34
k d f a s i n t ( kdf enb ( kdf asme ( f 3 ( ki 5871 , rand hn 5872 ) ,
35
f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) ) )
36
a t {20} i n copy a
37
38
f i n t e g a s ( as smcomplete msg , k d f a s i n t (
39
kdf enb ( kdf asme ( f 3 ( ki 5871 , rand hn 5872 ) ,
40
f 4 ( ki 5871 , rand hn 5872 ) ) ) ) ) ) ) a t {22} i n copy a
41
event ( endMS ( imsi ms 5870 , kdf enb ( kdf asme ( f 3 ( ki 5871 ,
42
rand hn 5872 ) , f 4 ( ki 5871 , rand hn 5872 ) ) ) , t r u e ) )
43
a t {23} i n copy a
44
The event endMS ( imsi ms 5870 , kdf enb ( kdf asme ( f 3 ( ki 5871 ,
45
rand hn 5872 ) , f 4 ( ki 5871 , rand hn 5872 ) ) ) , t r u e )
46
i s executed .
47
48
49
50
In this trace, the attacker intercepts the capability message 51

sent by the MS and replaces the capabilities with different 52
ones. Since the event beginMS in process SN records the 5453
capabilities received by the SN, which are the replaced ones. 55
The event endMS is executed after the MS receives the security 5756
mode command message. Because the security mode command 58
message does not contain the received MSs capabilities, the 59
MS has no way to confirm whether the SN receives the correct 60
61
capabilities. The event endMS is executed with recording 62
the original capabilities of the MS. The two events do not 63
agree the third parameter (the capabilities), which violates the 6564
correspondence assertion.
66
16
S8. LTE I k UMTS IIIII k LTE IVV, conv(CK IK nonces

KASME , MME)
Figure 18 shows details of the ProVerif model and the locations of the events which are used to specify the conditional
payload secrecy and the authentication properties. Most of the
code in this model is inherited from the 4G model and the
UMTS model. The key derivation function used to derive the
KASME is defined as:
fun kdf asme ( cipherKey , integKey , nonce , nonce ) : asmeKey .
There are four main processes in our model representing the

behavior of the MS, the BS, the SN and the HN respectively.
(AS SMC procedure i n process MS)
kasint ms ) ) ) ;
l e t msgcontent : b i t s t r i n g =
s d e c r y p t a s ( datamsg , kasenc ms ) i n 0 .
( process r e s p r e s e n t i n g MS)
l e t processMS =
( The i d e n t i t y o f t h e MS)
( Preshared key )
new k i : key ;
( I n s e r t i d / preshared key p a i r i n t o t h e p r i v a t e t a b l e )
(MS nond e t e r m i n i s t i c a l l y choose t h e c a p a b i l i t y o f e n c r y p t i o n )
new nonce ms : nonce ;
out ( pubChannel , (NONCE TAU, nonce ms ) ) ;
i n ( pubChannel , (=CHALLENGE, rand ms : nonce , = f 1 ( k i , rand ms ) ) ) ;
(NAS SMC procedure )
=nonce ms , nonce mme ms : nonce , nas mac : msgMac ) ) ;
l e t kasme ms : asmeKey = kdf asme ( ck ms , ik ms ,
nonce ms , nonce mme ms ) i n
l e t knasenc ms : nasEncKey = kdf nas enc ( kasme ms ) i n
l e t knasint ms : nasIntKey = k d f n a s i n t ( kasme ms ) i n
i f ( nas mac = f i n t e g n a s ( ( enableEnc nas ms , cap ms ,
nonce ms , nonce mme ms ) , knasint ms ) ) then
event endMS ( imsi ms , ck ms , ik ms , cap ms ) ;
(NAS key secrecy )
else
out ( pubChannel , ( NASSMComplete ,
sencrypt nas ( nas smcomplete msg , knasenc ms ) ,
f i n t e g n a s ( sencrypt nas ( nas smcomplete msg ,
knasenc ms ) , knasint ms ) ) ) ;
( process r e p r e s e n t i n g enodeB )
MME
BS
MS
4G HN
LTE I
1.CAP
2. IMSI
3. NONCEMS
4. IMSI
UMTS II
Generate RAND ,MAC = f1(Ki, RAND)

5. IMSI, RAND, AUTN,
XRES, CK, IK
6. RAND, AUTN
UMTS III
XMAC = f1(Ki, RAND)

event begSN(imsi_ms, ck_ms, ik_ms)
7. RES
Verify RES = XRES
event endSN(imsi_sn, ck_sn, ik_sn)
KASME = KDF(CK, IK, NONCEMS, NONCEMME)
Decide enableEnc?,
NAS-MAC = EIA((enableEnc, CAP, NONCEMS, NONCEMME), KNASint)
event begMS(imsi_sn, kasme_sn, cap_sn)
LTE IV
8. enableEnc, CAP, NONCEMS, NONCEMME, NAS-MAC

event endMS(imsi_ms, kasme_ms, cap_ms)
Verify CAP, NONCEMS
KASME = KDF(CK, IK, NONCEMS, NONCEMME)
XNAS-MAC = EIA((enableEnc, CAP,
NONCEMS, NONCEMME), KNASint)
9. NAS Security Mode Complete
ifenableEnbciphered , integrity protected
KeNB = KDF(KASME)
10. CAP, KeNB
LTE V

Decide enableEnc?, AS-MAC = EIA(enableEnc, KRRCint)
Start integrity protection
event begMS_ENB(imsi_sn, kenb_sn, cap_sn)
11. enableEnc, AS-MAC
XAS-MAC = EIA(enableEnc, KRRCint)
event endMS_ENB(imsi_ms, kenb_ms, cap_ms)
12. AS SMC Complete
Integrity protected
{payload}_KRRCenc, otherwise
Decrypt message
ifenableEnc_ms is true
Fig. 18.
67
68
69
70
71
72
73
74
75
76
77
78
79
80
Scenario S8 annotated in accord with our model
l e t processENB =
i n ( sChannelSnBts , ( kasme enb : asmeKey , imsi enb : i d e n t ,
cap enb : bool ) ) ;
l e t kenb enb : enbKey = kdf enb ( kasme enb ) i n
l e t kasenc enb : asEncKey = kdf as enc ( kenb enb ) i n
l e t k a s i n t e n b : a s I n t K e y = k d f a s i n t ( kenb enb ) i n
l e t kupenc enb : upEncKey = kdf up enc ( kenb enb ) i n
event begMS ENB( imsi enb , kenb enb , cap enb ) ;
out ( pubChannel , (ASSMC, cap enb ,
f i n t e g a s ( b o o l 2 b i t s t r i n g ( cap enb ) , k a s i n t e n b ) ) ) ;
= f i n t e g a s ( as smcomplete msg , k a s i n t e n b ) ) ) ;
i f cap enb = f a l s e then
event d i sa b l e E n c ;

f i n t e g a s ( payload , k a s i n t e n b ) ) )
81
82
83
84
85
86
else
out ( pubChannel , (MSG, s e n c r y p t a s ( payload , kasenc enb ) ,
f i n t e g a s ( s e n c r y p t a s ( payload , kasenc enb ) ,
kasint enb ) ) ) .
87
88
89
90
91
92
93
94
17
( process r e p r e s e n t i n g MME)
l e t processMME =
i n ( pubChannel , (=NONCE TAU, nonce ms sn : nonce ) ) ;
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
xres sn : resp , ck sn : cipherKey ,

i k s n : integKey , mac sn : mac ) ) ;
i n ( pubChannel , (=RES, =xres sn ) ) ;
new nonce mme : nonce ;
l e t kasme sn : asmeKey = kdf asme ( ck sn , ik sn ,
nonce ms sn , nonce mme ) i n
l e t knasenc sn : nasEncKey = kdf nas enc ( kasme sn ) i n
l e t k n a s i n t s n : nasIntKey = k d f n a s i n t ( kasme sn ) i n
event begMS ( imsi sn , ck sn , ik sn , cap sn ) ;
out ( pubChannel , (NASSMC, cap sn , cap sn , nonce ms sn ,
nonce mme , f i n t e g n a s ( ( cap sn , cap sn ,
nonce ms sn , nonce mme ) , k n a s i n t s n ) ) ) ;
i n ( pubChannel , (=NASSMComplete , msg nas : b i t s t r i n g ,
= f i n t e g n a s ( msg nas , k n a s i n t s n ) ) ) ;
i f cap sn = t r u e then
i f sdecrypt nas ( msg nas , knasenc sn )
= nas smcomplete msg then
out ( sChannelSnBts , ( kasme sn ,
imsi sn , cap sn ) )
else 0
else
i f msg nas = nas smcomplete msg then
else 0
else 0 .
1
2
Conditional Payload Secrecy

126
128
129
130
131
132
133
134
135
136
137
138
139
140
Mutual Authentication between the MS and the MME

1
2
3
4
5
6
event ( begSN ( x1 , x2 , x3 ) ) .
query x1 : i d e n t , x2 : cipherKey , x3 : integKey , x4 : bool ;
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
Authentication of the BS to the MS

1
2
3

Payload Secrecy
The analysis results are the same as the ones in 4G

authentication (Section VI). ProVerif proves all the properties
except the payload secrecy, because the BS could choose not
to enable encryption when communicating with the MS.
125
127
not a t t a c k e r (new k i ) .
( process r e p r e s e n t i n g HN)
l e t processHN =
S9+. GSM I k LTE IIIV k GSM IV, conv(CK IK Kc, MME),

AV = 4G AV + CK + IK
Figure 19 shows details of the ProVerif model and the
locations of the events which are used to specify the conditional payload secrecy and the authentication properties. Most
of the code in this model is inherited from the 4G model and
the GSM model. The MME uses the conversion function c3
to derive the GSM session key from the UMTS cipher and
integrity keys:
fun c3 ( cipherKey , i n t e g K e y ) : gsmKey .
This scenario is triggered by the TAU request, in addition to the

IMSI and capabilities, the MS generates a nonce and sends it to
the MME (lines 3435). The authentication vector request and
response procedure is modeled in lines 9396 and lines 129
140. The MME generates a nonce (line 100) and derives 1
2
the KASME using the nonces and cipher and integrity keys 3
(lines 102103). The MME then sends the integrity protected 4
NAS SMC messages which includes the received capabilities 56
and both nonces in lines 107109. Upon receiving the NAS 7
SMC messages, the MS derives the KASME using the nonces 8
and cipher and integrity keys as in MME (lines 4546). The 109
MS then verifies the MAC of the messages and sends out the 11
NAS Complete messages to the MME. The AS SMC procedure 12
13
is the same as in 4G model.
14
Security Property Specifications and Findings The
events used to specify the authentication properties are specified as:
1
2
3
4
5
6
event
event
event
event
event
event
begSN ( i d e n t , cipherKey , i n t e g K e y ) .
endSN ( i d e n t , cipherKey , i n t e g K e y ) .
begMS ( i d e n t , cipherKey , integKey , bool ) .
endMS ( i d e n t , cipherKey , integKey , bool ) .
begMS ENB( i d e n t , enbKey , bool ) .
endMS ENB( i d e n t , enbKey , bool ) .
15
16
17
18
19
20
21
22
23
24
25
26
27
We specify the security properties as following:

Key Secrecy
28
29
30
31
18
There are four main processes in our model representing the

behavior of the MS, the BS, the SN and the HN respectively.
l e t pMSAS( kc ms : gsmKey , imsi ms : i d e n t , cap ms : bool ) =
i n ( pubChannel , (=ASSMC, enableEnc as ms : bool ) ) ;
event endMS AS ( imsi ms , kc ms , cap ms ) ;
out ( pubChannel , CMComplete ) ;
i n ( pubChannel , (=MSG, datamsg : b i t s t r i n g ) ) ;
out ( pubChannel , s e n c r y p t a s ( s e c r e t , kc ms ) ) ;
l e t msgcontent : b i t s t r i n g = s d e c r y p t a s ( datamsg , kc ms )
in 0.
l e t processMS =
( Preshared key )
new k i : key ;
MME
2G BS
4G MS
4G HN
GSM I
1.CAP
2. IMSI
LTE II
3. IMSI, SNid,
Network Type
Generate RAND , MAC = f1(Ki, RAND)
KASME= KDF(CK, IK, SNid)
4. IMSI, SNid, CK, IK
RAND, AUTN, XRES, KASME
5. RAND, AUTN, SNid
LTE III
XMAC = f1(Ki, RAND)

KASME = KDF(CK, IK, SNid,)
6. RES
Verify RES = XRES
Decide enableEnc?,
NAS-MAC = EIA((enableEnc, CAP), KNASint)
KNASenc = KDF (KASME)

KNASint = KDF(KASME)
LTE IV
7. enableEnc, CAP, NAS-MAC

XNAS-MAC = EIA((enableEnc, CAP), KNASint)
if enableEnb ciphered , integrity protected
KC = c3(CK, IK)
KC = c3(CK, IK)
9. CAP, KC
Decide enableEnc?
GSM IV
event begMS_AS(imsi_sn, kc_sn, cap_sn)

10. enableEnc
event endMS_AS(imsi_ms, kc_ms, cap_ms)
11. CMComplete

{payload}_KC, otherwise
Decrypt message
Fig. 19.
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
Scenario S9+ annotated in accord with our model

50
51
52
53
i n ( pubChannel , (=NASSMC, enableEnc nas ms : bool , =cap ms , 54
= f i n t e g n a s ( ( enableEnc nas ms , cap ms ) , knasint ms ) ) ) 55
;
56
(NAS key secrecy )
57
58
59
l e t kc ms : gsmKey = c3 ( ck ms , ik ms ) i n
60
61
out ( pubChannel , ( NASSMComplete , nas smcomplete msg , 62
63
pMSAS( kc ms , imsi ms , cap ms )
64
else
65
66
67
19

pMSAS( kc ms , imsi ms , cap ms ) .
l e t processBS =
i n ( sChannelSnBts , ( kc bs : gsmKey ,
i m s i b s : i d e n t , cap bs : bool ) ) ;
event begMS AS ( imsi bs , kc bs , cap bs ) ;
out ( pubChannel , (ASSMC, cap bs ) ) ;
i n ( pubChannel , =CMComplete ) ;
i f cap bs = f a l s e then
out ( pubChannel , (MSG, payload ) )
else
out ( pubChannel , (MSG, s e n c r y p t a s ( payload , kc bs ) ) ) .
l e t processSN =
new snid sn : i d e n t ;
out ( secureChannel , (AV REQ, imsi sn , snid sn ) ) ;
i n ( secureChannel , (=AV, imsi hn sn : i d e n t ,
snid hn sn : i d e n t , rand sn : nonce ,
xres sn : resp , mac sn : mac , kasme sn : asmeKey ,
ck sn : cipherKey , i k s n : i n t e g K e y ) ) ;
out ( pubChannel , (CHALLENGE, rand sn , mac sn , snid sn ) ) ;
event begMS ( imsi hn sn , snid hn sn , kasme sn , cap sn ) ;
out ( pubChannel , (NASSMC, cap sn , cap sn ,
f i n t e g n a s ( ( cap sn , cap sn ) , k n a s i n t s n ) ) ) ;
l e t kc sn : gsmKey = c3 ( ck sn , i k s n ) i n
i f sdecrypt nas ( msg nas , knasenc sn ) =
nas smcomplete msg then
event endSN ( imsi hn sn , snid hn sn , kasme sn ) ;
out ( sChannelSnBts , ( kc sn , imsi hn sn , cap sn ) )
else 0
else
else 0
else 0 .
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
1
2
3
4
event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .

1
2
query x1 : i d e n t , x2 : gsmKey , x3 : bool ;

event ( endMS AS ( x1 , x2 , x3 ) )
event ( begMS AS ( x1 , x2 , x3 ) ) .
Payload Secrecy
All the keys are proved to be remained secret. The conditional

payload secrecy also holds, that means, if the encryption is
enabled, the content of the encrypted data messages cannot be
learned by the attacker. The mutual authentication properties
between the MS and the MME are proved. However, because
the BS is the GSM BS, the CMC attack is found when
checking the authentication of the BS to the MS. As in other
models, the payload secrecy could be violated because the BS
could choose to disable encryption when communicating with
the MS.
S10+. UMTS I k LTE IIIV k UMTS IV, AV = 4G AV + CK
+ IK
l e t processHN =
i n ( secureChannel , (=AV REQ, imsi hn : i d e n t , snid hn : i d e n t ) ) ;
Figure 20 shows details of the ProVerif model and the
( Generate a t h e n i c a t i o n v e c t o r s )
locations of the events which are used to specify the condinew rand hn : nonce ;
tional payload secrecy, authentication properties. Most of the
code in this model is inherited from the 4G model and the
UMTS model. There are four main processes in our model
representing the behavior of the MS, the BS, the SN and the
l e t kasme hn : asmeKey = kdf asme ( ck hn , ik hn , snid hn ) i n
HN respectively.
out ( secureChannel , ( AV, imsi hn , snid hn , rand hn ,
xres hn , mac hn , kasme hn , ck hn , i k h n ) ) .
1
2
l e t pMSAS( ck ms : cipherKey , ik ms : integKey ,
3
imsi ms : i d e n t , cap ms : bool ) =
The authentication vector request and response procedure is 4
i n ( pubChannel , (=ASSMC, =cap ms , enableEnc as ms : bool ,
= f 9 ( ( cap ms , enableEnc as ms ) , ik ms ) ) ) ;
modeled in lines 7276 and lines 104-114. The MME derives 5
the GSM session key in line 87 and sends the key to the GSM 76
f 9 ( as smcomplete msg , ik ms ) ) ) ;
BS in line 92 or 98 through the private channel between the 8
event endMS AS ( imsi ms , ck ms , ik ms , cap ms ) ;
MME and the GSM BS. The MS also computes the GSM 9
10
= f 9 ( datamsg , ik ms ) ) ) ;
session key in line 42. The code of the GSM SMC procedure 11
out ( pubChannel , s e n c r y p t a s ( s e c r e t , ck ms ) ) ;
out ( pubChannel , s e n c i n t a s ( s e c r e t , ik ms ) ) ;
(lines 35 and lines 5960) is inherited from the GSM model. 12
13
Security Property Specifications and Findings Since the 14
15
s d e c r y p t a s ( datamsg , ck ms ) i n 0 .
GSM BS uses the GSM session key Kc , the events used to 16
specify the authentication of the BS to the MS use this key as 17
18
one of the parameters:
19
event begMS AS ( i d e n t , gsmKey , bool ) .
event endMS AS ( i d e n t , gsmKey , bool ) .
1
2
20
21
22
23
The authentication properties between the MME and the MS

are specified the same as the ones in the 4G model. We specify
the security properties as following:
24
25
26
27
28
Key Secrecy
1
2
29
30
31
32
33
34
35
Mutual Authentication between the MS and the MME
36
37
38
20
l e t processMS =
( Preshared key )
new k i : key ;
MME
3G BS
4G MS
4G HN
UMTS I
1.CAP
2. IMSI
LTE II
3. IMSI, SNid,
Network Type
Generate RAND , MAC = f1(Ki, RAND)
KASME=KDF(CK, IK, SNid)
4. IMSI, SNid, CK, IK
RAND, AUTN, XRES, KASME
5. RAND, AUTN, SNid
LTE III
XMAC = f1(Ki, RAND)

KASME = KDF(CK, IK, SNid)
6. RES
Verify RES = XRES
Decide enableEnc?,
NAS-MAC = EIA((enableEnc, CAP), KNASint)
7. enableEnc, CAP, NAS-MAC
LTE IV

XNAS-MAC = EIA((enableEnc, CAP), KNASint)
ifenableEnb ciphered , integrity protected
9. CAP, CK, IK
Decide enableEnc?,
AS-MAC = f9((enableEnc, CAP), IK)
event begMS_AS(imsi_sn, ck_sn, ik_sn, cap_sn)
UMTS IV
10. enableEnc,
CAP, AS-MAC
XAS-MAC = f9((enableEnc, CAP), IK)
event endMS_AS(imsi_ms, ck_ms, ik_ms, cap_ms)
11. AS SMC Complete
Integrity protected
{payload}_CK, otherwise
Decrypt message
Fig. 20.
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
Scenario S10+ annotated in accord with our model

55
56
i n ( pubChannel , (=NASSMC, enableEnc nas ms : bool , =cap ms , 57
= f i n t e g n a s ( ( enableEnc nas ms , cap ms ) , knasint ms ) ) ) 58
;
59
(NAS key secrecy )
60
61
62
63
out ( pubChannel , ( NASSMComplete , nas smcomplete msg , 64
65
pMSAS( ck ms , ik ms , imsi ms , cap ms )
66
else
67
68
69
70
21
knasenc ms ) , knasint ms ) ) ) ; ( [ Msg 8 ] )

pMSAS( ck ms , ik ms , imsi ms , cap ms ) .
l e t processBS =
i n ( sChannelSnBts , ( ck bs : cipherKey , i k b s : integKey ,
event begMS AS ( imsi bs , ck bs , ik bs , cap bs ) ;
out ( pubChannel , (ASSMC, cap bs , cap bs ,
f 9 ( ( cap bs , cap bs ) , i k b s ) ) ) ;
= f 9 ( as smcomplete msg , i k b s ) ) ) ;
out ( pubChannel , (MSG, payload , f 9 ( payload , i k b s ) ) )
else
out ( pubChannel , (MSG, s e n c r y p t a s ( payload , ck bs ) ,

f 9 ( s en c r y p t a s ( payload , ck bs ) , i k b s ) ) ) .
71
72
73
l e t processSN =
i n ( secureChannel , (=AV, =imsi sn , snid hn sn : i d e n t ,
rand sn : nonce , xres sn : resp , mac sn : mac ,
kasme sn : asmeKey , ck sn : cipherKey , i k s n : i n t e g K e y ) ) ;
event begMS ( imsi sn , snid hn sn , kasme sn , cap sn ) ;
event endSN ( imsi sn , snid hn sn , kasme sn ) ;
out ( sChannelSnBts , ( ck sn , ik sn , imsi sn , cap sn ) )
else 0
else
out ( sChannelSnBts , ( ck sn , ik sn ,
else 0
else 0 .
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
Mutual Authentication between the MS and the SN

event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
1
2
3
4

event ( endMS AS ( x1 , x2 , x3 , x4 ) )
event ( begMS AS ( x1 , x2 , x3 , x4 ) ) .
1
2
Payload Secrecy
The analysis results are the same as the ones in 4G

authentication (Section VI). ProVerif proves all the properties
except the payload secrecy, because the BS could choose not
to enable encryption when communicating with the MS.
107
l e t processHN =
108
109
110
111
112
113
114
115
116
117
118
119
120
The MME sends out the authentication vector request in

line 79. Upon receiving the authentication request (line 110),
the HN generates the 4G authentication vector based on the
UMTS authentication vector. The HN then sends the 4G
authentication vectors plus the CK and the IK to the MME
(line 119120). And the MME receives the authentication
vectors in line 8082. The NAS authentication procedure
(lines 3955 and lines 8792) is the same as in the 4G model.
In line 97 and line 103104 , the MME sends the CK and the
IK to the UMTS BS on the private channel. The code of the
UMTS SMC procedure (lines 47 and lines 6366) is inherited
from the UMTS model.
Security Property Specifications and Findings Since the
UMTS BS uses the CK and the IK instead of the keys derived
from KeNB , the events used to specify the authentication of the
BS to the MS use the CK and the IK as their parameters:
event begMS AS ( i d e n t , cipherKey , integKey , bool ) .
event endMS AS ( i d e n t , cipherKey , integKey , bool ) .
1
2
We specify the security properties as following:

Key Secrecy
1
2
22
A PPENDIX D
COMPLETE CODE LISTINGS FOR ALL SCENARIOS

( Send o u t permanent ID [ Msg 2 ] )
( I n p u t c h a l l e n g e message from SN [ Msg 5 ] )
i n ( pubChannel , (=CHALLENGE, rand ms : nonce ) ) ;
l e t res ms : resp = a3 ( rand ms , k i ) i n
l e t kc ms : sessKey = a8 ( rand ms , k i ) i n
event begSN ( imsi ms , kc ms ) ;
( Send o u t response t o SN [ Msg 6 ] )
( Receive GSM c i p h e r mode command [ Msg 7 ] )
i n ( pubChannel , (=CMC, enableEnc ms : bool ) ) ;
event endMS ( imsi ms , kc ms ) ;
( Receive message from SN [ Msg 8 ] )
i n ( pubChannel , (=MSG, msg : b i t s t r i n g ) ) ;
out ( pubChannel , s e n c r y p t ( secretKc , kc ms ) ) ;
i f enableEnc ms = t r u e then
l e t msgcontent : b i t s t r i n g = s d e c r y p t ( msg , kc ms ) i n
0.
All models are checked by ProVerif version 1.86pl4.

S1. GSM I IV
( P u b l i c channel between t h e MS and t h e SN )
f r e e pubChannel : channel .
( Secure channel between t h e SN and t h e HN )
f r e e secureChannel : channel [ p r i v a t e ] .
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type sessKey .
( c o n s t a n t message headers )
const CAP: msgHdr .
const ID : msgHdr .
const AV REQ: msgHdr .
const AV : msgHdr .
const CHALLENGE: msgHdr .
const RES: msgHdr .
const CMC: msgHdr .
const MSG: msgHdr .
l e t processSN =
( Receive MS s c a p a b i l i t y [ Msg 1 ] )
( Receive permanent ID [ Msg 2 ] )
( Send o u t a u t h e n t i c a t i o n v e c t o r r e q u e s t [ Msg 3 ] )
( Receive a u t h e n t i c a t i o n v e c t o r [ Msg 4 ] )
i n ( secureChannel , (=AV, imsi hn sn : i d e n t , rand sn : nonce ,
xres sn : resp , kc sn : sessKey ) ) ;
( Send a u t h e n t i c a t i o n c h a l l e n g e t o MS [ Msg 5 ] )
out ( pubChannel , (CHALLENGE, rand sn ) ) ;
( Receive response [ Msg 6 ] )
( Check whether r e c e i v e d response equal t o expected response )
event endSN ( imsi hn sn , kc sn ) ;
(SN decide whether t o e n c r y p t messages ;
based on r e c e i v e d c a p a b i l i t i e s o f MS)
( l e t enableEnc sn : b o o l = cap sn i n )
event begMS ( imsi hn sn , kc sn ) ;
( Send o u t c i p h e r mode command [ Msg 7 ] )
( o u t ( pubChannel , (CMC, enableEnc sn ) ) ; )
out ( pubChannel , (CMC, cap sn ) ) ;
out ( pubChannel , s e n c r y p t ( secretKc , kc sn ) ) ;
( i f enableEnc sn = f a l s e then )
out ( pubChannel , (MSG, s ) )
else
out ( pubChannel , (MSG, s e n c r y p t ( s , kc sn ) ) ) .
( F u n c t i o n s )
fun a3 ( nonce , key ) : resp .
fun a8 ( nonce , key ) : sessKey .
fun s e n c r y p t ( b i t s t r i n g , sessKey ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : sessKey ;
s d e c r y p t ( s e n c r y p t (m, k ) , k ) = m.
reduc e n c C a p a b i l i t y ( ) = t r u e ;
encCapability ( ) = false .
( The key t a b l e c o n s i s t s o f p a i r s
( i d e n t , key ) shared between t h e MS and t h e HN.
Table i s n o t a c c e s s i b l e by t h e a t t a c k e r )
t a b l e keys ( i d e n t , key ) .
free s : bitstring [ private ] .
query a t t a c k e r ( s ) .
( The s t a n d a r d secrecy q u e r i e s o f P r o V e r i f o n l y )
( d e a l w i t h t h e secrecy o f p r i v a t e f r e e names)
( s e c r e t K c i s s e c r e t i f and o n l y i f a l l kcs are s e c r e t )
free secretKc : b i t s t r i n g [ private ] .
query a t t a c k e r ( s e c r e t K c ) .
l e t processHN =
( Receive a u t h e n t i c a t i o n v e c t o r r e q u e s t [ Msg 3 ] )
l e t xres hn : resp = a3 ( rand hn , k i h n ) i n
l e t kc hn : sessKey = a8 ( rand hn , k i h n ) i n
( Send o u t a u t h e n t i c a t i o n v e c t o r [ Msg 4 ] )
out ( secureChannel , ( AV, imsi hn , rand hn , xres hn , kc hn ) ) ;
out ( pubChannel , s e n c r y p t ( secretKc , kc hn ) ) .
( A u t h e n t i c a t i o n q u e r i e s )
event begSN ( i d e n t , sessKey ) .
event endSN ( i d e n t , sessKey ) .
event begMS ( i d e n t , sessKey ) .
event endMS ( i d e n t , sessKey ) .
query x1 : i d e n t , x2 : sessKey ;
event ( endSN ( x1 , x2 ) )
event ( begSN ( x1 , x2 ) ) .
event ( endMS ( x1 , x2 ) )
event ( begMS ( x1 , x2 ) ) .
process
( ( ! processMS ) | processSN | processHN )
event d i sa b l e E nc .
(When t h e a t t a c k e r knows s ,
t h e event d i s a b l e E n c has been executed . )
query a t t a c k e r ( s )
S2. UMTS I IV
l e t processMS =
( The i d e n t and preshared key o f t h e MS )
new k i : key ;
( Send o u t cap ms t o SN[ Msg 1 ] )
( t y p e s )
type key .
type i d e n t .
type nonce .
23
type
type
type
type
type
type

i n ( pubChannel , (=SMC, enableEnc ms : bool ,
=cap ms , fresh ms : nonce ,
= f 9 ( ( enableEnc ms , cap ms , fresh ms ) , ik ms ) ) ) ;
i n ( pubChannel , (=MSG, msg : b i t s t r i n g , fresh msg ms : nonce ,
= f 9 ( ( msg , fresh msg ms ) , ik ms ) ) ) ;
out ( pubChannel , s e n c r y p t ( secretCk , ck ms ) ) ;
out ( pubChannel , s e n c r y p t I n t e g ( s e c r e t I k , ik ms ) ) ;
l e t msgcontent : b i t s t r i n g = s d e c r y p t ( msg , ck ms ) i n
0.
msgHdr .
resp .
cipherKey .
integKey .
mac .
msgMac .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const SMC: msgHdr .
const MSG: msgHdr .
fun f 1 ( key , nonce ) : mac .
fun f 2 ( key , nonce ) : resp .
fun f 3 ( key , nonce ) : cipherKey .
fun f 4 ( key , nonce ) : i n t e g K e y .
fun f 9 ( b i t s t r i n g , i n t e g K e y ) : msgMac .
fun s e n c r y p t ( b i t s t r i n g , cipherKey ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : cipherKey ;
l e t processSN =
mac sn : mac ) ) ;
event endSN ( imsi hn sn , ck sn , i k s n ) ;
new f r e s h s n : nonce ;
(SN decide whether t o e n c r y p t messages )
( base on t h e r e c e i v e d c a p a b i l i t i e s o f MS)
event begMS ( imsi hn sn , ck sn , ik sn , cap sn ) ;
out ( pubChannel , (SMC, cap sn , cap sn , fresh sn ,
f 9 ( ( cap sn , cap sn , f r e s h s n ) , i k s n ) ) ) ;
out ( pubChannel , s e n c r y p t ( secretCk , ck sn ) ) ;
out ( pubChannel , s e n c r y p t I n t e g ( s e c r e t I k , i k s n ) ) ;
new fresh msg sn : nonce ;
( Send o u t one message [ Msg 8 ] )
out ( pubChannel , (MSG, s , fresh msg sn ,
f 9 ( ( s , fresh msg sn ) , i k s n ) ) )
else
out ( pubChannel , (MSG, s e n c r y p t ( s , ck sn ) , fresh msg sn ,
f 9 ( ( s e n c r y p t ( s , ck sn ) , fresh msg sn ) , i k s n ) ) ) .
reduc
encCapability ( ) = true ;
( To t e s t secrecy o f t h e i n t e g r i t y key , )
( use them as s e s s i o n keys t o e n c r y p t a f r e e p r i v a t e name )
fun s e n c r y p t I n t e g ( b i t s t r i n g , i n t e g K e y ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : i n t e g K e y ;
s d e c r y p t I n t e g ( s e n c r y p t I n t e g (m, k ) , k ) = m.
( t h e t a b l e i d e n t / keys
The key t a b l e c o n s i s t s o f p a i r s
( i d e n t , key ) shared between MS and HN
( secretCk i s s e c r e t i f and o n l y i f a l l cks are s e c r e t )
f r e e secretCk : b i t s t r i n g [ p r i v a t e ] .
query a t t a c k e r ( secretCk ) .
( s e c r e t I k i s s e c r e t i f and o n l y i f
free secretIk : bitstring [ private ] .
query a t t a c k e r ( s e c r e t I k ) .
a l l i k s are s e c r e t )
event begSN ( i d e n t , cipherKey ,
event endSN ( i d e n t , cipherKey ,
event begMS ( i d e n t , cipherKey ,
event endMS ( i d e n t , cipherKey ,
integKey ) .
integKey ) .
integKey , bool ) .
integKey , bool ) .
event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
event d i s ab l e E n c .
l e t processHN =
out ( secureChannel , ( AV, imsi hn , rand hn , xres hn ,
ck hn , ik hn , mac hn ) ) ;
out ( pubChannel , s e n c r y p t ( secretCk , ck hn ) ) ;
l e t processMS =
new k i : key ;
(MS nond e t e r m i n i s t i c a l l y
choose t h e c a p a b i l i t y o f e n c r y p t i o n )
24
out ( pubChannel , s e n c r y p t I n t e g ( s e c r e t I k , i k h n ) ) .
f r e e payload : b i t s t r i n g [ p r i v a t e ] .
event d i s a b l e E n c .
(When t h e a t t a c k e r knows s , t h e event
d i s a b l e E n c has been executed . )
process
S3. LTE I V
free secret : bitstring [ private ] .
fun s e n c i n t n a s ( b i t s t r i n g , nasIntKey ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : nasIntKey ;
sdec in nas ( s e n c i n t n a s (m, k ) , k ) = m.
fun s e n c i n t a s ( b i t s t r i n g , a s I n t K e y ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : a s I n t K e y ;
sdec in as ( s e n c i n t a s (m, k ) , k ) = m.
fun senc up ( b i t s t r i n g , upEncKey ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : upEncKey ;
sdec up ( senc up (m, k ) , k ) = m.
( P u b l i c channel between t h e MS and t h e SN)

( Secure channel between t h e SN and t h e HN)
( Secure channel between MME and BS)
f r e e sChannelSnBts : channel [ p r i v a t e ] .
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type i n t e g K e y .
type mac .
type msgMac .
type asmeKey .
type nasEncKey .
type nasIntKey .
type enbKey .
type asEncKey .
type a s I n t K e y .
type upEncKey .
event begSN ( i d e n t , i d e n t , asmeKey ) .
event endSN ( i d e n t , i d e n t , asmeKey ) .
event begMS ( i d e n t , i d e n t , asmeKey , bool ) .
event endMS ( i d e n t , i d e n t , asmeKey , bool ) .
event begENB ( i d e n t , enbKey ) .
event endENB ( i d e n t , enbKey ) .
event begMS ENB( i d e n t , enbKey , bool ) .
event endMS ENB( i d e n t , enbKey , bool ) .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const NASSMC: msgHdr .
const NASSMComplete : msgHdr .
const ASSMC: msgHdr .
const ASSMComplete : msgHdr .
const MSG: msgHdr .
event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
query x1 : i d e n t , x2 : enbKey ;
event ( endENB ( x1 , x2 ) )
event ( begENB ( x1 , x2 ) ) .
event begENB ( imsi ms , kenb ms ) ;
f i n t e g a s ( as smcomplete msg , kasint ms ) ) ) ; ( [ Msg 1 1 ] )
= f i n t e g a s ( datamsg , kasint ms ) ) ) ; ( [ Msg 1 2 ] )
fun kdf asme ( cipherKey , integKey , i d e n t ) : asmeKey .
fun kdf nas enc ( asmeKey ) : nasEncKey .
fun k d f n a s i n t ( asmeKey ) : nasIntKey .
fun f i n t e g n a s ( b i t s t r i n g , nasIntKey ) : msgMac .
fun kdf enb ( asmeKey ) : enbKey .
fun kdf as enc ( enbKey ) : asEncKey .
fun k d f a s i n t ( enbKey ) : a s I n t K e y .
fun kdf up enc ( enbKey ) : upEncKey .
fun f i n t e g a s ( b i t s t r i n g , a s I n t K e y ) : msgMac .
fun sencrypt nas ( b i t s t r i n g , nasEncKey ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : nasEncKey ;
sdecrypt nas ( sencrypt nas (m, k ) , k ) = m.
l e t msgcontent : b i t s t r i n g = s d e c r y p t a s ( datamsg , kasenc ms )
in 0.
fun se nc ry pt as ( b i t s t r i n g , asEncKey ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : asEncKey ;
sd ec ry pt as ( s en c r y p t a s (m, k ) , k ) = m.
l e t processMS =
( Preshared key )
new k i : key ;
( Type C o n v e r t e r )
fun b o o l 2 b i t s t r i n g ( bool ) : b i t s t r i n g [ data , t y p e C o n v e r t e r ] .
reduc
(SMC command msg)
f r e e nas smcomplete msg : b i t s t r i n g .
f r e e as smcomplete msg : b i t s t r i n g .
25
(NAS key secrecy )
else
snid hn : i d e n t ) ) ;
xres hn , mac hn , kasme hn ) ) .
process
( ( ! processMS ) | processMME | processENB | processHN )
S4. GSM I IV, convert(3G AV 2G AV)

( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type mac .
type msgMac .
type sessKey .
l e t processENB =
i n ( sChannelSnBts , ( kasme enb : asmeKey ,
imsi enb : i d e n t , cap enb : bool ) ) ;
event endENB ( imsi enb , kenb enb ) ;
else
kasint enb ) ) ) .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const CMC: msgHdr .
const MSG: msgHdr .
l e t processMME =
i n ( secureChannel , (=AV, =imsi sn , =snid sn , rand sn : nonce ,
xres sn : resp , mac sn : mac , kasme sn : asmeKey ) ) ;
event begMS ( imsi sn , snid sn , kasme sn , cap sn ) ;
event endSN ( imsi sn , snid sn , kasme sn ) ;
out ( sChannelSnBts , ( kasme sn , imsi sn , cap sn ) )
else 0
else
event endSN ( imsi sn , snid sn , kasme sn ) ;
out ( sChannelSnBts , ( kasme sn , imsi sn , cap sn ) )
else 0
else 0 .
fun c2 ( resp ) : resp .
fun c3 ( cipherKey , i n t e g K e y ) : sessKey .
( To t e s t secrecy o f t h e c i p h e r key , )
fun s e n c r y p t C i p h e r ( b i t s t r i n g , cipherKey ) : b i t s t r i n g .
s d e c r y p t C i p h e r ( s e n c r y p t C i p h e r (m, k ) , k ) = m.
reduc
( s e c r e t K c i s s e c r e t i f and o n l y i f a l l kcs i s s e c r e t )
l e t processHN =
i n ( secureChannel , (=AV REQ, imsi hn : i d e n t ,
26
( secretCk i s s e c r e t i f and o n l y i f

( Send o u t c i p h e r mode command [ Message 7 ] )
out ( pubChannel , (MSG, s ) )
else
out ( pubChannel , (MSG, s e n c r y p t ( s , kc sn ) ) ) .
a l l cks are s e c r e t )
( I f KC and CK are s e c r e t , then IK i s s e c r e t )

query x1 : i d e n t
event ( begSN ( x1 ,
query x1 : i d e n t
event ( begMS ( x1 ,
( Process r e p r e s e n t i n g HN)
l e t processHN =
( Receive a u t h e n t i c a t i o n v e c t o r r e q u e s t [ Message 3 ] )
l e t xres hn u : resp = f 2 ( ki hn , rand hn ) i n
l e t xres hn g : resp = c2 ( xres hn u ) i n
l e t kc hn : sessKey = c3 ( ck hn , i k h n ) i n
( Send o u t a u t h e n t i c a t i o n v e c t o r [ Message 4 ] )
out ( secureChannel , ( AV, imsi hn , rand hn , xres hn g , kc hn ) ) ;
out ( pubChannel , s e n c r y p t C i p h e r ( secretCk , ck hn ) ) ;
out ( pubChannel , s e n c r y p t ( secretKc , kc hn ) ) .
, x2 : sessKey ; event ( endSN ( x1 , x2 ) )

x2 ) ) .
, x2 : sessKey ; event ( endMS ( x1 , x2 ) )
x2 ) ) .
d i sa b l e E nc has been executed . )
( Process r e s p r e s e n t i n g MS)
l e t processMS =
new k i : key ;
( Send o u t cap ms t o SN[ Message 1 ] )
( Send o u t permanent ID [ Message 2 ] )
( I n p u t c h a l l e n g e message from SN [ Message 5 ] )
l e t res ms u : resp = f 2 ( k i , rand ms ) i n
l e t res ms g : resp = c2 ( res ms u ) i n
l e t kc ms : sessKey = c3 ( ck ms , ik ms ) i n
( Send o u t response t o SN [ Message 6 ] )
out ( pubChannel , (RES, res ms g ) ) ;
( Receive GSM c i p h e r mode command [ Message 7 ] )
( Receive message from SN [ Message 8 ] )
out ( pubChannel , s e n c r y p t C i p h e r ( secretCk , ck ms ) ) ;
0.
process
S5. GSM IIII k UMTS IV, conv(Kc CK IK, VLR/SGSN)

( param verboseClauses = e x p l a i n e d . )
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type sessKey .
type cipherKey .
type mac .
type msgMac .
( Process r e s p r e s e n t i n g SN)
l e t processSN =
( Receive MS s c a p a b i l i t y [ Message 1 ] )
( Receive permanent ID [ Message 2 ] )
( Send o u t a u t h e n t i c a t i o n v e c t o r r e q u e s t [ Message 3 ] )
( Receive a u t h e n t i c a t i o n v e c t o r [ Message 4 ] )
( Send a u t h e n t i c a t i o n c h a l l e n g e t o MS [ Message 5 ] )
( Receive response [ Message 6 ] )
( Check whether r e c e i v e d response matches expected response )
( SN decide whether t o e n c r y p t messages )
27
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const SMC: msgHdr .
const MSG: msgHdr .
fun a3 ( nonce , key ) : resp .
fun a8 ( nonce , key ) : sessKey .
fun c4 ( sessKey ) : cipherKey .
fun c5 ( sessKey ) : i n t e g K e y .
reduc
l e t processSN =
( secretCk i s s e c r e t i f and o n l y i f a l l cks are s e c r e t )
( Convert Kc i n t o UMTS keys )
( s e c r e t I k i s s e c r e t i f and o n l y i f a l l i k s are s e c r e t )
l e t ck sn : cipherKey = c4 ( kc sn ) i n
free secretIk : bitstring [ private ] .
l e t i k s n : i n t e g K e y = c5 ( kc sn ) i n
query a t t a c k e r ( s e c r e t I k ) .
( I f IK and CK are s e c r e t , then KC i s s e c r e t . )
( Because CK and IK are computed from KC by p u b l i c f u n c t i o n s )
event begMS ( imsi hn sn , ck sn , ik sn , cap sn ) ;
( o u t ( pubChannel , (SMC, enableEnc sn , cap sn , fresh sn ,
f 9 ( ( enableEnc sn , cap sn , f r e s h s n ) , i k s n ) ) ) ; )
out ( pubChannel , (SMC, cap sn , cap sn , fresh sn ,
event begMS ( i d e n t , cipherKey , integKey , bool ) .
out ( pubChannel , s e n c r y p t ( secretCk , ck sn ) ) ;
event endMS ( i d e n t , cipherKey , integKey , bool ) .
out ( pubChannel , s e n c r y p t I n t e g ( s e c r e t I k , i k s n ) ) ;
new fresh msg sn : nonce ;
( Send o u t one message [ Msg 8 ] )
event ( endSN ( x1 , x2 ) )
event ( begSN ( x1 , x2 ) ) .
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
out ( pubChannel , (MSG, s , fresh msg sn ,
f 9 ( ( s , fresh msg sn ) , i k s n ) ) )
else
out ( pubChannel , (MSG, s e n c r y p t ( s , ck sn ) , fresh msg sn ,
f 9 ( ( s e n c r y p t ( s , ck sn ) , fresh msg sn ) , i k s n ) ) ) .
l e t processMS =
new k i : key ;
(MS nond e t e r m i n i s t i c a l l y choose t h e
c a p a b i l i t y o f e n c r y p t i o n )
l e t res ms : resp = a3 ( rand ms , k i ) i n
l e t kc ms : sessKey = a8 ( rand ms , k i ) i n
( Convert Kc i n t o UMTS keys )
l e t ck ms : cipherKey = c4 ( kc ms ) i n
l e t ik ms : i n t e g K e y = c5 ( kc ms ) i n
i n ( pubChannel , (=SMC, enableEnc ms : bool ,
=cap ms , fresh ms : nonce ,
= f 9 ( ( enableEnc ms , cap ms , fresh ms ) , ik ms ) ) ) ;
i n ( pubChannel , (=MSG, msg : b i t s t r i n g , fresh msg ms : nonce ,
= f 9 ( ( msg , fresh msg ms ) , ik ms ) ) ) ;
out ( pubChannel , s e n c r y p t ( secretCk , ck ms ) ) ;
out ( pubChannel , s e n c r y p t I n t e g ( s e c r e t I k , ik ms ) ) ;
l e t msgcontent : b i t s t r i n g = s d e c r y p t ( msg , ck ms ) i n
0.
l e t processHN =
l e t xres hn : resp = a3 ( rand hn , k i h n ) i n
l e t kc hn : sessKey = a8 ( rand hn , k i h n ) i n
out ( secureChannel , ( AV, imsi hn , rand hn , xres hn , kc hn ) ) .
process
S6. UMTS IIII k GSM IV, conv(CK IK Kc, VLR/SGSN)

( Secure channel between t h e MS and t h e HN )
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type sessKey .
type mac .
type msgMac .
const CAP: msgHdr .
28
const
const
const
const
const
const
const

l e t kc ms : sessKey = c3 ( ck ms , ik ms ) i n
out ( pubChannel , s e n c r y p t C i p h e r ( secretCk , ck ms ) ) ;
0.
ID : msgHdr .
AV REQ: msgHdr .
AV : msgHdr .
CHALLENGE: msgHdr .
RES: msgHdr .
CMC: msgHdr .
MSG: msgHdr .
fun c3 ( cipherKey , i n t e g K e y ) : sessKey .
( To t e s t secrecy o f t h e c i p h e r key , )
fun s e n c r y p t C i p h e r ( b i t s t r i n g , cipherKey ) : b i t s t r i n g .
s d e c r y p t C i p h e r ( s e n c r y p t C i p h e r (m, k ) , k ) = m.
l e t processSN =
xres sn : resp , ck sn : cipherKey , i k s n : integKey , mac sn : mac ) ) ;
event endSN ( imsi hn sn , ck sn , i k s n ) ;
l e t kc sn : sessKey = c3 ( ck sn , i k s n ) i n
out ( pubChannel , s e n c r y p t C i p h e r ( secretCk , ck sn ) ) ;
out ( pubChannel , (MSG, s ) ) ( [ Msg 8 ] )
else
out ( pubChannel , (MSG, s e n c r y p t ( s , kc sn ) ) ) . ( [ Msg 8 ] )
reduc
( s e c r e t K c i s s e c r e t i f and o n l y i f a l l kcs i s s e c r e t )
( secretCk i s s e c r e t i f and o n l y i f
a l l cks are s e c r e t )
( I f KC and CK are s e c r e t , then IK i s s e c r e t )

event begSN ( i d e n t , cipherKey , i n t e g K e y ) .
event endSN ( i d e n t , cipherKey , i n t e g K e y ) .
l e t processHN =
out ( secureChannel , ( AV, imsi hn , rand hn , xres hn ,
ck hn , ik hn , mac hn ) ) ;
out ( pubChannel , s e n c r y p t C i p h e r ( secretCk , ck hn ) ) .
event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 ) )
event ( begMS ( x1 , x2 ) ) .
l e t processMS =
( The i d e n t and preshared key o f t h e mobile s t a t i o n )
new k i : key ;
process
S7. LTE I k UMTS IIIII k LTE V, conv(CK IK KASME ,

MME)
29

event begMS ( i d e n t , enbKey , bool ) .
event endMS ( i d e n t , enbKey , bool ) .
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type asmeKey .
type enbKey .
type asEncKey .
type upEncKey .
type mac .
type msgMac .
event ( begSN ( x1 , x2 , x3 ) ) .
event ( begMS ( x1 , x2 , x3 ) ) .
l e t processMS =
( The i d e n t and preshared key o f t h e mobile s t a t i o n )
new k i : key ;
( Send o u t cap ms t o SN )
( Send o u t permanent ID )
( I n p u t c h a l l e n g e message from SN )
l e t kasme ms = kdf asme ( ck ms , ik ms ) i n
( Receive GSM c i p h e r mode command )
kasint ms ) ) ) ;
event endMS ( imsi ms , kenb ms , cap ms ) ;
out ( pubChannel , s e n c r y p t ( s e c r e t , ck ms ) ) ;
out ( pubChannel , s e n c r y p t I n t e g ( s e c r e t , ik ms ) ) ;
kasenc ms ) i n 0 .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const MSG: msgHdr .
sd ec ry pt as ( s en c r y p t a s (m, k ) , k ) = m.
l e t processSN =
( Receive MS s c a p a b i l i t y )
( Receive permanent ID )
( Send o u t a u t h e n t i c a t i o n v e c t o r r e q u e s t )
( Receive a u t h e n t i c a t i o n v e c t o r )
mac sn : mac ) ) ;
( Send a u t h e n t i c a t i o n c h a l l e n g e t o MS )
( Check whether r e c e i v e d response equal t o XRES)
l e t kasme sn = kdf asme ( ck sn , i k s n ) i n
l e t kenb sn : enbKey = kdf enb ( kasme sn ) i n
l e t kasenc sn : asEncKey = kdf as enc ( kenb sn ) i n
l e t k a s i n t s n : a s I n t K e y = k d f a s i n t ( kenb sn ) i n
l e t kupenc sn : upEncKey = kdf up enc ( kenb sn ) i n
event begMS ( imsi sn , kenb sn , cap sn ) ;
out ( pubChannel , (ASSMC, cap sn ,
f i n t e g a s ( b o o l 2 b i t s t r i n g ( cap sn ) , k a s i n t s n ) ) ) ;
= f i n t e g a s ( as smcomplete msg , k a s i n t s n ) ) ) ;
reduc
30
s d e c r y p t a s ( s e n c r y p t a s (m, k ) , k ) = m.
f i n t e g a s ( payload , k a s i n t s n ) ) )
else
kasenc sn ) , f i n t e g a s ( s e n c r y p t a s ( payload ,
kasenc sn ) , k a s i n t s n ) ) ) .
reduc
l e t processHN =
(SMC command msg)
process

S7+. LTE I k UMTS IIIII k LTE IVV, conv(CK IK KASME ,

MME)
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type mac .
type msgMac .
type asmeKey .
type nasEncKey .
type nasIntKey .
type enbKey .
type asEncKey .
type upEncKey .
event begMS ( i d e n t , asmeKey , bool ) .
event endMS ( i d e n t , asmeKey , bool ) .
event ( begSN ( x1 , x2 , x3 ) ) .
query x1 : i d e n t , x2 : asmeKey , x3 : bool ;
event ( begMS ( x1 , x2 , x3 ) ) .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const MSG: msgHdr .

s d e c r y p t a s ( datamsg , kasenc ms ) i n 0 .

l e t processMS =
31
( Preshared key )
new k i : key ;
= f 1 ( k i , rand ms ) ) ) ;
l e t kasme ms : asmeKey = kdf asme ( ck ms , ik ms ) i n
i n ( pubChannel , (=NASSMC, enableEnc nas ms : bool ,
=cap ms , = f i n t e g n a s ( ( enableEnc nas ms , cap ms ) ,
knasint ms ) ) ) ;
event endMS ( imsi ms , kasme ms , cap ms ) ;
(NAS key secrecy )
else
event begMS ( imsi sn , kasme sn , cap sn ) ;

pENB( kasme sn , imsi sn , cap sn )
else 0
else
pENB( kasme sn , imsi sn , cap sn )
else 0 .
process
( ( ! processMS ) | processMME )
S8. LTE I k UMTS IIIII k LTE IVV, conv(CK IK nonces

KASME , MME)
l e t pENB( kasme enb : asmeKey , imsi enb : i d e n t , cap enb : bool ) =
else
kasenc enb ) , f i n t e g a s ( s e n c r y p t a s ( payload ,
kasenc enb ) , k a s i n t e n b ) ) ) .
l e t processMME =
new rand sn : nonce ;
get keys (= imsi sn , k i s n ) i n
l e t mac sn : mac = f 1 ( ki sn , rand sn ) i n
l e t xres sn : resp = f 2 ( ki sn , rand sn ) i n
l e t ck sn : cipherKey = f 3 ( ki sn , rand sn ) i n
l e t i k s n : i n t e g K e y = f 4 ( ki sn , rand sn ) i n
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type mac .
type msgMac .
type asmeKey .
type nasEncKey .
type nasIntKey .
type enbKey .
type asEncKey .
type upEncKey .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const MSG: msgHdr .
const NONCE TAU: msgHdr .
fun kdf asme ( cipherKey , integKey , nonce , nonce ) : asmeKey .

l e t kasme sn : asmeKey = kdf asme ( ck sn , i k s n ) i n
fun s e n c r y p t a s ( b i t s t r i n g , asEncKey ) : b i t s t r i n g .
32

reduc

new nonce ms : nonce ;
out ( pubChannel , (NONCE TAU, nonce ms ) ) ;
i n ( pubChannel , (=CHALLENGE, rand ms : nonce , = f 1 ( k i , rand ms ) ) ) ;
=nonce ms , nonce mme ms : nonce , nas mac : msgMac ) ) ;
l e t kasme ms : asmeKey = kdf asme ( ck ms , ik ms ,
nonce ms , nonce mme ms ) i n
i f ( nas mac = f i n t e g n a s ( ( enableEnc nas ms , cap ms ,
nonce ms , nonce mme ms ) , knasint ms ) ) then
(NAS key secrecy )
else
(SMC command msg)
fun senc int nas ( b i t s t r i n g , nasIntKey ) : b i t s t r i n g .
sdec in nas ( sen c i n t n a s (m, k ) , k ) = m.
l e t processENB =
i n ( sChannelSnBts , ( kasme enb : asmeKey , imsi enb : i d e n t ,
cap enb : bool ) ) ;
else
kasint enb ) ) ) .
event begMS ( i d e n t , cipherKey , integKey , bool ) .
event endMS ( i d e n t , cipherKey , integKey , bool ) .
event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
kasint ms ) ) ) ;
sd ec ry p t a s ( datamsg , kasenc ms ) i n 0 .
l e t processMME =
i n ( pubChannel , (=NONCE TAU, nonce ms sn : nonce ) ) ;
xres sn : resp , ck sn : cipherKey ,
i k s n : integKey , mac sn : mac ) ) ;
new nonce mme : nonce ;
l e t kasme sn : asmeKey = kdf asme ( ck sn , ik sn ,
nonce ms sn , nonce mme ) i n
l e t processMS =
out ( pubChannel , (NASSMC, cap sn , cap sn , nonce ms sn ,
nonce mme , f i n t e g n a s ( ( cap sn , cap sn ,
nonce ms sn , nonce mme ) , k n a s i n t s n ) ) ) ;
( Preshared key )
new k i : key ;
33
reduc f o r a l l m: b i t s t r i n g , k : gsmKey ;
else 0
else
else 0
else 0 .
reduc
l e t processHN =
(SMC command msg)

process
( ( ! processMS ) | ( processMME ) | ( processENB ) | ( processHN ) )
S9. GSM I k LTE IIIII k GSM IV, conv(CK IK Kc, MME),


fun s e n c i n t a s ( b i t s t r i n g , i n t e g K e y ) : b i t s t r i n g .
event begSN ( i d e n t , cipherKey ,
event endSN ( i d e n t , cipherKey ,
event begMS AS ( i d e n t , gsmKey ,
event endMS AS ( i d e n t , gsmKey ,
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type gsmKey .
type mac .
type msgMac .
type asmeKey .
type nasEncKey .
type nasIntKey .
integKey ) .
integKey ) .
bool ) .
bool ) .
event ( begSN ( x1 , x2 , x3 ) ) .
l e t processMS =
( Preshared key )
new k i : key ;
s d e c r y p t a s ( datamsg , kc ms ) i n 0 .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const MSG: msgHdr .
const CMComplete : msgHdr .
fun f 9 ( b i t s t r i n g , i n t e g K e y ) : b i t s t r i n g .
fun c3 ( cipherKey , i n t e g K e y ) : gsmKey .
fun se nc ry pt as ( b i t s t r i n g , gsmKey ) : b i t s t r i n g .
34
fun
fun
fun
fun
fun
fun
fun
fun
fun
l e t processSN =
kasme sn : asmeKey ,
event begMS AS ( imsi sn , kc sn , cap sn ) ;
out ( pubChannel , (ASSMC, cap sn ) ) ;
else
out ( pubChannel , (MSG, s e n c r y p t a s ( payload , kc sn ) ) ) .
f 2 ( key , nonce ) : resp .

f 3 ( key , nonce ) : cipherKey .
f 4 ( key , nonce ) : i n t e g K e y .
f9 ( bitstring , integKey ) : b i t s t r i n g .
kdf asme ( cipherKey , integKey , i d e n t ) : asmeKey .
kdf nas enc ( asmeKey ) : nasEncKey .
k d f n a s i n t ( asmeKey ) : nasIntKey .
f i n t e g n a s ( b i t s t r i n g , nasIntKey ) : msgMac .
c3 ( cipherKey , i n t e g K e y ) : gsmKey .

fun s e n c r y p t a s ( b i t s t r i n g , gsmKey ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : gsmKey ;
reduc
l e t processHN =
i n ( secureChannel , (=AV REQ, imsi hn : i d e n t ,
snid hn : i d e n t ) ) ;
process
(SMC command msg)
S9+. GSM I k LTE IIIV k GSM IV, conv(CK IK Kc, MME),

event begMS AS ( i d e n t , gsmKey , bool ) .
event endMS AS ( i d e n t , gsmKey , bool ) .
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type gsmKey .
type mac .
type msgMac .
type asmeKey .
type nasEncKey .
type nasIntKey .
event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const MSG: msgHdr .
const CMComplete : msgHdr .

l e t pMSAS( kc ms : gsmKey , imsi ms : i d e n t , cap ms : bool ) =
l e t msgcontent : b i t s t r i n g = s d e c r y p t a s ( datamsg , kc ms )
in 0.
l e t processMS =
35
( Preshared key )
new k i : key ;
(NAS key secrecy )
pMSAS( kc ms , imsi ms , cap ms )
else
pMSAS( kc ms , imsi ms , cap ms ) .
l e t processBS =
i n ( sChannelSnBts , ( kc bs : gsmKey ,
event begMS AS ( imsi bs , kc bs , cap bs ) ;
out ( pubChannel , (ASSMC, cap bs ) ) ;
else
out ( pubChannel , (MSG, s e n c r y p t a s ( payload , kc bs ) ) ) .
l e t processSN =
i n ( secureChannel , (=AV, imsi hn sn : i d e n t ,
snid hn sn : i d e n t , rand sn : nonce ,
xres sn : resp , mac sn : mac , kasme sn : asmeKey ,
event begMS ( imsi hn sn , snid hn sn , kasme sn , cap sn ) ;
else 0
else
36

else 0
else 0 .
l e t processHN =
process
( ( ! processMS ) | processSN | processBS | processHN )
S10. UMTS I k LTE IIIII k UMTS IV, AV = 4G AV + CK +

IK
( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type mac .
type msgMac .
type asmeKey .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const MSG: msgHdr .
fun s e n c r y p t a s ( b i t s t r i n g , cipherKey ) : b i t s t r i n g .
reduc
(SMC command msg)
(When t h e a t t a c k e r knows s , )
( t h e event d i s a b le E n c has been executed . )

out ( pubChannel , (MSG, payload , f 9 ( payload , i k s n ) ) )
else
out ( pubChannel , (MSG, s e n c r y p t a s ( payload , ck sn ) ,
f 9 ( s e n c r y p t a s ( payload , ck sn ) , i k s n ) ) ) .

l e t processHN =
out ( secureChannel , ( AV, imsi hn , snid hn , rand hn , xres hn ,
mac hn , kasme hn , ck hn , i k h n ) ) .
( A u t h e n t i c a t i o n
event begSN ( i d e n t
event endSN ( i d e n t
event begMS ( i d e n t
event endMS ( i d e n t
q u e r i e s )
, cipherKey
, cipherKey
, cipherKey
, cipherKey
,
,
,
,
integKey ) .
integKey ) .
integKey , bool ) .
integKey , bool ) .
event ( begSN ( x1 , x2 , x3 ) ) .
process

event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
S10+. UMTS I k LTE IIIV k UMTS IV, AV = 4G AV + CK

+ IK
l e t processMS =
( Preshared key )
new k i : key ;
fresh ms : nonce , = f 9 ( ( cap ms , enableEnc as ms ,
fresh ms ) , ik ms ) ) ) ;
= f 9 ( datamsg , ik ms ) ) ) ;
l e t msgcontent : b i t s t r i n g = s d e c r y p t a s ( datamsg , ck ms )
in 0.
l e t processSN =
i n ( secureChannel , (=AV, =imsi sn , =snid sn ,
out ( pubChannel , (ASSMC, cap sn , cap sn , fresh sn ,
= f 9 ( as smcomplete msg , i k s n ) ) ) ;

( t y p e s )
type key .
type i d e n t .
type nonce .
type msgHdr .
type resp .
type cipherKey .
type mac .
type msgMac .
type asmeKey .
type nasEncKey .
type nasIntKey .
const CAP: msgHdr .
const ID : msgHdr .
const AV : msgHdr .
const RES: msgHdr .
const MSG: msgHdr .
fun s e n c r y p t a s ( b i t s t r i n g , cipherKey ) : b i t s t r i n g .
reduc
37

(NAS key secrecy )
pMSAS( ck ms , ik ms , imsi ms , cap ms )
else
knasenc ms ) , knasint ms ) ) ) ; ( [ Msg 8 ] )
pMSAS( ck ms , ik ms , imsi ms , cap ms ) .
(SMC command msg)
(When t h e a t t a c k e r knows s , )
( t h e event d i s a b le E n c has been executed . )
fun senc int nas ( b i t s t r i n g , nasIntKey ) : b i t s t r i n g .
sdec in nas ( senc in t n a s (m, k ) , k ) = m.
l e t processBS =
i n ( sChannelSnBts , ( ck bs : cipherKey , i k b s : integKey ,
event begMS AS ( imsi bs , ck bs , ik bs , cap bs ) ;
out ( pubChannel , (ASSMC, cap bs , cap bs ,
f 9 ( ( cap bs , cap bs ) , i k b s ) ) ) ;
= f 9 ( as smcomplete msg , i k b s ) ) ) ;
out ( pubChannel , (MSG, payload , f 9 ( payload , i k b s ) ) )
else
out ( pubChannel , (MSG, s e n c r y p t a s ( payload , ck bs ) ,
f 9 ( s e n c r y p t a s ( payload , ck bs ) , i k b s ) ) ) .
event begMS AS ( i d e n t , cipherKey , integKey , bool ) .
event endMS AS ( i d e n t , cipherKey , integKey , bool ) .
event ( begSN ( x1 , x2 , x3 ) ) .
event ( endMS ( x1 , x2 , x3 , x4 ) )
event ( begMS ( x1 , x2 , x3 , x4 ) ) .
event ( endMS AS ( x1 , x2 , x3 , x4 ) )
event ( begMS AS ( x1 , x2 , x3 , x4 ) ) .
l e t pMSAS( ck ms : cipherKey , ik ms : integKey ,
imsi ms : i d e n t , cap ms : bool ) =
= f 9 ( ( cap ms , enableEnc as ms ) , ik ms ) ) ) ;
event endMS AS ( imsi ms , ck ms , ik ms , cap ms ) ;
= f 9 ( datamsg , ik ms ) ) ) ;
sd ec ry p t a s ( datamsg , ck ms ) i n 0 .
l e t processMS =
( Preshared key )
new k i : key ;
38
l e t processSN =
event begMS ( imsi sn , snid hn sn , kasme sn , cap sn ) ;
out ( sChannelSnBts , ( ck sn , ik sn , imsi sn , cap sn ) )
else 0
else
out ( sChannelSnBts , ( ck sn , ik sn ,
else 0
else 0 .
l e t processHN =
process
( ( ! processMS ) | processSN | processBS | processHN )
39

Authentication 2G 3G 4G

Uploaded by

Authentication 2G 3G 4G

Uploaded by

Analysis of authentication and key establishment in

inter-generational mobile telephony

Chunyu Tang, David A. Naumann, and Susanne Wetzel

Mobile telephony has become an integral part of our daily

reference to the specifications. Of the 243 cases identified,

the specifications. Sect. VI describes our ProVerif models for

categorizing them in terms of secrecy, integrity, or authenticity

For reasons of space, we cannot present the complete

OVERVIEW OF GSM, UMTS, AND LTE SECURITY

The MS is the combination of the Mobile Equipment (ME)

The HN includes the Home Location Register (HLR) and

Lee et al. [25] analyze the anonymity property of the

Overview of GSM Security Mechanisms. Fig. 1 shows

Mobarhan et al. [26] evaluate the publically known attacks

Generate RAND & SQN

AK = f5(Ki, RAND), SQN = 1st(AUTN)AK

KNASenc = KDF (KASME, NAS-enc-alg, Alg-ID)

GSM message sequence diagram [29], [15]

Generate RAND & SQN

KNASenc = KDF (KASME, NAS-enc-alg, Alg-ID)

Decide algorithms ALG, Generate FRESH

KeNB = KDF (KASME)

LTE message sequence diagram [4]

messages are transmitted as in GSM I. In comparison to

UMTS message sequence diagram [3], [15]

that the attach request must have been executed previously.

Overview of LTE Security Mechanisms. The LTE AKA

GSM is prone to a false base station attack [14] as the

The LTE AKA can be triggered by the initial network

E XCERPT OF CLASSIFYING THE 243 INTEROPERATION

the table, we have adopted a color/font scheme: Rows in

E STABLISHING A NATIVE SECURITY CONTEXT IN

As mentioned previously, LTE introduces a comprehensive

For the ME, it is possible to use a SIM or a USIM with

In the following, we systematically enumerate all possible

For the BS, a 2G BS is only capable of handling a GSM

Enumeration of Interoperation Cases. As discussed in

For the VLR/SGSN/MME, a 2G VLR/SGSN can only

E XCERPT OF DETERMINING AKA SCENARIOS AND

Disallowed Interoperation Cases. We found that the

Using this approach, we categorize the 105 allowable and

An MME can control a 3G BS or a 2G BS.

Uncertain Interoperation Cases. The remaining 48 cases

Focusing on the allowable and uncertain interoperation

The blocks are as introduced in Figs. 1, 2, and 3. With notation

Table III shows an excerpt of determining and categorizing

R EASONS USED FOR DETERMINING AKA SCENARIOS

uses it with the CK, IK, and NONCEMS as input parameters

KASME = KDF(CK, IK)

S9. This scenario is characterized by a mixed SN including

S7. This scenario is characterized by a 4G ME, a 4G SN

XMAC = f1(Ki, RAND)

KNASenc = KDF (KASME), KNASint = KDF(KASME)

Part of the 4G AKA scenario (Fig. 3) annotated in accord with our

long version of the paper we consider integrity of data traffic,

M ODELING AND ANALYZING THE PURE PROTOCOLS

The ProVerif (PV) tool has been described well elsewhere,

In the LTE protocol, the MS already has the SN id before

7. RAND, AUTN, SNid

S10. This scenario is characterized by a 4G HN, a mixed

Fig. 6 shows the code of the MS process. The registration

challenge and successful use of the keys derived from KASME .

l e t pMSAS( kasme ms : asmeKey , imsi ms : i d e n t , cap ms : bool ) =

In Sect. III we annotate the protocol diagrams to mark

Of the 10 AKA scenarios, 5 of them are the same scenarios

MS process for LTE

The payload can be learned by the attacker when the MS is not

M ODELING AND ANALYZING INTEROPERATION IN

Scenario S7: LTE I k UMTS IIIII k [LTE IV] k LTE V,

As in pure 4G, plain secrecy of the message payload does not

Authentication of the MS to the MME is specified in

Generate RAND ,MAC = f1(Ki, RAND)

XMAC = f1(Ki, RAND)

KASME = KDF(CK, IK)

KeNB = KDF (KASME), KRRCenc = KDF (KeNB)

event endMS(imsi_ms, kenb_ms, cap_ms)