LTEInspector: A Systematic Approach for

Adversarial Testing of 4G LTE

Syed Rafiul Hussain Omar Chowdhury Shagufta Mehnaz Elisa Bertino

Abstract—In this paper, we investigate the security and pri- identified design weaknesses of the 3GPP (Third Generation
vacy of the three critical procedures of the 4G LTE protocol (i.e., Partnership Project) standard [3], [4] and unsafe practices by
attach, detach, and paging), and in the process, uncover potential the responsible stakeholders [5], [6], [7], [8], [9], [10], [11],
design flaws of the protocol and unsafe practices employed by the [12], [13], [14], [15], [16], [17]. Such work, however, has at
stakeholders. For exposing vulnerabilities, we propose a model- least one of the following limitations: (A) Analyses do not
based testing approach LTEInspector which lazily combines a
symbolic model checker and a cryptographic protocol verifier
use systematic methodologies for attack discovery [5], [6], [7],
in the symbolic attacker model. Using LTEInspector, we have [8], [9], [10], [11], [12], [13], [15]; (B) Analyses focus on
uncovered 10 new attacks along with 9 prior attacks, cate- prior generations of the protocols only, and hence some of the
gorized into three abstract classes (i.e., security, user privacy, findings do not directly apply to 4G LTE [5], [6], [7], [8], [9],
and disruption of service), in the three procedures of 4G LTE. [10], [11], [12], [16]; (C) Analyses do not explicitly reason
Notable among our findings is the authentication relay attack that about adversarial actions [17].
enables an adversary to spoof the location of a legitimate user
to the core network without possessing appropriate credentials. Problem and scope. The 4G LTE protocol can be viewed
To ensure that the exposed attacks pose real threats and are as an amalgamation of multiple critical procedures, such as
indeed realizable in practice, we have validated 8 of the 10 new attach, paging, detach, handover, and calls — to name a few.
attacks and their accompanying adversarial assumptions through Each of these procedures is complex and requires an in-depth
experimentation in a real testbed. security and privacy analysis of its own. Among the different
procedures, attach, paging, and detach are critical for the
I. I NTRODUCTION correct and reliable functionality of the other procedures. For
instance, without a correct and secure attach procedure (i.e.,
The adoption of Fourth generation Long Term Eval-
the initial secure connection setup), the security bootstrapping
uation (4G LTE)—the de facto standard for cellular
process is likely to be vulnerable; this may have serious
telecommunication—has seen a stable growth in recent years,
consequences, such as man-in-the-middle attacks, spurious
replacing prior generations due to its promise of improved
mobile billing, or even life threatening risks. This paper thus
assurances (e.g., higher bandwidth, reliable connectivity, en-
addresses the following central research question: is it possible
hanced security). Cellular networks which are part of a nation’s
to develop a systematic approach for scrutinizing the attach,
critical infrastructure not only influence our society as a whole
detach, and paging procedures to uncover vulnerabilities that
(e.g., business, public-safety message dissemination) but also
can be shown to be realizable in practice by an adversary?
can impact us at a more personal level by enabling applica-
tions that often improve our quality of life (e.g., navigation). Challenges. Any testing approach analyzing the security and
Because of their ubiquitous presence and use for critical appli- privacy of the 4G LTE protocol needs to address the following
cations, cellular networks are, however, attractive attack targets challenges: (a) Specification: The cellular protocol lacks a for-
for malicious parties. Resourceful adversaries (e.g., nation- mal specification, and the standard [3], [4] often suffers from
states, foreign intelligence agencies, terrorists) can wreak ambiguity and under-specification. (b) Protocol Complexity:
havoc by exploiting vulnerabilities of the cellular network The cellular protocol—comprising of multiple (cryptographic)
ecosystem (e.g., surveillance [1], cyberwarfare [2]). It is hence sub-protocols—is stateful in nature [17]. Also, analyses will
pivotal to investigate the existing design and deployments of likely experience scalability challenges due to the presence of
cellular networks for detecting potential vulnerabilities. multiple types of protocol participants, and messages contain-
ing data with a large domain. (c) Closed system: A majority of
There is already a substantial work that has analyzed the the deployed cellular systems are proprietary and closed sys-
security and privacy of telecommunication systems, and also tems which require any testing approach to be black-box and
system-agnostic. (d) Legal barrier: Regulatory requirements
[18] prohibit transmission in the licensed spectrum making
dynamic network testing and attack validation challenging.
Network and Distributed Systems Security (NDSS) Symposium 2018
18-21 February 2018, San Diego, CA, USA Approach. For analyzing the critical procedures of 4G LTE,
ISBN 1-1891562-49-5 in this paper, we take a first step by proposing LTEInspector
http://dx.doi.org/10.14722/ndss.2018.23313 which employs a property-driven adversarial model-based test-
www.ndss-symposium.org
ing philosophy. LTEInspector considers the standard symbolic
adversary model (alternatively known as the Dolev-Yao model
[19]) for its analysis. LTEInspector takes the relevant 4G LTE report π to be a feasible vulnerability. If, however, there exists
abstract model M and a desired property ϕ, and tries to find a one adversary action in π which is not feasible, we refine the
violation of ϕ in M. The set of properties that LTEInspector property ϕabs to rule out traces in which the adversary takes
aims to check include authenticity (e.g., disallowing imperson- that action. The analysis is then run again with the refined
ation), availability (e.g., preventing service denial), integrity property. For further confidence, we validate π by concretely
(e.g., restricting unauthorized billing), and secrecy of user’s executing it in a testbed.
sensitive information (e.g., preventing activity profiling).
Finally, we show the application of a technique we call
As a prerequisite of LTEInspector’s analysis, we first attack chaining in which seemingly low-impact attacks are
construct the 4G LTE ecosystem model by consulting the stitched together to yield a damaging high-impact attack. We
standard [3], [4]. Our model M (publicly available in https: show its successful application by chaining together attacks,
//github.com/relentless-warrior/LTEInspector) captures the ab- exposed using LTEInspector, to allow an adversary to carry
stract functionality (ignoring low-level implementation details) out an authentication relay attack in the 4G LTE network.
of the 4G LTE ecosystem—only relevant to the analysis of the Findings. Notable among our findings is the authentication
three procedures—as synchronous communicating finite state relay attack which enables an adversary to connect to the core
machines (FSM). Each FSM captures the stateful functionality networks—without possessing any legitimate credentials—
of a protocol participant’s (i.e, user’s cellular device and the while impersonating a victim cellular device. Through this
core network) at the Non-Access Stratum (NAS) protocol attack the adversary can poison the location of the victim
layer [3], [4]. The two FSMs communicate with each other device in the core networks, thus allowing setting up a false
through public (adversary-controlled) communication channels alibi or planting fake evidence during a criminal investigation.
by sending each other NAS layer messages.
Other notable attacks reported in this paper enable an
Our analysis is an instance of the parameterized system adversary to obtain user’s coarse-grained location information
verification problem (i.e., parameterized by the number of and also mount denial of service (DoS) attacks. In particular,
protocol participants) which is generally undecidable [20]; using LTEInspector, we obtained the intuition of an attack
achieving both soundness and completeness is thus impos- which enables an adversary to possibly hijack a cellular
sible. Consequently, we follow the conventional method of device’s paging channel with which it can not only stop
aiming for soundness instead of completeness, that is, if our notifications (e.g., call, SMS) to reach the device but also can
approach reports a violation, it is indeed a violation; we cannot, inject fabricated messages resulting in multiple implications
however, detect all violations. Also, checking compliance including energy depletion and activity profiling.
of the protocol model against desired security and privacy
properties often requires simultaneously reasoning about: (➊) Contributions. In summary, the paper makes the following
temporal ordering of different events/actions (i.e., trace prop- technical contributions:
erties such as response properties [21]), (➋) cryptographically- (1) We propose LTEInspector—a systematic model-based
protected messages and constructs (e.g., encryption, hashing), adversarial testing approach—that leverages the combined
and (➌) other rich constraints (e.g., linear integer arithmetic power of a symbolic model checker and a protocol verifier
constraints). General purpose model checkers [22], [23] have for analyzing three critical procedures (i.e., attach, detach,
shown promise in successfully reasoning about properties and paging) of the 4G LTE network. The general principle
concerning ➊ and ➌. Cryptographic protocol verifiers [24], employed by LTEInspector is to be tool-agnostic, that is, it can
[25], [26], [27], [28], [29], although proficient in verifying be instantiated through any generic symbolic model checker
cryptography related properties, for tractability reasons only and cryptographic protocol verifier.
provide primitive support at best for properties concerning ➊ (2) We show the effectiveness of our approach in finding
and ➌. This naturally leads us to the question: is it possible new vulnerabilities as well as 9 prior attacks. Our approach
to get the best of both these techniques? has contributed to exposing 10 new attacks.
(3) We show that the majority of our new attacks (i.e., 8 out
To this end, LTEInspector lazily (or, on an on-demand of 10) are realizable in practice through experimentation in a
basis) combines the reasoning powers of a symbolic model low cost (i.e., $3, 900), real test-bed while adhering to ethical,
checker and a cryptographic protocol verifier. To the best of legal, and moral practices.
our knowledge, in the context of 4G LTE, the use of symbolic
model checking and a cryptographic protocol verifier to reason
II. LTE P RELIMINARIES
about rich temporal trace properties is novel. In this approach,
we first abstract away all cryptography-related constructs from In this section, we provide a brief primer of 4G LTE. For
the model M and the desired property ϕ and only reason the ease of exposition, we simplify the network architecture
about aspects ➊ and ➌ of the ϕ (denoted by ϕabs ). For any substantially (see Figure 1) and only focus on the aspects
violation of ϕabs in M, the symbolic model checker would relevant to the attach, detach, and paging procedures.
yield a counterexample π demonstrating the violation. Now, A. LTE Network Architecture
π may include adversary actions which may not be realizable
The LTE network is broadly comprised of the following
due to cryptographic assumption violations (e.g., constructing a
three components: the cellular device (also known as user
valid ciphertext of a message without possessing the encryption
equipment or UE), the radio access network (or, (E-UTRAN),
key). To rule out such cases, for each adversary action in π, we
and the core network or Evolved Packet Core (EPC).
query a cryptographic protocol verifier to check the action’s
feasibility with accordance to the cryptographic assumptions. UE: UE is the cellular device equipped with a universal
In case all adversary actions in π turn out to be feasible, we can subscriber identity module known as SIM card. The SIM card

2
procedures—without fine-grained implementation details—as the case MC finds an execution π of Madv which violates ϕ,
two synchronous communicating finite state machines (FSM) MC outputs π as an evidence of the violation (also, known as
(denoted by Mvanilla ). The two FSMs in Mvanilla (one for the the counterexample). π includes the adversary actions which
UE and another for the MME) communicate with each other were used to violate ϕ, and alternatively, can be viewed as
by sending messages through public communication channel. the attack strategy. The Adv−c used when model checking
We model the communication channel between the two FSMs Madv does not have the necessary cryptographic proficiency
MUE and MMME with two uni-directional channels; one of Adv+c (i.e., A-3), and hence π can violate cryptographic
from MUE to MMME and another from MMME to MUE . assumptions, making it unrealizable in practice. We rule out
The choice of two unidirectional channels instead of a single such spurious πs through the following process.
bidirectional channel is not only for modeling convenience
Validating counterexamples with CPV. For a given coun-
but also for effortlessly modeling weaker adversaries than
terexample π, we check each sub-step of π that requires
Adv+c during adversary model instrumentation (e.g., only one
manipulating some crytographically-protected message type.
direction of the public channel to be adversary controlled).
We model each small sub-step in a CPV, denoted as Mcrypto .
To keep the analysis tractable, in Mvanilla , we do not We then pose a query to CPV that will be violated in Mcrypto
model message data with arbitrarily large domains. For in- only if the Adv+c has the specific capability that π requires.
stance, the attach request message can possibly contain IMSI For few message types, such as, paging, we know from the
as a data; in our model, we do not capture the IMSI 3GPP standard that there are no confidentiality and integrity
and just model attach request as a possible message type. protections; for those message types we do not invoke the
We, however, model message data-dependent conditions as CPV.
environment-controlled (or, in short, environmental) Boolean
Testbed experimentation. Once both MC and CPV ad-
variables. For instance, for each message that can have in-
judicate a given π to be feasible, we try to realize this
tegrity protection, we capture its integrity verification with a
attack in a testbed. This is essential because π may not be
unique Boolean variable mac failure whose value is nonde-
realizable in practice due to possible technical safeguards. Any
terministically set by the environment during model checking.
π validated in the testbed experiment can thus be considered
Mvanilla can capture an unbounded number of sequential ses-
a vulnerability. We built a testbed using low-cost software
sions. It, however, can neither capture an unbounded number
defined radios and open-source LTE software stack having a
of parallel sessions nor an unbounded number of protocol
price tag of around $3, 900 which we would argue is within
participants; the latter is shown to be undecidable [34].
the reach of a motivated adversary.
Adversarial model instrumentor. The adversarial model in-
strumentor takes Mvanilla and instruments it to incorporate C. Example Demonstrating LTEInspector’s Effectiveness
the presence of an adversary to obtain a new model Madv . We now show the effectiveness of LTEInspector’s vul-
We model a cryptography-agnostic adversary Adv−c which nerability detection through a concrete example. For ease of
possesses the same capabilities of Adv+c except for its crypto- exposition, we rely on a simplified and partial model of the
graphic proficiency (i.e., A-3). We model the Adv−c capabili- LTE ecosystem shown in Figure 4 for this example.
ties for each unidirectional public channel ch in the following
In the example, the UE FSM (the top FSM) has 3 states
manner. Capability A-1 is modeled as ch’s property, that is, ch
and 9 transitions whereas the MME FSM (the bottom FSM)
nondeterministically drops any message msg passing through
has 3 states and 6 transitions. Transition labels are of the
it (represented as a no operation) or replaces it with another
form “condition/actions” in which condition is a proposi-
plausible message including the current message msg.
tional logic formula specifying the condition under which the
Modeling capability A-2 for ch requires considering an transition will be triggered whereas the actions component
adversarial FSM which nondeterministically injects one of refers to a sequence of actions that will be performed (in their
the possible messages including no operation. We call such appearance order) by the FSM after the transition is taken.
adversary FSMs the injection adversaries. In the case both Although the actions component can be empty (denoted with
the legitimate protocol participant and the adversary simulta- –), the condition component cannot be empty. We represent
neously push messages msgv and msgadv , respectively, into the states with barebone arrows (i.e., arrows with no condition
ch, the message received on the other side is decided by and action) as the initial states of the FSMs. We use ➊,
the value of an environmental Boolean variable adv turn; ➋,. . . to denote the UE transitions whereas we use ➀, ➁,. . . ,
the value of adv turn is nondeterministically chosen by the to denote the MME transitions. The FSMs have the following
environment. Precisely, the other side of ch will receive environmental variables: mobile restart (signifying UE reboot-
msgadv only if the value of adv turn is set to be true by the ing); mac failure (improper MAC for auth request message);
environment. The nondeterministic behavior of the channels xres matches sres (correct authentication response message
and the injection adversaries are crucial for reasoning about for a given authentication request message). Both the FSMs
all possible adversary strategies. Our instrumentation makes start with their respective sequence numbers to be 0.
it effortless to customize the capabilities of the adversary, for
The response property we want to verify is the following:
instance, independently making each ch to have adversarial
“It is always the case that whenever the UE FSM is in the
interference.
wait for auth request state, it will eventually move to the
General-purpose Model Checker (MC). MC takes as input state where the UE authenticates the MME” (denoted by ϕ1 ).
Madv and a desired abstract property ϕ, and checks to see The property is desirable as its violation signifies a denial-
whether all possible executions of Madv (considering all of-service attack in which the UE cannot proceed to the next
possible values of the environmental variables) satisfy ϕ. In stage of the attach procedure after initiating it.

5
 +-*.'(&/-&)* 0
5678'9:;:<7 3 =:75<8'9:>6:?7 , @ +-*.'(&/-&)* 0 (1mac_failure 0 (UE_sqn 2 xsqn
(mac_failure 3 1(UE_sqn 2 xsqn 2 2 UE_sqn + range)) , UE_sqn =
ID MC property details 6 xsqn + 1, auth_response
UE_sqn + range)) ,4auth_failure
ϕ1 It is always the case that whenever the UE FSM is 2 7
in the wait for auth request state, it will eventu- !"#$%&'(&)*+(* , attach_request
ally move to the state where the UE authenticates 8
the MME. +-*.'(&/-&)* 0
(1mac_failure 0 (UE_sqn 2
ϕ2 Refinement over ϕ1 : Once UE FSM moves to the !"#$%&'(&)*+(* UE UE
UE , attach_request
xsqn 2 UE_sqn + range))
wait for &auth request state, the environment 1 waits for 5 authenticates
will never set the value of mobile restart to be disconnected
auth_request , UE_sqn = xsqn + 1, MME
true. 5678'9:;:<7 3 auth_response
ϕ3 Refinement over ϕ2 : mac failure is never set to 4 =:75<8'9:>6:?7 , @ 9
true by the environment. 3 +-*.'(&/-&)* 0
!"#$%&'(&)*+(* (mac_failure 3 1(UE_sqn 2 xsqn 2 UE_sqn +
ϕ4 Refinement over ϕ3 : UE FSM never receives the , attach_request range)) ,4auth_failure
detach req message. d
ϕ5 Refinement over ϕ4 : UE FSM never receives the Attacker-controlled UE to MME channel d Attacker-controlled MME to UE channel
auth reject message.
auth_failure , @
2 5
Table I: MC properties used in attach_request , auth_response 0
xres_matches_sres ,
the motivating example. MME_sqn = MME_sqn + 1,
MME C&B-($*D'!"E&'B"!!+FE MME
MME +-*.'(&/-&)*
1 waits for authenticates
ID CPV property details disconnected
auth_response 0 auth_response attach_request , MME_sqn UE
Ψ1 Every attach request message received by 1xres_matches_sres , = MME_sqn + 1,
+-*.'(&/-&)*
the MME should be preceded by a unique 3 +-*.'(&A&B*
6
attach request message sent by the UE. 4
attach_request , MME_sqn
= MME_sqn + 1, +-*.'(&/-&)*
Table II: CPV Properties used in
the motivating example. Figure 4: A simplified LTE ecosystem model.

When ϕ1 is checked against the given Madv , it gives the Attack 2: We then check Madv against ϕ4 , and it yields an-
trivial counterexample π in which after the UE FSM moves other similar π in which the UE FSM receives an auth reject
to the wait for auth request state, it continuously observes message (triggering transition ➍); this moves the FSM to the
the value of the environmental variable mobile restart to be disconnected state. Again, one needs to determine whether the
true (triggering transition ➌)—signifying the repeated restart adversary can fabricate an auth reject message. A close in-
of the UE—which even though plausible, is not interesting spection of the standard revealed that the auth reject message
as the Adv+c has no control over UE reboot. One possible is never integrity protected and our experimentation validated
way of removing this π is to refine ϕ1 to add the restriction it. In a similar way, we refine ϕ4 to exclude any auth reject
that once UE FSM moves to the wait for auth request state, message and obtain our final property ϕ5 .
the environment will never set the value of mobile restart
to be true. When this refined property (denoted by ϕ2 —see Attack 3: Finally, checking Madv against ϕ5 with MC results
Table I) is checked, the MC yields a π in which all the in a very interesting π in which the adversary sends the
auth request messages received by the UE fails the MAC range (a UE-specific constant non-negative integer) number
verification (triggering transition ➋) because the MC assigns of fake attach request messages to the MME, before the UE
the value of the mac failure to be continuously true. We then reboots and sends the attach request. After receiving each
refine ϕ2 further to ensure that mac failure is never set to true attach request message, the MME increases its own sequence
by the MC and obtain the property ϕ3 . number (according to transitions ➀ and ➃) and uses the value
of the sequence number to provide replay protection to the
Attack 1: Checking Madv against ϕ3 using MC yields auth request message which it sends to the UE. As the UE
another π in which after UE FSM moves to the wait for is still in the disconnected state (with its sequence number 0,
auth request state, it receives a network initiated detach i.e., U E sqn = 0) and there is no transition that is triggered
request (detach req)–injected by the adversary—triggering by the auth request when the UE is in the disconnected
transition ➍ which moves it to the disconnected state and due state (see Figure 4), these auth request messages are ignored.
to avoiding reboot after transitioning to wait for auth request Then the UE observes a mobile restart (triggering transition
state (in ϕ2 ), stops the UE FSM to get out of the disconnected ➊) and sends an attach request to the MME which the
state. This is a legitimate attack and we would like to know adversary allows to reach the MME. After the MME receives
whether it is possible for the attacker to forge a network initi- it (transitions ➀, ➃, and ➅), the MME as usual responds
ated detach request. A close inspection of the standard reveals with an auth request with the sequence number range + 1.
that once the security context has been established between The adversary also allows the auth request from the MME
the UE and the MME, the network initiated detach request to reach the UE. Upon receiving the message, the UE checks
should be integrity protected only. Our experiment with the for mac failure (which cannot be true as we excluded it while
UE, however, revealed that the UE does not actually check refining ϕ2 to obtain ϕ3 ) and checks whether the received
the validity of the MAC for detach req even in the case the sequence number from MME (denoted with xsqn) satisfies
security context has been established. This means such an the following: U E sqn ≤ xsqn ≤ U E sqn + range; this
attack is plausible and we have verified it in our testbed. We condition will fail as xsqn = range + 1 resulting in the
then refine ϕ3 further to exclude this π and ensure that the UE UE not being able to attach with the MME. To ensure that
FSM never receives the network initiated detach request; as a validity of the π, one has to verify whether the Adv−c can
result, we obtain the refined property ϕ4 . inject a fake attach request message; we use the CPV to

6
validate it. We pose an injective-correspondence [32] query, Such a threat is very practical and has been validated through
Ψ1 (shown in Table II) which asserts that every attach request experimentation in our testbed (see Section V-A1).
message received by the MME should be preceded by a unique
attach request message sent by the UE. The CPV produced Detection. We exposed this attack by first model checking
an attack in which the adversary injected an attach request; Madv with respect to a refinement ϕ5 of the following
validating the desired sub-step of π. We have also observed the property: “It is always the case that whenever the UE FSM
feasibility of this attack in our testbed. We call this attack the is in the wait for auth request state, it will eventually move
authentication synchronization failure attack; this attack is to the state where the UE authenticates the MME” (see Table
also applicable against a recent proposal for defeating IMSI I for details). We observed a violation of ϕ5 in Madv where
catchers [16]. One of the challenges of detecting such an the Adv−c fabricates attach request messages and sends them
attack through CPVs is to precisely capture the sanity check to the MME. To validate the Adv−c ’s capability of forging an
corresponding to the sequence number. It is not immediately attach request message, we leverage ProVerif which showed
clear to us how one would directly capture such a requirement that forging attach request messages are possible; validating
in the CPV in a fine-grained fashion. The MC, however, can the feasibility of the attack.
efficiently reason about such requirement precisely. This shows Malicious Victim
the effectiveness of combining a MC with a CPV for attack MME HSS
UE UE
discovery. 5ÌÊÇ :
attach_request (+/5+) +/5+ JEs
attach_request (+/5+)
This example demonstrates the analysis power of +/5+ JEt
attach_request (+/5+)
LTEInspector’s approach, that is, based on the violation of +/5+ JEI
attach_request (+/5+) +/5+
a single desired property (and, its refinements) LTEInspector 4#0&á #760á :4'5á %-á
JEIEs
authentication_request
was able to find three different attacks which have been shown for :530 L J E I E s
+-á :530 L J E I E s;
to be realizable in practice. As we will demonstrate later, }z O „}z - }z E ˜‡”‹
Attacks 1 or 2 can be stitched with a relay attack to yield authentication_failure
(OUJ? B=EHQNA)
the authentication relay attack.
Figure 5: Authentication synchronization failure attack.
D. Implementation
Attack description: The steps of this attack are shown in
We now discuss some additional details of LTEInspector. Figure 5. It is very similar to the description of Attack 3 in
MC and CPV: We instantiate LTEInspector’s MC compo- Section III-C with one caveat. It is just not sufficient to send the
nent with NuSMV [22] and use ProVerif [24] for CPV. same attach request message m times (where m > range).
The malicious UE needs to send different security capabilities
Model. We manually construct the abstract LTE model by (by selecting different encryption and integrity protection
consulting the 3GPP standard [3], [4]. Our model has a total algorithms) in successive attach request messages. This is
of 13 states and 107 transitions. Our current model and the crucial as the HSS only processes an attach request message
respective properties are publicly available at https://github. only if one or more of the information elements in the current
com/relentless-warrior/LTEInspector. attach request message differs from the already received one.
Properties. Our properties were extracted from the 3GPP In which case, in accordance to subclause 5.5.1.2 of 3GPP
standard [3], [4]. We have tested Madv against 14 properties standard [35], the previously initiated attach procedure is
in total in which 7 properties were analyzed with NuSMV aborted and the new attach request message is processed
whereas 7 properties were analyzed with ProVerif. Note that, (including, the increment of the sequence number).
we do not claim our list of properties to be exhaustive. Re-synchronization: When the sequence number sanity check
fails on the UE side, it sends an auth failure message
IV. LTEI NSPECTOR F INDINGS (cause: sync. failure) to the EPC with AU T S parameter
In this section, we highlight the findings of LTEInspector. containing the UE’s current sequence number resulting in the
For readers’ convenience, we have provided a summary of the EPC to re-synchronize its sequence number. Even after re-
attacks and their implications in Table III. synchronization, the adversary can continue repeating step 1
to make the UE and the HSS sequence numbers to go out-of-
A. Attacks Against Attach Procedure sync again; preventing the UE from connecting to the EPC.
We now present our findings on the attach procedure. Implication: The major implication of this attack is the service
A-1 Authentication Synchronization Failure Attack: This disruption suffered by the victim UE.
attack exploits the UE’s sequence number sanity check to
A-2 Traceability Attack: This attack exploits the re-
disrupt its attach procedure. Precisely, the adversary interacts
sponses of security mode command messages to track a
with the HSS through the MME to ensure that the sequence
particular victim UE. Typically during the attach procedure, the
numbers of the UE and the HSS are out-of-sync. As a result,
MME uses the security mode command message to choose
the authentication challenge received through the legitimate
one of the UE-supported cipher suites to use for communi-
auth request message fails the UE’s sanity check and conse-
cation. When the UE receives this message, it is expected to
quently is discarded by the UE.
respond with a security mode complete message when the
Adversary assumptions. For successfully carrying out this received message satisfies the MAC validation. In case of
attack, the adversary is required to set up a malicious UE MAC failure, the UE responds with a security mode reject
and also is required to the know the victim UE’s IMSI. message. The MME can also send a security mode command

7
 Affected Assumption Standard/ New Vali- Setup
ID Attack name proce- Adversary assumptions validation Stakeholder attack? Detection process Notable implications dated cost
dure slip-up
Authentication Known IMSI, malicious IMSI [13], Denial-of-attach or Denial-of- $2600 (2
A-1 sync. failure Attach UE Section V-A1
3GPP Yes LTEInspector
services. USRPs)
Valid security mode Operational
Inspired LTEInspector Coarse-grained location infor- $2600 (2
A-2 Traceability Attach command, malicious Section V-A1 networks,
eNodeB mobile devices by [10] mation leakage. USRPs)
Numb using $1300 (1
A-3 auth reject Attach Malicious eNodeB Section V-A1 3GPP Yes LTEInspector Denial of all cellular services.
USRP)
3GPP, Reading incoming/outgoing
Authentication Known IMSI, malicious IMSI [13]; operational LTEInspector, messages of victim, stealthy $3900 (3
A-4 relay Attach Yes
eNodeB Section V-A1 networks attack chaining denial of all/selective services, USRPs)
location history poisoning.
Intuition from
Paging chan- Known IMSI, malicious IMSI [13], Stealthy denial of incoming $1300 (1
P-1 nel hijacking Paging eNodeB Section V-A1 3GPP Yes LTEInspector, services. USRP)
domain Knowledge
Stealthy Known IMSI, malicious IMSI [13], Consequence of P-1, Detaching a victim from the $1300 (1
P-2 kicking-off Paging eNodeB Section V-A1 3GPP Yes domain knowledge network surreptitiously. USRP)
Life threatening impact against
Consequence of P-1, mass people, e.g., artificial $1300 (1
P-3 Panic Paging Malicious eNodeB Section V-A1 3GPP Yes domain knowledge USRP)
chaos for terrorist activity.
Energy deple- Paging Known IMSI, GUTI, IMSI
GUTI
[13];
[8], 3GPP
Inspired Consequence of P-1,
by [36], Battery depletion. $1300 (1
P-4 tion malicious eNodeB domain knowledge USRP)
Section V-A1 [37]
3GPP,
Known IMSI or old Section V-A1 enhanced Coarse-grained location infor- $1300 (1
P-5 Linkability Paging
pseudo-IMSI
Yes ProVerif only
mation leakage USRP)
AKA [16]
Detach/ Malicious eNodeB, IMSI [13]; Inspired LTEInspector, Denial of services/Downgrade $1300 (1
D-1 Downgrade Detach known IMSI (for 3GPP attack chaining (for
Section V-A1 by [13] to 2G/3G. USRP)
targeted version) targeted version)
Table III: Summary of our findings ( =validated, =partially validated, =not validated) of the reported attacks.
D. Attack Chaining will forward the c to the eNodeBadv which the eNodeBadv
will send to the UEvic . After the UEvic receives c, unaware
We now demonstrate the application of the attack chaining that the eNodeBadv sent it, it will solve the challenge c to
technique through the authentication relay attack. generate the correct response r. The UEvic will then send r to
A-4 Authentication Relay Attack: In this attack, one the eNodeBadv which it will forward to the UEadv . The UEadv
of our exposed attacks (e.g., paging with IMSI) is stitched then will use r to respond to the MME challenge. Using the
with a relay attack with which an adversary impersonates the same principle, the UEadv will finish the rest of the steps of
victim UE to connect to the EPC without possessing proper the attach procedure.
credentials, and in the process, spoof the victim UE’s location Discussion. Unlike a typical man-in-the-middle attack, the
in the core networks. adversary in this attack can neither decrypt the encrypted traffic
Adversary assumptions. For this attack, the adversary is between the victim UE and the core networks, nor can inject
required to setup a malicious eNodeB (eNodeBadv ) and a valid encrypted traffic unless the service provider blatantly
malicious UE (UEadv ), and also needs to know the IMSI of disregards the standard’s security recommendations and choose
the victim UE. We assume there is a private channel between a weak-/no- security context during connection establishment.
the eNodeBadv and the UEadv . Implications: The implications of this attack include:
Attack description. In this attack, the adversary impersonates (1) Deception: The adversary deceives the victim into be-
an already attached victim UE (UEvic ) to connect to the EPC by lieving that the UEvic is connected to the core network.
collaborating with the eNodeBadv and the UEadv . Suppose the (2) Location History Poisoning: Since the UEadv does not
UEvic is already attached with the legitimate eNodeB denoted need to be in the same tracking area as the UEvic , it can
by eNodeBbenign . The attack can be broken down into two authenticate itself to the EPC from a different tracking area and
main goals: (i) Force UEvic to disconnect from the EPC; (ii) thus provide misleading location information about the UEvic .
UEadv pretends to be UEvic to connect to the EPC. Thus, the UEadv can poison the location history of the UEvic
by performing this attack successively from different tracking
Disconnecting UEvic from the EPC: For disconnecting the
areas. As a result, a fugitive or criminal hiding in one location
UEvic from the EPC, we use our paging with IMSI attack. This
can deceive the core network into believing that the criminal
can also be achieved with our network initiated detach request
has attached to the core network from a different location.
or auth reject attacks.
(3) Loss of confidentiality: The security mode command
UEadv connecting to the EPC by impersonating as UEvic : message sent by the MME during the attach procedure in-
As the UEvic detached itself from the EPC due to a paging with cludes the selected cipher (EEA0-EEA7) and integrity protec-
IMSI message, it will try attach to the eNodeB with the highest tion (EIA0-EIA7) algorithms of the MME. By observing the
signal strength; which is the eNodeBadv . The UEvic will send security mode command messages of all four major network
an attach request message mreq to the eNodeBadv which the providers in the US, we have observed that at least one
eNodeBadv forwards to the UEadv . The UEadv then sends the carrier (OP-I) never used encryption (i.e., uses EEA0—no
same attach request mreq to the eNodeBbenign . The legitimate cipher). Note that, to keep the four major US network oper-
MME will send an authentication challenge c to the UEadv ators anonymous, we use pseudonyms (i.e., OP-I, OP-II, OP-
through the eNodeBbenign upon receipt of mreq . The UEadv III, OP-IV) to identify them. We have observed this insecure

10
 Dete- a custom-built LTE network and commercial networks with a
# Prior attack How/Why?
cted
logical Faraday cage [13].
1 Downgrade using tau reject [13] Yes LTEInspector.
2 Denial of all services [13] Yes LTEInspector.
Do not model A. Testbed Setup and Assumption Validation
3 Denial of selected services [13] No data for
attach request. We now describe our testbed setup for attack validation.
Location tracking through mapping Do not model mul-
4 user’s phone number/social network ID No tiple instance of 1) Malicious eNodeB Setup: We have used a Universal
to GUTI [8], [13]. UEs.
5 IMSI catching [16] Yes LTEInspector.
Software-defined Radio Peripheral device (i.e., USRP B210
Do not model RRC [39]) connected to an Intel Core i7 machine running Ubuntu
6 Fine-grained location exposure [13] No 14.04 as the hardware component and OpenLTE [40], an
layer messages.
7
DoS exploiting race condition with
Yes LTEInspector. open source LTE protocol stack implementation, to set up a
paging response [38] in 2G malicious eNodeB which costs around $1300 for the dedicated
Service hijacking exploiting race condi-
8 tion with paging response [38] in 2G Yes LTEInspector. hardware (i.e., excluding the core i7 machine). We used
Linkability using TMSI reallocation OpenLTE’s LTE_Fdd_enodeb application which simultane-
9 Yes LTEInspector.
command [11] in 3G ously acts as a bare-minimal eNodeB, a mobility management
Linkability of IMSI to GUTI using entity (MME), and a home subscriber server (HSS). We have
10 paging request [10] in 3G Yes LTEInspector.
Linkability using
implemented support for the detach procedure in OpenLTE as
11 auth sync failure [10] in 3G Yes LTEInspector. it originally had support for the attach procedure only. We
12 Man-in-the-Middle in 2G [9] Yes LTEInspector. have also instrumented OpenLTE to inject different fabricated
13 Man-in-the-Middle in 3G [12] No Do not model data. messages (e.g., network initiated detach request message)
Table IV: Prior attacks (related to attach, detach, and paging when necessary. For validating attacks against the paging
procedures) that are detected/not detected by LTEInspector. procedure, we use srsLTE [41] which we enhanced to support
eNodeB-initiated paging messages; its original support only
practice multiple times in two different geographical locations. included MME-initiated paging messages.
The adversary hence can learn the UEvic ’s conversation, SMSs,
eNodeB configuration. Our malicious eNodeB can imper-
and data through the UEadv and the eNodeBadv . We reported
sonate the legitimate eNodeB of a network operator (i.e.,
this to the affected carrier which has now been addressed.
OP-I to OP-IV) by broadcasting system info block messages
(4) Complete or Selective DoS: Using this attack, the with higher signal power. For successful impersonation, these
UEadv and the eNodeBadv can relay the incoming/outgoing messages must include parameter values that are equal to
traffic of the UEvic and the EPC. Therefore, the UEadv and that of an operator’s legitimate eNodeB. The adversary uses
the eNodeBadv can deny the UEvic ’s phone-calls/SMS/data- a UE with the operator’s SIM to learn the parameters in
transfers completely/selectively. Consequently, the operational the system info block messages sent by the operator’s eN-
network is deprived of the charges for the incoming/outgoing odeB. In our setup, we use both our custom-built sniffer
calls and SMSs. and QXDM [42] to sniff the incoming and outgoing LTE
(5) Profiling victim’s service usage: Since all the incom- messages on a consumer UE to learn the operator’s parameters.
ing/outgoing communications of the UEvic take place through Table V shows the parameters that we capture from the
the UEadv and the eNodeBadv , the adversary can profile the operator eNodeB’s system info block messages. We use them
service usage pattern (i.e., patterns of phone calls, SMSs, data) to configure the malicious eNodeB with OpenLTE.
of the victim.
Parameters Description
E. Prior Attacks Detected by LTEInspector band The frequency band number of the network operator.
dl earfcn E-UTRA absolute radio frequency channel number.
In addition to the new attacks, LTEInspector is capable mcc Mobile country code specific to a country.
mnc Mobile network code specific to a network operator.
of detecting 9 [16], [13], [38], [10], [11], [9] out of 13 prior p0 nominal pucch Power control parameter.
attacks (see Table IV) that are relevant in the context of attach, p0 nominal pusch Power control parameter.
detach, and paging procedures. The previous attacks [13], q rx lev min Used for cell re-selection.
[8], [12] that LTEInspector cannot detect exploit one of the q hyst Used for cell re-selection
DRX cycle Paging cycle
following which LTEInspector currently does not support: (1)
message data, (2) multiple instances of UEs or MMEs, (3) Table V: Configuration parameters captured from Operator’s
other layers’ (e.g., RRC layer) messages, (4) 2G/3G procedures system info block messages.
that are different from 4G LTE, (5) properties about sets Learning IMSI/IMEI. As soon as the victim UE is forced
of traces, and (6) performance related parameters (e.g., data to connect with the malicious eNodeB, the malicious eNodeB
transmission and reception rate). sends an identity request (IMSI/IMEI) message to the vic-
tim UE which responds with the identity response message
V. VALIDATION OF ATTACKS WITH T ESTBED including its IMSI/IMEI.
In this section, we describe the verification of the new Learning GUTI. We use the well-known set intersection
attacks (along with their adversarial assumptions) detected by technique to find the GUTI as described in [8].
LTEInspector. We have tried to exercise restraint—conforming
to best practices—in validating the effectiveness of the dif- 2) Malicious UE Setup: We use a USRP B210 [39] running
ferent vulnerabilities while maintaining the validation process srsUE [43] (open source protocol stack implementation for
meaningful. To limit the impact of our attacks, we use both UE) as the malicious UE which costs around $1300.

11
 Detach Type Our observation of victim UE’s response
attack ∼ 8 times to that of the benign condition. The attacker
Re-attach re- No cellular signals (shows “No Service”). Requires mobile can make it worse, in case it chooses to inject the paging with
quired restart or SIM re-insert to get the 4G LTE back again.
Re-attach not Detaches from 4G LTE. Immediately downgrades to GUTI in every paging occasion.
required 3G/2G and sends attach request to the 3G/2G network.
IMSI detach Does not detach from the 4G LTE network. VI. R ELATED W ORK
Table VI: Victim UE’s responses to different types of detach. In this section, we present existing efforts that focus on
the security, privacy, and availability of cellular networks. In
paging cycle/occasions. To this end, we captured and decoded this context, although prior work has extensively investigated
the system info block and attach request messages—sent in the security and privacy issues of 2G and 3G protocols [8],
plaintext by the carrier’s eNodeB and the victim UE, respec- [6], [7], [49], [50], there is less work that addresses the same
tively, and learned the parameters relevant for computing the concerns for the 4G LTE networks [13].
victim UE’s paging occasion (e.g., DRX cycle, IMSI). The
malicious eNodeB then injected fake paging messages (with The closest to LTEInspector’s approach is by Tu et al. [17]
no paging records) at the paging occasions of the victim UE. where they focus on identifying non-trivial interactions—using
We observed that the victim UE only received the fake paging an explicit-state model checker [23]—between the different
messages instead of the legitimate messages. control-plane protocol layers of LTE. Unlike LTEInspector,
their work, however, can neither explicitly reason about ad-
After hijacking the victim UE’s paging channel, we allowed versarial actions nor can support cryptographic constructs.
two senders to place phone calls and send SMSs to victim’s
phone number triggering the (benign) MME to send multiple Man-in-the-Middle Attacks: Meyer et al. [12] exploit the null
paging messages to the victim UE. We observed that the victim integrity of the security mode command message in 3G net-
did not receive any of the legitimate paging messages, i.e., the works to perform a man-in-the-middle attack. In contrast, our
service notifications. The victim’s unresponsiveness was also authentication relay attack in 4G LTE allows the adversary to
noticed on the sender-side. connect to the EPC without nullifying the security capabilities.
In this attack the adversary, however, cannot decrypt or inject
P-2 Stealthy Kicking-off Attack: For this attack, instead valid encrypted messages unless the operator uses a weak or no
of injecting empty paging messages, the malicious eNodeB security context. Rupprecht et al. [44] used an implementation
fabricated the paging messages with a paging record contain- bug in a particular LTE dongle (Huawei E3276 USB Dongle)
ing the victim UE’s IMSI. As soon as the victim UE received to demonstrate a man-in-the-middle attack for 4G LTE.
this message, we observed that it locally detached itself from
the network and sent an attach request, confirming the attack. IMSI Catching Attacks and 5G AKA Solutions: The IMSI
catching attacks [51], [5], [52] still prevail for 4G LTE
P-3 Panic Attack: To inject fake paging messages to networks as they did for 2G and 3G networks. Arapinis et
arbitrary neighboring UEs, the malicious eNodeB broadcasted al. [10] propose to use public key encryption mechanism for
paging messages at all possible paging occasions. Each of protecting against the IMSI exposure attacks. However, public
these paging messages had the ETWS (earthquake and tsunami key encryption of the IMSI will likely incur high overhead
warning system) bits set to provide the UEs an alert noti- during the attach procedure. Also, this mechanism will require
fication. Upon receiving such alert notification, a UE looks managing multiple public keys for different MMEs (i.e., the
for the actual warning message which the eNodeB broadcasts serving network) in the SIM, as well as modification of the
through the system information block type 10 or 11 or 12 LTE protocol implementation in the legacy UEs. Due to these
messages. Since such warning messages may be received by reasons, the 3GPP community has not yet adopted this solution
other mobile phones which are not subject to our experiment, for real deployments. Broek et al. [16] and Khan et al. [53]
we refrained the malicious eNodeB from sending the actual both proposed changing pseudonym-based (PMSI) defense
warning messages. against IMSI catching attack which have several limitations as
discussed in Section IV. The 5G AKA protocol proposed by
P-4 Energy Depletion Attack: We quantitatively measure
Norman et al.[54] can be viewed as a hybrid of the approaches
the UE’s energy depletion due to this attack. In particular, we
by Arapinis et al. [10] and Broek et al. [16]. In such a protocol,
leverage the strong correlation between energy consumption
the UE encrypts the IMSI using HSS’ public key—unlike the
with message transmission rate [47]. We essentially measured
public-key of MME as in Arapinis et al. [10]—during the very
the message transmission rate in the benign and attack case,
first occurrence of the attach procedure and then subsequently
and drew conclusions about energy consumption. To realize
uses pseudo-IMSIs for communicating with MME. Although
this attack, we configured the malicious eNodeB to broadcast
this approach does not have to manage multiple MME public
paging message with the victim’s GUTI at every third paging
keys, it will likely incur additional overhead due to the use of
occasion (i.e., ∼ 3 seconds) of the victim UE. Upon reception
public key encryption and also suffers from the same weakness
of this paging message, we observed that the victim UE sent
as the solution proposed in [16]. Dabrowski et al. [14] and
an encrypted and integrity protected service request message
Nohl [52] have designed a mobile application that warns the
to the malicious eNodeB. We also carried out this attack where
users about the likely presence of IMSI catchers. In contrast,
the paging message included the victim’s IMSI in which case,
LTEInspector can identify the IMSI catching attack and other
however, the victim initiated the attach procedure. For the
attacks that the adversary may launch after knowing the IMSIs.
paging with GUTI, we carried out the attack for an hour and
observed that the victim sent 1200 service request messages. Linkability Attacks: Arapinis et al. [10] exploit the paging
In the benign case (measured from 4G LTE traces [48]), messages with GUTI for linking the IMSI to the GUTI in 3G
however, on average the UE responds to 156 (std. dev. 14.27) protocols. In contrast, using paging message with IMSI in 4G
paging messages . Roughly, the energy depletion due to this LTE we demonstrate how an adversary along with other attacks

13
(discussed in Section IV-B) can link the IMSIs in 3GPP [35] currently manual and the extracted FSMs are not complete. In
and the old PMSI with the new PMSI in the enhanced the same vein, the list of properties we have checked is not
Authentication and Key Agreement (AKA) mechanism [16]. exhaustive. Our current model also does not capture all the
data embedded in the messages.
Traceability Attacks: Arapinis et al. [11] presented a trace-
ability attack by exploiting an implementation bug in the 3G Threat to Validity. Our manually extracted FSMs from the
network which violates the 3GPP standard recommendation of 3GPP standard may not reflect the behavior of real operational
adopting new temporary identity for the UE with a tracking networks. Inaccuracies in the FSMs may induce false positives,
area change. In another work, Arapinis et al. [10] demonstrate although, we have not observed any. Due to ethical considera-
another traceability attack in which the adversary replays the tions, we limit our experiments to a custom-built network for
auth request for the victim UE to all the UEs in an area and some attack validations which may not faithfully capture the
detects the presence of the victim UE from the causes (MAC operational network behavior.
failure or SQN synchronization failure). In contrast, our
traceability attack with the security mode command procedure VIII. C ONCLUSION AND F UTURE W ORK
exploits the missing nonces in security mode command, a In this paper, we propose LTEInspector which employs
different implementation bug of the commercial networks. an adversarial model-based testing philosophy for expos-
ing attacks against three critical procedures of 4G LTE.
Denial-of-Service (DoS) Attacks: Shaik et al. [13] demonstrate LTEInspector harnesses the strengths of both a symbolic model
3 DoS attacks against UEs in which downgrading to 3G/2G checkers and a protocol verifier and is demonstrated to be
and denial of all network services are performed with the same effective in finding 10 novel and 9 prior attacks. We have also
tracking area update reject message with just two different validated most of our attacks (i.e., 8 out of 10) in a testbed.
causes. In contrast, our DoS attacks use four new techniques
as discussed in Section IV. As opposed to the DoS attacks Future work. In future, we would like to explore the
against the UE, Jover et al. [15] discuss a DoS attack against following four directions: (i) supporting analysis of other pro-
the EPC using a compromised UE/eNodeB that sends huge cedures and protocol layers (e.g., RRC and PDCP) messages;
number of attach request messages to the EPC and thus takes (ii) automating some of the manual tasks in LTEInspector; (iii)
the EPC down. Jermyn et al. [55] show a similar DoS attack enriching the model features and analysis of LTEInspector to
and simulate a set of compromised UEs that exhaust the victim handle message data; (iv) investigating the defense techniques.
UEs’ traffic capacity. Golde et al. [38] exploit a race condition
in the paging message responses in 2G networks that enables a ACKNOWLEDGEMENT
malicious UE to send the paging response message before the We thank our Shepherd, Yongdae Kim, and the anony-
victim UE, and thus preventing the victim UE from receiving mous reviewers for their valuable suggestions. This work
incoming phone calls/SMS. was supported by Intel/CERIAS RAship, FFTF fellowship
by Schlumberger Foundation, NSF grant CNS-1657124, NSF
VII. D ISCUSSION grant CNS-1719369, and Intel as part of the NSF/Intel ICN-
Properties amenable to our analysis. LTEInspector can WEN program.
reason about temporal trace properties (with cryptographic
constructs) of both safety and liveness variations. Our current R EFERENCES
model cannot handle properties that require reasoning about [1] Hackers Are Tapping Into Mobile Networks’ Backbone, New Re-
sets of traces (e.g., noninterference) instead of a single trace. search Shows, https://www.forbes.com/sites/parmyolson/2015/10/14/
hackers-mobile-network-backbone-ss7.
For such properties, we mainly rely on the protocol verifier.
[2] Hackers Take Down the Most Wired Country in Europe, https://www.
Defenses. We deliberately do not discuss defenses for the wired.com/2007/08/ff-estonia/.
observed attacks as retrospectively adding security into an [3] 3GPP Standard, www.3gpp.org.
existing protocol without breaking backward compatibility [4] 3GPP Standard. Release 12., http://www.3gpp.org/specifications/
often yields band-aid-like-solutions which do not hold up releases/68-release-12.
under extreme scrutiny. It is also not clear, especially, for the [5] D. Abodunrin, Y. Miche, and S. Holtmanns, “Some dangers from 2g
networks legacy support and a possible mitigation,” in Communications
authentication relay attack whether a defense exists that does and Network Security (CNS), Sept 2015, pp. 585–593.
not require major infrastructural or protocol overhaul. A pos- [6] P. P. C. Lee, T. Bu, and T. Woo, “On the detection of signaling dos
sibility is to employ a distance-bounding protocol; realization attacks on 3g wireless networks,” in 26th International Conference on
of such protocol is, however, rare in practice [56]. Due to the Computer Communications (INFOCOM), May 2007, pp. 1289–1297.
strict performance requirements of 4G LTE, any public-key [7] N. Golde, K. Redon, and R. Borgaonkar, “Weaponizing Femtocells:
cryptography-based solution is unlikely to be feasible. On the The Effect of Rogue Devices on Mobile Telecommunications,” in
contrary, symmetric-key cryptography often have scalability Proceedings of the 19th Annual Network & Distributed System Security
Symposium, Feb. 2012.
issues due to establishing a common shared key for broadcast-
[8] D. F. Kune, J. Koelndorfer, and Y. Kim, “Location leaks on the gsm
ing sensitive (e.g., paging) messages. Further investigation on air interface,” in NDSS, 2012.
defenses is, therefore, required for balancing the performance
[9] I. Androulidakis, “Intercepting mobile phone calls and short messages
and scalability as well as guaranteeing the security. using a gsm tester,” in 18th Conference on Computer Networks, Ustron,
Poland, A. Kwiecień, P. Gaj, and P. Stera, Eds., 2011, pp. 281–288.
Limitations. Although LTEInspector suggests a systematic ap-
[10] M. Arapinis, L. Mancini, E. Ritter, M. Ryan, N. Golde, K. Redon,
proach, it currently requires human intervention, for instance, and R. Borgaonkar, “New privacy issues in mobile telephony: Fix and
deciding which sub-steps of the counterexample is required to verification,” in Proceedings of the 2012 ACM Conference on Computer
be modeled in ProVerif and how. Also, our FSM extraction is and Communications Security, ser. CCS ’12. ACM, 2012, pp. 205–216.

14
[11] M. Arapinis, L. I. Mancini, E. Ritter, and M. Ryan, “Privacy through [32] B. Blanchet, “Automatic verification of correspondences for security
pseudonymity in mobile telephony systems,” in NDSS, 2014. protocols,” Journal of Computer Security, vol. 17, no. 4, pp. 363–434,
[12] U. Meyer and S. Wetzel, “A man-in-the-middle attack on umts,” in Jul. 2009.
Proceedings of the 3rd ACM Workshop on Wireless Security, ser. WiSe [33] M. Abadi and B. Blanchet, “Analyzing Security Protocols with Secrecy
’04. ACM, 2004, pp. 90–97. Types and Logic Programs,” in 29th Annual ACM SIGPLAN - SIGACT
Symposium on Principles of Programming Languages (POPL 2002).
[13] A. Shaik, J. Seifert, R. Borgaonkar, N. Asokan, and V. Niemi, “Practical
Portland, Oregon: ACM Press, Jan. 2002, pp. 33–44.
attacks against privacy and availability in 4g/lte mobile communication
systems,” in 23nd Annual Network and Distributed System Security [34] E. A. Emerson and K. S. Namjoshi, “Reasoning about rings,” in Pro-
Symposium, NDSS, San Diego, CA, USA, February 21-24, 2016. ceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages (POPL). ACM, 1995, pp. 85–94.
[14] A. Dabrowski, N. Pianta, T. Klepp, M. Mulazzani, and E. Weippl, “Imsi-
catch me if you can: Imsi-catcher-catchers,” in Proceedings of the 30th [35] 3GPP. Non-Access-Stratum (NAS) protocol for Evolved Packet System
Annual Computer Security Applications Conference, ser. ACSAC ’14. (EPS); Stage 3 Specification 3GPP TS 24.301 version 12.8.0 Release
ACM, 2014, pp. 246–255. 12., [Online]. Available: http://www.3gpp.org/dynareport/24301.htm.
[15] R. P. Jover, “Security attacks against the availability of lte mobility [36] R. Racic, D. Ma, and H. Chen, “Exploiting mms vulnerabilities to
networks: Overview and research directions,” in Wireless Personal Mul- stealthily exhaust mobile phone’s battery,” in Securecomm and Work-
timedia Communications (WPMC), 2013 16th International Symposium shops, Aug 2006, pp. 1–10.
on, June 2013, pp. 1–9. [37] J. Serror, H. Zang, and J. C. Bolot, “Impact of paging channel overloads
or attacks on a cellular network,” in Proceedings of the 5th ACM
[16] F. van den Broek, R. Verdult, and J. de Ruiter, “Defeating imsi catchers,”
Workshop on Wireless Security, 2006, pp. 75–84.
in Proceedings of the 22Nd ACM SIGSAC Conference on Computer and
Communications Security, ser. CCS ’15. ACM, 2015, pp. 340–351. [38] N. Golde, K. Redon, and J.-P. Seifert, “Let me answer that for you:
Exploiting broadcast information in cellular networks,” in Proceedings
[17] G.-H. Tu, Y. Li, C. Peng, C.-Y. Li, H. Wang, and S. Lu, “Control-plane of the 22Nd USENIX Conference on Security, 2013, pp. 33–48.
protocol interactions in cellular networks,” in Proceedings of the 2014
ACM Conference on SIGCOMM. ACM, 2014, pp. 223–234. [39] USRP B210, https://www.ettus.com/product/details/UB210-KIT.
[18] Cellular Service, https://www.fcc.gov/wireless/bureau-divisions/ [40] OpenLTE, http://openlte.sourceforge.net/.
mobility-division/cellular-service. [41] srsLTE, https://github.com/srsLTE.
[19] D. Dolev and A. C. Yao, “On the security of public [42] Qxdm Professional Qualcomm Extensible Diagnostic-
key protocols,” Stanford, CA, USA, Tech. Rep., 1981, Monitor, www.qualcomm.com/media/documents/files/
http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail&id=oai qxdm-professional-qualcomm-extensible-diagnostic-monitor.pdf.
[20] K. R. Apt and D. C. Kozen, “Limits for automatic verification of finite- [43] srsUE, https://github.com/srsLTE/srsUE.
state concurrent systems,” Inf. Process. Lett., vol. 22, no. 6, pp. 307–309, [44] D. Rupprecht, K. Jansen, and C. Pöpper, “Putting lte security functions
May 1986. to the test: A framework to evaluate implementation correctness,” in
Proceedings of the 10th USENIX Conference on Offensive Technologies,
[21] Z. Manna and A. Pnueli, “A hierarchy of temporal properties (invited
paper, 1989),” in Proceedings of the ninth annual ACM symposium on ser. WOOT’16, 2016, pp. 40–51.
Principles of distributed computing. ACM, 1990, pp. 377–410. [45] N. Bui and J. Widmer, “Owl: A reliable online watcher for lte control
channel measurements,” in Proceedings of the 5th Workshop on All
[22] A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri, “Nusmv: A
Things Cellular: Operations, Applications and Challenges, ser. ATC
new symbolic model verifier,” in Proceedings of the 11th International
’16. ACM, 2016, pp. 25–30.
Conference on Computer Aided Verification, ser. CAV ’99. London,
UK, UK: Springer-Verlag, 1999, pp. 495–499. [46] OpenEPC, www.openepc.com.
[23] G. Holzmann, Spin Model Checker, the: Primer and Reference Manual, [47] P. Y. Kong, “Power consumption and packet delay relationship for het-
1st ed. Addison-Wesley Professional, 2003. erogeneous wireless networks,” IEEE Communications Letters, vol. 17,
no. 7, pp. 1376–1379, July 2013.
[24] B. Blanchet, “Modeling and verifying security protocols with the
[48] Y. Li, C. Peng, Z. Yuan, J. Li, H. Deng, and T. Wang, “Mobileinsight:
applied pi calculus and proverif,” Foundations and Trends in Privacy
Extracting and analyzing cellular network information on smartphones,”
and Security, vol. 1, no. 1-2, pp. 1–135, 2016.
in Proceedings of the 22nd Annual International Conference on Mobile
[25] S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The tamarin prover Computing and Networking, ser. MobiCom ’16, 2016, pp. 202–215.
for the symbolic analysis of security protocols,” in Proceedings of the [49] P. Traynor, P. McDaniel, and T. La Porta, “On attack causality in
25th International Conference on Computer Aided Verification (CAV). internet-connected cellular networks,” in Proceedings of 16th USENIX
Springer-Verlag, 2013, pp. 696–701. Security Symposium, 2007, pp. 21:1–21:16.
[26] A. Armando and et al., “The avispa tool for the automated validation of [50] P. Traynor, M. Lin, M. Ongtang, V. Rao, T. Jaeger, P. McDaniel, and
internet security protocols and applications,” in Proceedings of the 17th T. La Porta, “On cellular botnets: Measuring the impact of malicious
International Conference on Computer Aided Verification, ser. CAV’05. devices on a cellular network core,” in Proceedings of the 16th ACM
Springer-Verlag, 2005, pp. 281–285. Conference on Computer and Communications Security (CCS), 2009,
[27] J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, pp. 223–234.
“Refinement types for secure implementations,” ACM Trans. Program. [51] R. Borgaonkar and S. Udar, “Understanding imsi privacy,” in BlackHat,
Lang. Syst., vol. 33, no. 2, pp. 8:1–8:45, Feb. 2011. 2014.
[28] G. Lowe, “Breaking and fixing the needham-schroeder public-key pro- [52] K. Nohl, “Mobile self-defense.” [Online]. Avail-
tocol using fdr,” in Proceedings of the Second International Workshop able: https://events.ccc.de/congress/2014/Fahrplan/system/attachments/
on Tools and Algorithms for Construction and Analysis of Systems, ser. 2493/original/Mobile Self Defense-Karsten Nohl-31C3-v1.pdf
TACAs ’96. Springer-Verlag, 1996, pp. 147–166. [53] M. S. A. Khan and C. J. Mitchell, “Trashing imsi catchers in mobile
[29] C. J. Cremers, “Unbounded verification, falsification, and characteriza- networks,” in Proceedings of the 10th ACM Conference on Security and
tion of security protocols by pattern refinement,” in Proceedings of the Privacy in Wireless and Mobile Networks, 2017, pp. 207–218.
15th ACM Conference on Computer and Communications Security, ser. [54] Protecting IMSI and User Privacy in 5G Networks, www.ericsson.com/
CCS ’08. ACM, 2008, pp. 119–128. res/docs/2016/protecting-imsi-and-user-privacy-in-5g-networks.pdf.
[30] A. C. Yao, “Theory and application of trapdoor functions,” in Pro- [55] J. Jermyn, G. Salles-Loustau, and S. Zonouz, “An analysis of dos attack
ceedings of the 23rd Annual Symposium on Foundations of Computer strategies against the lte ran,” vol. 3, 2014, pp. 159–180.
Science, ser. SFCS ’82. IEEE Computer Society, 1982, pp. 80–91.
[56] K. B. Rasmussen and S. Čapkun, “Realization of rf distance bounding,”
[31] J.-K. Tsay and S. F. Mjølsnes, “A vulnerability in the umts and lte in Proceedings of the 19th USENIX Conference on Security, ser.
authentication and key agreement protocols,” in Proceedings of the 6th USENIX Security’10, 2010, pp. 25–25.
MMM-ACNS. Springer-Verlag, 2012, pp. 65–76.

15