Ravishankar Borgaonkar
email: ravi.borgaonkar@sintef.no

Lucca Hirschi
email: lucca.hirschi@inria.fr.

Shinjo Park

Altaf Shaik New
email: altaf329@sect.tu-berlin.de

AK ← f5(R, K) MAC ← f1(⟨SQN HN , R⟩, K) CONC ← SQN HN ⊕ AK AUTN ← ⟨CONC, MAC⟩ CK, IK ← f3(R, K), f4(R, K) xRES ← f2(R, K) SQN HN ← Sqn Hn +

Autn Ak

RES K ) Auth_Resp

Proceedings on Privacy Enhancing Technologies 2019

Mobile communications are used by more than two-thirds of the world population who expect security and privacy guarantees. The 3rd Generation Partnership Project (3GPP) responsible for the worldwide standardization of mobile communication has designed and mandated the use of the AKA protocol to protect the subscribers' mobile services. Even though privacy was a requirement, numerous subscriber location attacks have been demonstrated against AKA, some of which have been fixed or mitigated in the enhanced AKA protocol designed for 5G. In this paper, we reveal a new privacy attack against all variants of the AKA protocol, including 5G AKA, that breaches subscriber privacy more severely than known location privacy attacks do. Our attack exploits a new logical vulnerability we uncovered that would require dedicated fixes. We demonstrate the practical feasibility of our attack using low cost and widely available setups. Finally we conduct a security analysis of the vulnerability and discuss countermeasures to remedy our attack.

Introduction

As of 2018, around 5 billion mobile subscribers equipped with Universal Subscriber Identity Module cards (USIM) are accessing cellular network services (e.g., Internet, calls), mostly relying on 3G or 4G technologies [START_REF]Definitive data and analysis for the mobile industry[END_REF] (e.g., ca. 75% of connections in Europe and North America). With the growing importance of cellular network services in our daily activities, there is a crucial need to provide security and privacy protection to mobile subscribers. in the specifications of all aforementioned variants of AKA: the protection mechanism of the SQN can be defeated under specific replay attacks due to its use of Exclusive-OR (XOR) and a lack of randomness. We show how to leverage this vulnerability to break the confidentiality of SQN, thus defeating the purpose of a dedicated protection mechanism and breaking an explicit privacy requirement [START_REF]3G security; Security architecture[END_REF]. We show that partly learning SQN leads to a new class of privacy attacks (i.e., activity monitoring attacks): an active attacker can leverage fake base stations and our attack to learn information about targeted subscribers' mobile service consumption, even when subscribers move away from the attack area (e.g., range of a fake base station). This is in stark contrast to location attacks that do not reveal service consumption and requires the targeted subscribers to stay in attack areas. Less importantly, we show that our logical vulnerability also yields a new location attack.

2. Low-cost proof of concept. We demonstrate the feasibility of our attack using widely available and low-cost setup on commercial 4G networks in several European countries. Our attack affects all 3G and 4G devices currently deployed all over the world and future 5G devices (according to the specification [START_REF] Gpp | Security architecture and procedures for 5G System[END_REF]).

3. Security analysis and countermeasures. We discuss the weaknesses of the AKA protocol, its deployment, design trade-offs, and the overall cellular architecture that have made possible our attack in order to draw lessons for the future generation networks. We propose countermeasures to our attack and establish formal security guarantees using the state-of-the-art tool Tamarin [START_REF] Meier | The Tamarin Prover for the Symbolic Analysis of Security Protocols[END_REF].

Impact. Unlike the previously known location privacy attacks [START_REF] Arapinis | New privacy issues in mobile telephony: fix and verification[END_REF][START_REF] Hahn | A Privacy Threat in 4th Generation Mobile Telephony and Its Countermeasure[END_REF][START_REF] Shaik | Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems[END_REF][START_REF] Udar | Understanding IMSI Privacy[END_REF][START_REF] Van Den Broek | Defeating IMSI Catchers[END_REF][START_REF] Khan | Another look at privacy threats in 3G mobile telephony[END_REF][START_REF] Zhang | Security analysis and enhancements of 3GPP authentication and key agreement protocol[END_REF][START_REF] Khan | Vulnerabilities of UMTS Access Domain Security Architecture[END_REF][START_REF] Bikos | LTE/SAE Security Issues on 4G Wireless Networks[END_REF], we disclose a new type of privacy attack enabling subscriber activity monitoring. We now discuss subsequent impacts of our attack. First, an attacker can learn 3G, 4G, and 5G subscribers' typical activity patterns (e.g., number of calls, SMSs sent in a given time). We stress that those activity patterns can be monitored remotely for a long time even if, most of the time, subscribers move away from the attack areas. We followed the responsible disclosure procedure and reported our findings to the 3GPP, GSM Association (GSMA), several manufacturers (Ericsson, Nokia, and Huawei), and carriers (Deutsche Telekom and Vodafone UK). Our findings were acknowledged by the 3GPP and GSMA and remedial actions are underway to improve the protocol for the next generations. Finally, while 5G AKA will suffer from our attack in the first deployment of 5G (i.e., Release 15 [START_REF] Gpp | Security architecture and procedures for 5G System[END_REF], phase 1), we are still hopeful that 5G AKA could be fixed before the deployment of the second phase (Release 16, to be completed by the end of 2019).

Outline. In section 2, we explain the general cellular security architecture and the core protocol underlying all AKA protocol variants. Section 3 presents our new logical vulnerability breaking the confidentiality of SQN. In Section 4, we show how the latter can be exploited to mount activity monitoring and location attacks and discuss practical impact. In Section 5, we show feasibility of our attacks in real 4G networks. We conduct a security analysis in Section 6 and provide potential countermeasures in Section 7. We conclude in Section 8.

Background

We first give a high-level overview of the security architecture used in 3G, 4G, and 5G networks and explain how mobile subscribers are authenticated to the network using the AKA protocol. We then describe the different privacy requirements of 3G, 4G, and 5G networks outlined in the 3GPP specification. We conclude with a discussion on threat models, previously known attacks against the AKA protocol, formerly proposed fixes, and a comparison with our attack.

Security Architecture and the AKA Protocol

We describe a simplified view of the security architecture deployed in cellular networks and focus on the parts that are necessary to understand our attack. We also slightly simplify our description of the AKA protocol for the sake of clarity and only focus on the core protocol which is common to all the AKA protocol variants. Further, we adopt a simplified terminology since the official terminology heavily depends on the generation. We refer the knowledgeable reader to Appendix A where an informal correspondence with standardized terminologies for the different generations is given.

Architecture

The cellular network architecture mainly consists of three components. First, User Equipments (UEs) are carried by subscribers (we shall use both terms alternatively) and are typically smartphones or IoT devices containing a USIM card. Second, Home Networks (HNs) contain a database of their subscribers' and their corresponding USIM cards and are in charge of their authentication. However, it is often the case that UEs are in locations where their corresponding HN has no base station (i.e., antennas that may connect UEs to the network). Therefore, the architecture also considers a third entity: the Serving Networks (SN ) to which UEs may attach to and that play the role of relays to HNs.

Each UE contains a USIM having cryptographic capabilities (e.g., symmetric encryption, MAC) which notably stores:

-an unique and permanent subscriber identity, called International Mobile Subscriber Identity (IMSI), -a unique, permanent secret symmetric key that we indicate as K IMSI (used as a shared secret between a UE and its corresponding HN ), -and a 48-bits counter, called Sequence Number that we denote as SQN (used as replay protection, as explained later in this section).

The HN associated with some USIM card stores the same information in its database. When the context is clear, we use K to refer to K IMSI .

The AKA Protocol

When a UE attaches to a SN (or when UE requests access to a service such as sending an SMS or making a call), it needs to establish a secure channel with the SN (ensuring confidentiality of the user data) after authenticating itself to its corresponding HN (mainly for billing purpose) and authenticating its HN (so that fake SN cannot establish such a channel and break confidentiality). To do so, 3GPP has standardized the AKA protocol (the only authentication method allowed for 3G, 4G and 5G for 3GPP access). While this protocol has evolved with each generation [START_REF] Gpp | Security architecture and procedures for 5G System[END_REF][START_REF]3G security; Security architecture[END_REF][START_REF]3GPP System Architecture Evolution (SAE); Security architecture[END_REF], its core specification remained the same. We shall only focus on this core protocol that already suffers from our attack. The AKA protocol achieves mutual authentication and key exchange between a UE and its corresponding HN , relying on some SN that is known by the HN . It allows some UE and SN to establish session keys to be used to secure subsequent communications (e.g., integrity and confidentiality of calls or SMSs). As mentioned before, the key K IMSI is used as a long-term shared secret, and SQN is used as replay protection for the UE. While SQN is expected to be synchronized between the UE and HN , it may become out-of-sync. We thus use SQN UE (resp. SQN HN ) to refer to the SQN value stored in the UE (resp. HN ). The AKA protocol is made up of 3 main phases: identification, challengeresponse, and re-synchronization procedure (that is optional and aims at updating SQN on the HN side in case SQN is out-of-sync). The whole protocol flow with message specifications is depicted in Figure 1, which uses the same notations as in this section.

Identification. First, the SN identifies the UE. If the current UE's identity is unknown to the SN , it may ask for the permanent identity IMSI (or an encryption thereof in 5G) by sending an Identity Request message. The UE then gives its identity in an Identity Response message. This identity enables the SN to request authentication material to the appropriate HN in the next phase. In 5G, UE never reveals its permanent identity in plaintext. It rather sends the randomized encryption thereof, protected with the HN 's public key, along with the HN 's identity (forming the so-called SUCI [START_REF] Gpp | Security architecture and procedures for 5G System[END_REF]).

Challenge-response.

Upon reception of a request for authentication material from a SN , the HN computes an authentication challenge made of a random nonce R and some message AUTN. In addition, the expected authentication response xRES = f2(R, K IMSI ) -computed using f2 described below-, the encryption key CK, and the integrity key IK are also computed by HN (but not sent by SN to UE). Note that, in 5G, the message xRES has a slightly different form; this has no impact on our attack.

The functions f1 -f5, f1 * , and f5 * , used to compute the authentication parameters, are one-way keyed cryptographic functions completely unrelated1 , and ⊕ denotes the eXclusive-OR (XOR) operator.

AUTN contains a MAC (Message Authentication Code) of the concatenation of R with the corresponding sequence number SQN HN stored for this subscriber. A new sequence number is generated by an increment of the counter. The sequence number SQN HN allows the UE to verify the freshness of the authentication request to defend against replay attacks and the MAC proves the authenticity of the challenge. However, SQN HN is not transmitted in clear text to avoid being eavesdropped on. Thus, the specification requires SQN to be concealed; i.e., XORed with a value, called Anonymity Key, that should remain private: AK = f5(R, K IMSI ). Formally, the concealed value, also included in AUTN, is as follows: CONC * = SQN HN ⊕ AK and allows the UE to extract SQN HN by computing AK.

The UE replies with an Authentication Response message when the authentication is successful, or Authentication Failure message with the cause of failure otherwise. To check whether authentication is successful or not, the UE extracts SQN HN from AUTN and checks that: (i) M AC is a correct MAC value w.r.

Privacy Requirements

The 3G and 4G specifications consider user identity and location confidentiality, and user untraceability as explicit privacy requirements [START_REF]3G security; Security architecture[END_REF][START_REF]3GPP System Architecture Evolution (SAE); Security architecture[END_REF]. Privacy was even more of a critical security goal in the design of 5G, as acknowledged by the standard: [START_REF] Gpp | Study on the security aspects of the next generation system[END_REF]: "Subscription privacy deals with various aspects related to the protection of subscribers' personal information, e.g., identifiers, location, data, etc. [...] The subscription privacy is very important area for Next Generation system as can be seen by the growing attention towards it, both inside and outside [3GPP]."

We also emphasize that, SQN is considered to be privacy-sensitive, and must be protected (i.e., remain confidential) by the AKA protocol: [START_REF]3G security; Security architecture[END_REF]: "[AK * ] is an anonymity key used to conceal the sequence number as the latter may expose the identity and location of the user." More recently, a 3GPP study on privacy explains that: [START_REF]Study on subscriber privacy impact in 3GPP[END_REF]: "[AKA] is an example of how to fulfill anonymity: [

...] Anonymizing technique used: use Anonymity Key in the Authentication Token to conceal (blind) the sequence number."

As we shall see, our attack defeats the purpose of the anonymity AK * .

Threat Model

While designing the AKA protocol in the year 2000, fake base stations were considered expensive in terms of required financial resources and the attacker's capabilities. However, such fake base stations can now be easily built using e.g., widely available hardware [START_REF]USRP B210[END_REF] or even WiFi technology [START_REF] O'hanlon | Mobile subscriber WiFi privacy[END_REF]. Therefore, in our security analysis, we consider both passive and active attacker models for 3G, 4G, and 5G networks. Passive. The passive adversary can sniff over-the-air radio broadcast channels using dedicated hardware and software (as described in Section 5). Note that, he does not need to know any key material used in the authentication procedure. Active. In addition, the active adversary has the capability to set up and operate a rogue base station to inject malicious traffic towards UEs. To achieve this, we assume he knows the protocol specification. However, we do not assume he knows any cryptographic keys.

Related Work on AKA and Known Flaws

There are numerous known attacks against the AKA protocol that were often described for older generation cellular networks but are still inherited in 4G networks due to the support of legacy systems and re-use of the same core protocol from AKA.

Identity Requests and IMSI-catchers. The first kind of attacks relies on the unprotected identity request mechanism that is broadcast over-the-air and is often termed as IMSI-catchers.

In a nutshell, an active attacker can easily broadcast an identity request to all the UEs in the area. Consequently, the UEs will reply with their permanent identities -this flaw is commonly exploited in IMSI catcher attacks [START_REF] Shaik | Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems[END_REF][START_REF] Udar | Understanding IMSI Privacy[END_REF][START_REF] Van Den Broek | Defeating IMSI Catchers[END_REF][START_REF] Khan | Another look at privacy threats in 3G mobile telephony[END_REF] to track subscribers in certain geographical areas. Even though UEs may use temporary identities, a passive attacker can find a co-relation between them and social identities [START_REF] Shaik | Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems[END_REF] (including Facebook, Twitter, or phone number).

Several studies cover research on how to secure unprotected messages carrying identity requests by additional cryptographic mechanisms [START_REF] Arapinis | New privacy issues in mobile telephony: fix and verification[END_REF][START_REF] Leu | Improving security level of LTE authentication and key agreement procedure[END_REF][START_REF] Li | Security Enhanced Authentication and Key Agreement Protocol for LTE/SAE Network[END_REF]. More importantly, in order to comply with the new stronger privacy protection requirement in 5G, 3GPP has modified the identity request phase of the AKA protocol. As mentioned earlier, the UE sends its permanent identity protected by randomized, asymmetric encryption using the HN 's public key, in such a way that the SNs or fake base stations only learn the underlying HN . Attack Area Safe Area (b) UEs were supposed to be safe when outside of attack areas. This is no longer the case due to our attack as UEs' activities in that area will partially leak when they re-enter an attack area. Fig. 2. Privacy threats depend on the UE 's location depicted with a dot. Attacker's fake base station (resp. genuine base station) is depicted with a cross (resp. box). Independently from the UE 's location, the UE 's activities have an effect on SQN stored at the HN.

Therefore, the aforementioned IMSI catchers attacks will be defeated in 5G.

However, note that, even after fixing these vulnerable messages (including the fix in 5G phase 1 [START_REF] Gpp | Security architecture and procedures for 5G System[END_REF]), our attack re-introduces new subscriber privacy risks since it does not rely on this identification phase.

Linkability of failure messages.

A few other attacks [START_REF] Arapinis | New privacy issues in mobile telephony: fix and verification[END_REF][START_REF] Hahn | A Privacy Threat in 4th Generation Mobile Telephony and Its Countermeasure[END_REF] exploit the fact that the AKA protocol exposes to the attacker the reason for the failure when an authentication is rejected by a UE: either Mac_Failure or Sync_Failure. This allows to track a targeted UE: it suffices to replay an old authentication challenge that UE has already received and then observe whether the reply is Mac_Failure (not the targeted UE) or Sync_Failure (only replied by the targeted UE). Again, our attack does not rely on distinguishing between the two sources of failure and cannot be prevented by fixing this issue alone (e.g., by merging the two sources of failure into a single message).

Comparisons Between Existing Attacks and our Attack

First, as explained in Section 2.3, our attack relies on a different logical vulnerability that is completely orthogonal to the attack vectors of prior, known attacks (i.e., unprotected identities and linkability of failure messages). Therefore, our attack would require different and dedicated fixes. Second, our attack poses a new kind of threat on privacy as it allows an attacker to learn subscribers' mobile services consumption patterns. In contrast, prior privacy attacks only leak the presence of targeted UEs in attack areas.

Third, our attack can break subscribers' privacy even when they escape attack areas. Indeed, remind that we consider a threat model for which attackers may exploit a limited number of fake base stations deployed at specific locations; typically busy crossing points (e.g., subway or train stations, airports), targeted offices (e.g., nearby embassies), or, places visited on a regular basis by targeted UEs (e.g., shops). With prior attacks, there were two very different situations (depicted in Figure 2):

-if the targeted UE is outside the range of attacker's base stations (e.g., at home), then the UE is completely safe: no fake base station-based attacks could break the subscriber's privacy (situation shown in Figure 2b); -otherwise, the subscriber may be subject to location attacks or monitoring attacks (i.e., attacker may eavesdrop on communication between UE and SN c to learn when UE consumes services) (situation depicted in Figure 2a). Therefore, even though the UEs may be attacked when in the range of attacker's fake base stations, as soon as they escape such (a priori narrow) areas, they were safe. This is unfortunately no longer the case as our attack introduces a totally new threat on privacy. Indeed, even when UEs are using mobile services outside the attack area, part of this activity may be leaked to some adversary using our attack the next time the UE enters again the attack area. Intuitively, this is because, independently of its location, the UE's activity has an effect on the counter SQN stored in the HN that will be leaked when the UE is (actively) under attack (we extensively discuss impacts on privacy in Section 4). We call this new kind of threat activity monitoring attacks. Hence, areas outside fake base stations range are no longer safe.

Logical Attack

In this section, we reveal the main attack vector based on a new logical vulnerability (Section 3.1) that can be exploited to mount an attack breaking the confidentiality of SQN (Section 3.2).

Logical Vulnerability

Our attack vector exploits a lack of randomness and the use of XOR in AUTS, more precisely in the concealed sequence number

CONC * = SQN UE ⊕AK * where AK * = f5 * (R, K IMSI ).
The value R is extracted from the challenge R, AUTN received by the UE. Therefore, if the UE receives two times the same challenge R, AUTN and yield two synchronization failures, then the two concealed SQNs will be of the form:

CONC * 1 = SQN 1 UE ⊕ AK * 1 and CONC * 2 = SQN 2 UE ⊕ AK * 2 such that AK * 1 = f5 * (R, K IMSI ) = AK * 2 .
Therefore, an attacker having a genuine challenge R, AUTN for some UE can transmit it to the UE at two different times t 1 and t 2 , retrieve values CONC * 1 and CONC * 2 , and compute:

CONC * 1 ⊕ CONC * 2 = (SQN 1 UE ⊕ AK * 1 )⊕ (SQN 2 UE ⊕ AK * 2 ) = SQN 1 UE ⊕ SQN 2 UE
where SQN i UE is the value SQN UE at time t i . We show in the next section that by cleverly choosing several timestamps t i 's, the attacker is able to exploit values such as SQN i UE ⊕ SQN j UE to break the confidentiality of SQN.

Breaking the Confidentiality of SQN

We show how an active attacker who knows any UE's identity (temporary, permanent, or encrypted) is then able to learn the n least significant bits of SQN HN , stored in the HN . The attacker first fetches 2 n + 2 successive, fresh, authentication challenges intended for the targeted UE and replays a total of 2(n+2) of them to the UE. The interaction is depicted in Figure 3. The attack ends with an offline computation using algo(⋅) which takes fetched AUTS messages as inputs and returns the n least significant bits of the sequence number SQN HN .

In a nutshell, the attack consists in choosing appropriate injections and timestamps t i such that the attacker can retrieve values δ i = SQN HN ⊕ (SQN HN + 2 i ) for 1 ≤ i ≤ n (see Section 3.2.1). We then explain (Section 3.2.2) how one can infer from the δ i 's the n least significant bits of SQN HN . Finally, we also show that under certain circumstances (i.e., when the UE is performing a lot of authentication sessions when in the attack area), a far less costly variant of the attack (only n + 2 injections) achieves the same goal (Section 3.2.3).

We describe the attack and our inference algorithm when the HN increments SQN HN by 1 after each successful authentications as described in Section 2. Our attack works for any such increment; the interaction is always the same and we designed a generic algo(⋅) parametrized by the increment used by the operator. However, for the sake of clarity, we only describe here our attack and our generic algorithm for an increment equal to 1. We describe the full algorithm in Appendix B. Note that the full algorithm might actually infer more than n bits for some inputs; we report on practical results of this algorithm in Section 5.

Fetching Data

In a first phase (loop for i = 0 to 2 n from Figure 3), the attacker needs to fetch consecutive challenges R i , AUTN i intended for the targeted UE. This is made possible by the fact that, in the AKA protocol, UE receives such challenges prior to authentication but after identification. Therefore, an attacker only needs to know one valid identity of the targeted UE (e.g., IMSI, temporary identifiers such as TMSI, or encrypted permanent identities such as SUCI) in order to (partly) impersonate the UE to the SN (and the corresponding HN ) and get those challenges. We will explain in Section 5 how this can be easily done in practice. Note that because SQN HN is incremented by 1 after the computation of every challenge, R i , AUTN i is computed based on some SQN value (that we denote by SQN HN (AUTN i )) equals to SQN 0 HN + i. Immediately after the first phase, the attacker injects the first challenge he obtained: R 0 , AUTN 0 . From the UE's perspective, this is a genuine challenge (the MAC verification (i) succeeds) that has never be received before and that is based on a recent enough SQN HN (AUTN 0 ) = SQN 0 HN (the freshness verification (ii) succeeds). At this time (before the second loop), SQN UE equals SQN 0 HN + 1. Then, the attacker injects again the challenge R 0 , AUTN 0 yielding a synchronization failure containing some AUTS ′ = ⟨c ′ , MAC * ⟩ message where the conceal SQN equals:

c ′ = (SQN 0 HN + 1) ⊕ f5 * (R 0 , K IMSI ).
In the last phase (loop for j = 0 to n from Figure 3), the attacker injects R 2 j , AUTN 2 j that is accepted by the UE, in order to make the UE updates its SQN UE to the value

SQN UE ∶= SQN HN (AUTN 2 j ) + 1 = SQN 0 HN + 2 j + 1.
After each such injection, the attacker then injects again the challenge R 0 , AUTN 0 provoking a synchronization failure containing some AUTS j = ⟨c * j , MAC * j ⟩ where:

c j = (SQN 0 HN + 2 j + 1) ⊕ f5 * (R 0 , K IMSI ).

Inference Algorithm

We now describe algo(⋅) that takes the n + 2 fetched AUTS's messages (i.e., c ′ , c j for 0 ≤ j ≤ n) as inputs and outputs the n least significant bits of

1 + SQN 0 HN . Recall that c ′ = (1 + SQN 0 HN ) ⊕ f5 * (R 0 , K IMSI ) and c j = (1 + SQN 0 HN + 2 j ) ⊕ f5 * (R 0 , K IMSI ).
Therefore, for any 0 ≤ j ≤ n, it holds that:

c ′ ⊕ c j = (1 + SQN 0 HN ) ⊕ (2 j + 1 + SQN 0 HN ).
We note δ i the quantity c ′ ⊕ c i . One has that

δ i = (2 i + X) ⊕ X for all 0 ≤ i ≤ n where X = 1 + SQN 0

HN

is the quantity we seek to infer the n least significant bits of. In a nutshell, the idea of the algorithm consists in analyzing how remainders propagate in (2 i +X) at bit position i and i + 1 (in little-endian notation) by looking at δ i . Considering X and δ i as arrays of 48 bits in little-endian, we describe the algorithm in Algorithm 1 that, given the δ i 's, infers n bits of X. Note that this algorithm can be executed completely offline on the collected data.

Improving the Attack Under Stronger Threat Model

When the targeted UE stays a long time in the attack area or intensely consumes mobile services (triggering a lot of AKA authentication sessions), the attacker has a simpler way to break the confidentiality of SQN. This

Data: δ i = (2 i + X) ⊕ X for 0 ≤ i ≤ n (in little-endian), n < 48 Result: Res: n least significant bits of X (in little-endian) Res ← [0, 0, . . . , 0] //size n for i from 0 to n -1 do //Let's analyze δ i at bit positions i, i + 1 (b 1 , b 2 ) ← (δ i [i], δ i [i + 1]) if (b 1 , b 2 ) == (1, 0) then //no remainder propagate when +2 i to X Res[i] ← 0 elif (b 1 , b 2 ) == (1, 1) then //a remainder propagates when +2 i to X Res[i] ← 1 else //cannot happen Error end return (Res)
Algorithm 1: SQN Inference Algorithm kind of scenarios are realistic when the attack areas are e.g., offices where targeted UEs stay most of the day but expect to be safe when being outside attack areas (e.g., at home).

Essentially, instead of fetching the challenges R i , AUTN i and injecting the challenges that are accepted by the UE (i.e., R 0 , AUTN 0 and then R 2 j , AUTN 2 j for 0 ≤ j ≤ n), the attacker can let the UE attaches to any genuine SN and let it receives challenges and completes the AKA sessions. The attacker just passively eavesdrops on the exchanged messages, notably the challenges, and counts the number of successful authentications. However, the attacker still needs to (actively) replay the challenge R 0 , AUTN 0 at appropriate times; more precisely, after the UE received the genuine challenge (R 0 , AUTN 0 ) and then challenges (R 2 j , AUTN 2 j ) for 0 ≤ j ≤ n. This variant is far less costly: it only requires passive attacking capabilities and n + 2 additional (active) injections.

Variants for Other SQN Policies

According to non-normative parts of the specification [START_REF]3G security; Security architecture[END_REF]), SQN and its update policy can take different forms. We briefly explain how our attack can be easily adapted for those variants. We refer to Appendix C for more details.

SQN can be composed of two components SQN = SEQ IND where SEQ is a 43 bits long integer that for i = 0 to 2 n :

Auth_Req, R0, AUTN0 Auth_Resp,RES0 Auth_Req, R0, AUTN0 Sync_Failure, AUTS ′ Auth_Req, R 2 j , AUTN 2 j Auth_Resp,RESj Auth_Req, R0, AUTN0
Sync_Failure, AUTSj for j = 0 to n: counts all past AKA sessions and IND is a 5 bits long index that describes the SN for which the given SEQ is valid. When such a policy is in use, one can use a slightly different variant of our attack: (i) injections of authentication challenges should be done while using the same SN identifier towards the UE and the same SN while fetching authentication tokens, and (ii) the algorithm used to infer bits should drop the 5 bits of SQN corresponding to IND. This allows the attacker to break the counter part of SQN, namely SEQ; leading to the same privacy attacks explained in the next section.

[1 + SQN 0 HN ] n ← algo(AUTS ′ , {AUTSj }0≤j≤n)

Attacks on Privacy

We now explain how one can leverage the attack presented in Section 3 to break subscribers' privacy by conducting an activity monitoring attack. As explained in Section 2.4, this new class of attacks allows an attacker to monitor targeted subscribers' activity, even for periods where subscribers escape the attack area (see Figure 2b).

In a nutshell, the attacker needs to conduct the previously described attack when targeted subscribers are in the attack area, thereby learning n significant bits of SQN at different times t 1 , t 2 , . . . We explain in Section 4.1 how the attacker can then relate this information to the number of AKA sessions subscribers have made between times t 1 , t 2 , . . .. Next, we show how the attacker can relate the number of AKA sessions some UE has performed in a given period of time to its typical service consumption during that period.

Therefore, the attacker learns the typical service consumption of targeted subscribers between times t 1 , t 2 , . . . even if such subscribers escape the attack area most of the time (i.e., in between times t i ). Please refer to Section 5 for practical aspects of the attack (e.g., number of bits of SQN that can be inferred). We illustrate this new threat by giving some illustrations of practical attack scenarios (Section 4.2). We conclude in Section 4.3 with a variant of our attack that could yield location attacks in a variant of AKA that fix previously known privacy attacks which is notably relevant in the context of the in-progress standardization of 5G AKA, phase 2.

Relating SQN Increases to Activity Patterns

We first need to learn the value that is added to SQN after each successful authentication. The conclusion of our practical investigations (see Section 5) is that this value is 1 for all tested operators. This value is needed because equal differences of SQN could be resulted by different operations: if the victim SQN had been increased by 20, it could be the result of either 4 increases of 5 (4 authentications) or 2 increases of 10 (2 authentications). We found how much SQN is increasing upon authentication for several operators by running the algorithm algo() for several values of the increment and keeping the value yielding no Error (see Algorithm 1). We stress that this has to be done just once for or a given operator.

Next, in order to relate information about the number of AKA sessions of a victim with the victim's activity, we have to exploit the fixed authentication policies discussed in Section 5.2 (i.e., which user's activities trigger an authentication and thus an AKA session). Because of the different operator configurations, authentication may or may not happen on each SN network attach, call or reception/sending of SMSs. As a result, we also analyzed how frequently authentication is performed by analyzing signaling messages during repeated attach procedure (by calling or sending SMSs). We found that there are little variations in authentication frequency among operators but for most of them, an authentication was required for each outgoing call and sent SMS). Despite those variations, one can easily infer the fixed policy for some operator, once for all, by inspecting signaling messages e.g., on her own phone.

We leave as future work the task of doing a comprehensive review of existing policies.

Examples of Practical Scenarios

We now illustrate the potential real-life impacts of our activity monitoring attack with two practical scenarios. Spying on embassy officials, journalists, or any high-value target. Assuming an adversary having a fake base station near an embassy, he can learn the officials' activity not only when they are at the office during working hours, but also when they are not, including during evenings and nights (e.g., at home) or during business trips. Therefore, such an attacker may learn if targets use different SIMs cards for private use (no activity at home), if some specific time periods (e.g., one evening and night) were specifically busy (a lot of calls or SMSs were made yielding a big rise of SQN), if one is using his work phone at home, if a phone was switched off for certain time periods or trips (possibly indicating multiple SIMs usage), etc. Better ads targeting. Consider for instance a shop that is willing to know more about its customers (e.g., for improving ads targeting) using fake base stations. This kind of scenario has already been reported [START_REF] Musa | Tracking unmodified smartphones using Wi-Fi monitors[END_REF] (using Wi-Fi capabilities of smartphones) and exploited [START_REF] Clifford | Attention Shoppers: Store is Tracking Your Cell[END_REF] in real shops. Our attack causes a new threat in that context since it leaks to the shop typical customers' mobile consumption during time periods between customers' visit (while they escape the attack area).

Deriving Location Attacks

Using variants of our attack, one could mount location attacks (i.e., inferring if some targeted UE is in some physical area) even if the leak of identity (currently enabling IMSI-catchers attacks) and the traceability based on failure messages were fixed.

More precisely, we first assume that the identity request phase would be well-protected using e.g., encryption (as done in 5G, phase 1 [START_REF] Gpp | Security architecture and procedures for 5G System[END_REF]). Second, we assume that the two failure cases (MAC or freshness failure) would be merged (AUTS message is also sent out in case of MAC failure, the network being able to infer the reason of the failure) to address the aforementioned known flaw. Under those assumptions, to the best of our knowledge, there is no known attack that could break subscribers' privacy. However, either of the two following variants of our attack still allows an active adversary to perform location attacks 2 .

First, if an attacker knows a value CONC 0 of some targeted UE 0 and obtains a value CONC from some unknown UE (this can be easily obtained by replaying a genuine challenge), then he can infer if the unknown UE is UE 0 with very high probability by inspecting how large is CONC 0 ⊕ CONC, interpreted as an integer. Indeed, when both UEs do not match then CONC 0 ⊕ CONC = (SQN UE0 ⊕ AK * 0 ) ⊕ (SQN ′ UE ? ⊕ AK * ? ) (where AK * ? ≠ AK * 0 ; see Section 3.1) which is a 48-bits randomlooking value. By contrast, when they do match, then CONC 0 ⊕ CONC = SQN UE0 ⊕ SQN ′ UE0 which is very likely a small value (we never observed more than 10 bits-values). We stress that this can be done even when the SQN values of different UEs are close to each other or even equal. E.g., if Alice and Bob both have the same SQN , the attacker will still be able to locate Alice later on and distinguish her from Bob.

Second, by learning sufficiently many bits of some targeted UE, an active attacker will be able to track this UE with reasonable probability by keeping track of the SQN values he may repeatedly learn (recall that SQNs are 48-bits long so they almost injectively identify UEs even taking into account the fact that they evolve). Obviously, the practicality of this second attack heavily depends on the number of bits one can infer, closeness of SQNs between different UEs, the frequency at which the target visits the attack area, and the speed at which the target's SQN rises.

We consider those location attacks as potential threats for the upcoming 5G, phase 2 that may address previous flaws but not necessarily this new attack.

Proof of Concept of the Attack and Practical Considerations

In this section, we show how to conduct our attacks in practice on 4G networks using a low-cost and easily available setup. We then explain practical aspects which make our attack easily feasible (e.g., issues in different operator's network and security configurations). We finally discuss our PoC and our experimental results.

Feasibility in 5G.

Due to unavailability of 5G devices and networks, we only demonstrate our attack in a 4G environment. As already mentioned, we know that the 5G, phase 1 specification already suffers from our attacks. Moreover, we believe that it will be feasible to demonstrate our attack against real 5G networks soon due to the fast open source developments for 5G [START_REF] Gcore | Open5GCore -The Next Mobile Core Network Testbed Platform[END_REF]. For example, 2G has been launched in 1991 but the first open source software were only made available in 2010 (with OpenBTS [START_REF] Venturebeat | DEMO: Range Networks rings in cell-phone service for USD 2 a month[END_REF]). In contrast, 4G has been launched in 2009 [START_REF]TeliaSonera launches world's first commercial LTE networks in Sweden and Norway[END_REF] and open source 4G software was already supported the same year by OpenAirInterface [START_REF]History[END_REF].

Experimental Setup

The first experimental setup aims at building a platform to collect the victim's authentication challenges. Further, we modify and build software tools to make victim's UE to attach to a rogue 4G base station so that one can inject legitimate radio layer signaling messages. Our hardware setup is depicted in Figure 4 which consists of a laptop, a Universal Software Radio Peripheral (USRP) B210 [START_REF]USRP B210[END_REF], and a PC/SC [START_REF]PC/SC Workgroup Specifications[END_REF] capable smartcard reader (we used ACS ACR38 [START_REF]ACR38 Smart Card Reader[END_REF]) with commercial USIM cards.

Our complete experimental setup costs about 1140e excluding a laptop price (that could be replaced by a cheaper Raspberry pi) -1120e for USRP, 20e for commercial operator's prepaid USIM cards.

Attacker's Setups

We now explain how hardware and software components can be combined into different setups to demonstrate our attack.

Obtaining authentication challenges. We used the software srsUE from the srsLTE suite [START_REF] Gomez-Miguelez | srsLTE: An Open-Source Platform for LTE Evolution and Experimentation[END_REF] configured with the target's IMSI with the USRP B210 for obtaining authentication challenges. Essentially, the USRP B210 tries to impersonate the target's USIM. When doing so, each session fails because srsUE does not know the target's secret key K (so it cannot compute the appropriate RES) but, before the failure, we obtain a new, genuine authentication challenge that is intended for the target's USIM. We were able to fetch authentication tokens using the USRP at a surprisingly high speed (see discussion later) but, if for some reason, a network recognizes the USRP as a fake smartphone, we can still use genuine phones with programmable [START_REF] Sysmocom | sysmoUSIM-SJS1[END_REF] USIM cards (ca. 80e). We describe this alternative setup in Appendix D.

Fetching AUTS messages using rogue base station. Utilizing OpenLTE [START_REF] Wojtowicz | OpenLTE[END_REF] based 4G network running on an USRP B210, we sniff over-the-air signaling messages and masquerade as a real base station. We configure a rogue base station to mimic a real operator to lure victim's UE to attach by 4G reselection procedure [START_REF] Shaik | Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems[END_REF]. The base station is then able to inject messages and eavesdrop on replied messages. We use this method to fetch AUTS messages that a USIM sends as part of the AKA protocol.

Ethical Considerations

Our research reveals weaknesses in the AKA protocol specification which is implemented in every USIM installed in 3G and 4G devices worldwide. We reported our findings to relevant standardization bodies 3GPP [START_REF]SA3 -Security[END_REF] and GSMA, and affected network operators. Our results were acknowledged by the involved parties.

We conducted passive attacks only against test USIM cards and smartphones. We operated our rogue 4G base station inside a Faraday cage [START_REF] Instrumens | Faraday Cage: What Is It? How Does It Work[END_REF], to comply with legal requirements.

Attack Background

Before explaining our PoC, we report on our investigation on AKA related security configurations of 4G networks which make our attack easier to perform. We selected several major European 4G operators including three German, three Austrian, two French, and one Swiss operators.

We were successfully able to collect authentication challenges intended for the targeted USIM at any moment for any subscriber in the world. Note that to achieve this step, the attacker only needs to know the IMSI (or any temporary or encrypted identity) of that particular victim's USIM. If the attacker knows the subscriber's mobile phone number, he can perform HLR Lookup attacks [START_REF] Engel | Locating Mobile Phones using Signalling System 7[END_REF] to learn victim's IMSI. The previous work [START_REF] Shaik | Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems[END_REF] also demonstrates how to find IMSI and GUTI of the targeted victim by knowing the mobile phone number or social identities such as email, Facebook and Twitter. Based on the data collected from our experiments, we studied the following parameters of the operator's 4G networks. We stress that there is no need to learn more information (e.g., private key K IMSI ) about the targeted USIM).

We found that most operators allowed to fetch authentication challenges without a rate limit. Using our first setup using srsUE, we were able to fetch fresh, unused authentication challenges consecutively at the speed of 1 per second. Using our second setup involving a smartphone, we were able to fetch more than 30 challenges in less than 10 minutes. We expect a setup based on multiple rogue base stations to achieve much better performance.

Background in 5G. Since no 5G deployment has been completed yet, we could not conduct a full PoC in 5G. We emphasize however that, if no dedicated mitigation is implemented, the different steps of our attack could be performed in 5G as well. The only major difference concerns the way we would fetch authentication challenges. To do so, we do not have to learn SUPI (the subscribers' identifier in 5G that is supposed to remain secret) but only a valid SUCI. Since SUCI is sent in the clear by subscribers, the attacker just has to eavesdrop on one SUCI and can from then on, fetch as many authentication tokens for that subscriber he wants (using SUCI instead of IMSI). The rest of the attack remains the same for 5G infrastructure.

Proof of Concept

Upon knowing the victim's identity and location [START_REF] Shaik | Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems[END_REF], an attacker can perform our subscriber activity monitoring attack. This attack requires obtaining a larger number of authentication challenges of victim's USIM. But as discussed in Section 5.2, we did not observe any countermeasure preventing us to fetch a large amount of them.

Exploiting our attack, the more consecutive challenges one fetches, the more is the number of bits he can infer from the SQN of the victim. Then, using a rogue base station, the attacker is then able to inject parts of those challenges and store replied AUTS as explained in Section 5.2.

We build a modest setup as a proof of concept of our attack. We were able to request 1025 authentication challenges and collected 12 AUTS from 24 injections of AKA messages. Using our generic SQN inference algorithm, those 12 AUTS messages were enough to infer at least 10 bits of SQN (the least significant ones), sometimes more 3 . Obviously, an attacker with greater capabilities and more elaborate setups (notably multiple rogue base stations for fetching challenges; which turns out to be the bottleneck) could infer more bits.

Attacks Feasibility and Amplifications

We now describe the feasibility of our subscriber activity monitoring attacks against commercially deployed 4G devices. Further, we discuss possibilities of extending the coverage range of the USRP device.

Impacted devices. The AKA protocol vulnerability we found is part of the 3GPP specifications and does not rely on implementation issues in 4G/3G devices. In fact, the affected AKA protocol is implemented in the USIM and not in the baseband OS of devices. Thus, any 3G/4G device deployed worldwide having active USIM card is affected by our attacks. For our investigations, we selected prepaid USIM cards of few leading cellular operators. We collected and stored unused authentication challenges of related USIM cards as described before. Then we successfully verified that these USIM cards were vulnerable to our attack. As mentioned earlier about feasibility in 5G networks, if no dedicated mechanism for mitigating our attack is implemented, 5G devices will also suffer from our attack.

Range of the attack. Previous research suggested that the coverage radius of a rogue base station using USRP B210 and OpenLTE ranges between 50 and 100 meters [START_REF] Shaik | Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems[END_REF], without external hardware to boost the signal. The coverage range of our attacks could be increased to locate and inject radio layer messages to a 4G device equipped with USIM within a 2 km 2 area as discussed in [START_REF] Shaik | Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems[END_REF]. Detection. We also investigated possible methods for the end subscribers to detect our attack. Unfortunately, our attacks cannot be detected by the mobile OS (e.g., Android or iOS). The reason is that the AKA protocol is executed in USIM and the baseband chip that communicates limited information to the mobile OS.

Security Analysis and Lessons Learned

In this section, we discuss the AKA specification issues and their impact on 3G/4G/5G security principles. First, we describe AKA protocol design choices and discuss the trade-off considerations related to security, availability, and cost which partly are responsible for our attacks. The following analysis is based on the data and practical experiments in 3G/4G networks. Finally, we draw conclusions and summarize lessons learned that may be relevant for the in-progress standardization of 5G, phase 2.

Choice of symmetric key encryption. We demonstrated (Section 5) how a low cost setup allows an attacker to fetch unused challenges (R, AUTN ) of any active 4G subscriber in the world from any network. We now explain the AKA protocol design choice of authentication method and trade-offs responsible for enabling access to R and AUTN ). The AKA is a challengeresponse type of protocol and utilizes symmetric encryption based authentication mechanism. We believe that the reason for choosing symmetric encryption stems from three trade-offs.

The first is a trade-off between security and cost, i.e., High cost of introducing a Public Key Infrastructure into the 3G/4G systems and asymmetric encryption mechanism in USIM, paves the way for choosing symmetric encryption based authentication technique. Due to this high cost, the 3GPP designers were limited in the previous 3G and 4G networks, however, PKI is introduced in 5G, only for protecting identities [START_REF] Gpp | Security architecture and procedures for 5G System[END_REF]. Note that, authentication in 5G, excluding identification, is still based on a symmetric cryptography.

The second is a trade-off between security and network availabilityi.e., Use of symmetric key avoids a risk of shutting down legitimate subscribers during a case of network fail or crash [START_REF] Forsberg | LTE Security[END_REF]. For example, if the SN (in particular MME) software crashes, the temporary identity of a subscriber can not be recognized. In such a case, the network needs to request the permanent identity from the subscriber.

The third is a trade-off between privacy and network efficiency -The AKA is a one round-trip authentication protocol; i.e., only two exchanged messages are needed to establish mutual authentication, after identification. The chosen mechanism to achieve mutual authentication with only two exchanged messages is the synchronized SQN . Allowing the UEs to generate a random number could have enabled different authentication methods. Meanwhile, in the year 2000 (when 3G AKA was designed), UE's computational resources were limited. With three exchanged messages, the protocol would not need this synchronized state and this additional message exchange could have enhanced privacy. However, this additional message exchange would also negatively impact the network efficiency, notably because it would always require a message exchange between the HN and the SN as well [START_REF] Forsberg | LTE Security[END_REF].

The above trade-offs force the network to send R and AUTN to perform a round of challenge-response for the authentication of a subscriber's temporary or permanent identities. This allows an attacker to impersonate a subscriber's identity to fetch unlimited R and AUTN challenges from any network. One reason why an attacker can fetch those challenges of any subscriber from any network is the trust between the SNs and the HNs. Indeed, in 3G and 4G architectures, the HN and SN trust each other due to roaming agreements. Further, such illegitimate requests are difficult to filter out from the legitimate ones due to the risk of shutting down real subscribers from accessing the network. One potential solution is to rate limit (based on time or numbers) authentication requests per subscriber, however, an attacker could learn such kind of rate limit by simply testing the network. We found that one of the operators is implementing the rate limit of 3 consecutive failures. Moreover, an attacker could bypass this countermeasure by requesting authentications challenges from different SNs.

Replay protection measures.

The AKA protocol uses SQN as a challenge to prevent replay attacks and synchronized state between the UE and the HN . This SQN challenge and the synchronization method prevent replay attacks. The UE verifies if a challenge (AUTN ) is fresh or replayed. In case of network failure, legitimate authentication challenges may get lost resulting to the HN and subscriber being de-synchronized. In order to re-synchronize, the protocol uses the AUTS message which contains the current SQN UE of USIM XORed with the anonymity key (AK * ). However, this message SQN UE ⊕ AK * contained in AUTS lacks randomness due to the fact that the key AK * derives from the same R value as discussed in Section 3.1. Our attack from Section 3.1 indicates a lack of replay protection for AUTS, like the one existing for AUTN.

Lessons for 5G. 5G phase 1 security has been released by the 3GPP including an enhanced AKA protocol featuring HN 's public keys to provide subscriber identifiers privacy [START_REF] Anand | 3GPP 5G Security[END_REF]. However, our attacks reveal another threat to the subscriber's privacy. In the future, clever and sophisticated attackers may find new ways to use every obtainable information to carry out further AKA protocol related attacks in 5G networks. Hence, it is important to protect the sequence numbers used in authentication procedure messages.

Though the first phase of 5G security is completed, we suggest that all security protocols in 5G shall go through formal verification before releasing phase 2 (some first steps have been taken in [START_REF] Basin | A Formal Analysis of 5G Authentication[END_REF] and in this paper). More generally, authors of [START_REF] Basin | Improving the Security of Cryptographic Protocol Standards[END_REF] provide some industrial case studies (WiMAX, EAP, and ISO/IEC 9798) and discuss how formal methods and associated security tools could be integrated into the standardization process.

Countermeasures

As already explained, the main attack vector we exploit in our attacks is the use of XOR and the lack of randomness in AUTS making the concealing of SQN by AK * inefficient. We propose three main countermeasures F1, F2, and F3 to solve this problem. We also discuss how our fixes also provide an opportunity to fix the known linkability attack based on failure messages discussed in Section 2.3. We conclude by a formal analysis of our fixes using the state-of-the-art Tamarin automated prover.

Note that, when discussing our countermeasures, we also consider practical aspects related to the existing and next-generation cellular networks. Thus, the following fix we propose is easy to deploy in the current cellular system and only requires changes in baseband and authentication server software in the HSS. Other two fixes F2 and F3 in appendices E.1 and E.2 are suitable for next-generation networks since they require additional modifications in deployed hardware (e.g., USIM).

Symmetrically Encrypt SQN UE

Our simplest fix consists in modifying the concealing mechanism: instead of using XOR (having algebraic relations enabling to cancel out AK * ), USIM may use symmetric encryption. Note that current USIMs and the HSS (in particular AuC) are already capable of symmetric encryption. The symmetric key to encrypt SQN UE could be derived from the key K IMSI and R in the received authentication challenge. The resulting fix is depicted in Figure 5. This can be very easily adapted to fix the linkability of failure messages (see Section 2.3) as well. It suffices to hide the failure reason inside the ciphertext CONC * as follows:

CONC * ← enc(⟨Reason_Failure, SQN UE ⟩, CK *
). The HN is required to decipher the CONC * in order to learn the reason of the UE's authentication failure. However, this mechanism could add extra processing load on the HN due to the decryption requirement. Alternatively, such a processing load of the HN could be offloaded to the SN by transmitting decryption key in a set of authentication vectors. Finally, note that this

Formal Verification

We have presented a new attack breaking the confidentiality of SQN, its impact on subscribers' privacy and possible fixes to address this issue. A natural goal is then to evaluate those fixes. While all our fixes intuitively remove the attack vector on which our attack is based, we believe that an informal argument or even a pen and paper proof would not provide enough confidence considering the complexity and size of the AKA protocol. We actually advocate for the use of formal methods providing rigorous, mathematical frameworks and techniques to analyze security protocols.

Related Work. Such techniques have already been leveraged in the past (notably by 3GPP) to formally verify the AKA protocol to some extent (e.g., formal analysis in enhanced BAN Logic and TLA [START_REF] Gpp | 3G Security; Formal Analysis of the 3G Authentication Protocol[END_REF], in the tool ProVerif [START_REF] Arapinis | New privacy issues in mobile telephony: fix and verification[END_REF][START_REF] O'hanlon | Mobile subscriber WiFi privacy[END_REF]). More recently, an in-depth formal analysis of 5G AKA [START_REF] Basin | A Formal Analysis of 5G Authentication[END_REF] has been conducted using the tool Tamarin [START_REF] Meier | The Tamarin Prover for the Symbolic Analysis of Security Protocols[END_REF]. However, all those analyses failed to capture our attack4 because those prior modelings abstracted the protocol too much. For instance, except for [START_REF] Basin | A Formal Analysis of 5G Authentication[END_REF], they do not model the re-synchronization procedure at all, which is at the core of our attack; while [START_REF] Basin | A Formal Analysis of 5G Authentication[END_REF] focuses on authentication properties and only models a specific scenario for privacy in order to capture a location privacy attack.

Challenges. We now focus on formal verification in the symbolic model which provides a high-level of automation. The limitations of prior analyses can be explained by the fact that the AKA protocol and its features cause several difficulties to the state-of-the-art tools and methods (such as ProVerif [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF] and Tamarin [START_REF] Meier | The Tamarin Prover for the Symbolic Analysis of Security Protocols[END_REF]): (i) the modeling of the ⊕ operator that most tools cannot handle at all, (ii) the presence of a (non-monotonous state) state (i.e., SQN whose value must be stored from one session to the other), and (iii) basic arithmetic (i.e., SQN is basically an integer and integer additions and comparisons are carried out by the USIM). Each one of those features constitutes a major challenge to existing techniques. Finally, location privacy or untraceability, as defined e.g., in [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF], is not a reachability property but an observational equivalence-based property that is notoriously more difficult to verify (see the survey [START_REF] Delaune | A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols[END_REF]).

For an unbounded number of sessions, the only tools that can verify some sort of observational equivalence are ProVerif and Tamarin. The approximations those tools adopt (due to the fact that the underlying problem is undecidable) make the verification less precise and often lead to false attacks when verifying untraceability; despite recent research efforts [START_REF] Cheval | Proving more observational equivalences with ProVerif[END_REF][START_REF] Hirschi | A method for verifying privacy-type properties: the unbounded case[END_REF].

Our Formal Analysis. We took a first step towards a precise formal analysis of privacy for the AKA protocol in the symbolic model. We leveraged the state-of-theart tool Tamarin [START_REF] Meier | The Tamarin Prover for the Symbolic Analysis of Security Protocols[END_REF] and built upon [START_REF] Basin | A Formal Analysis of 5G Authentication[END_REF] in order to provide a symbolic model of the AKA protocol that is precise enough to capture our attack. Our models are available at [START_REF]Tamarin tool code[END_REF]. We took the re-synchronization procedure into account and used the new feature [START_REF] Dreier | Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR[END_REF] to precisely model the ⊕ operator. Note also that Tamarin is capable of modeling stateful protocols, so we were able to precisely model SQN . We modeled the AKA protocol without the fix as well as with the three fixes. We were not able to faithfully analyze the confidentiality of the SQN value as this would require to model algebraic relations of ⊕ on integers; this is one of the reason explaining that [START_REF] Basin | A Formal Analysis of 5G Authentication[END_REF] missed our attack. However, for two sessions, we were able to analyze the confidentiality of δ 0 = SQN ⊕ (SQN + 1) which is one of the values needed to bootstrap our attack. In our model, the confidentiality of δ 0 was automatically proven for all our fixes and our attack breaking this property was automatically found without our fix. We consider this analysis as a first step towards a more precise model amenable to automatic verification of privacy-related properties which has proven itself extremely complex to produce. We leave that task as future work.

In summary, the state of the art of mechanized formal verification does not provide an off-the-shelf technique to verify privacy-related properties on the AKA protocol with sufficient precision. Considering the importance and ubiquity of the AKA protocol, we think that formally verifying it and solve the aforementioned challenges in order to provide a precise symbolic model of the AKA protocol and its variants is a substantial but major goal.

Conclusion

We disclose a subtle vulnerability in the AKA protocol affecting the 3G, 4G, and upcoming 5G technologies. We demonstrate how this vulnerability can be exploited to mount activity monitoring attacks, allowing the attackers to learn a new type of privacy-sensitive information about the subscribers; i.e., consumption patterns. As a proof-of-concept, we show how an active attacker equipped with a low cost and widely available setup can perform our attack in several European 4G networks, learning SQN with granularity 2 10 . We then analyze the root causes of the vulnerability and their impact on 3G/4G/5G security principles to derive lessons for future 3GPP standardization; notably 5G, phase 2. Finally, we provide countermeasures and formal guarantees that also motivate further research into improving and formally analyzing the AKA protocol. While our attack undeniably introduces a new threat on mobile subscribers privacy, we leave a comprehensive evaluation of the privacy impact in practice as future work. [START_REF]3G security; Security architecture[END_REF]). When such a policy is in use, one can use a slightly different variant of our attack: (i) injections of authentication challenges should be done while using the same SN identifier towards the UE and the same SN while fetching authentication tokens, and, (ii) the algorithm used to infer bits should drop the first 5 bits of SQN. This allows the attacker to break the counterpart of SQN, namely SEQ; leading to the same privacy attacks explained in Section 4. Indeed, SEQ is not useful for the practical attacks we describe in Section 4, only the integer counting the number of successful AKA sessions is relevant; here SEQ. Note however that it seems that IND is actually highly predictable. For example, two SQN in two AUTN vectors that were requested by the SN are expected to use the same IND value. Note that there are other policies, for example SQN can also be time-based. For such policies for which SQN does not contain any information about the number of successful AKA session made by the UE, our attack no longer works. However, we have not observed any operator using such policies.

D Attacker's Setup: Using

Reprogrammable USIM

In addition to the setup described in Section 5.1.1, we have shown that one case uses genuine smartphones with reprogrammable USIM for fetching a large number of authentication tokens intended for the target's USIM.

We used a tool pySIM [START_REF]pySIM: A python tool to program magic SIMs[END_REF] to program USIM cards using an external smartcard reader. While programming commercial USIM cards are not possible, Sys-moUSIM [START_REF] Sysmocom | sysmoUSIM-SJS1[END_REF] cards can be reprogrammed to store any given IMSI.

We inserted the programmed USIM in a smartphone to read all the traffic (i.e., signaling messages) as explained next. Having access to signaling messages, we stored the received authentication challenges (R and AUTN ) sent by the networks intended for the targeted USIM. We used the SCat tool [START_REF]SCAT: Signaling Collection and Analysis Tool[END_REF] to gain access to signaling messages We selected Android-based Huawei and Asus smartphone models due to the availability of direct access to baseband using AT commands [START_REF] Gpp | AT command set for User Equipment (UE)[END_REF] to store signaling messages automatically.

E Countermeasures E.1 Correctly Randomize AUTS (F2)

One way to fix the attack vector we have discovered consists in using a fresh random number generated by UE to conceal SQN UE instead of reusing the one contained in the received authentication challenge (generated by the HN ). This random has to be sent in the clear along with AUTS in order to let the HN computes AK * and recovers SQN UE . We depict this solution in Figure 7. Note that the value MAC * must use R instead of R * so that it really plays the role of a response to the fresh challenge corresponding the received authentication challenge. Otherwise, a rogue UE could impersonate a UE by replying one of its old AUTS vector forcing the HN to synchronize SQN to an older value.

With this fix, replaying two times the same authentication challenge leads to two AUTS vectors whose concealed values are c 1 = (SQN UE ) t1 ⊕ f5 * (R * 1 , K IMSI ) and c 2 = (SQN UE ) t2 ⊕ f5 * (R * 2 , K IMSI ). More importantly, when xoring c 1 and c 2 , the two AK * values do not cancel out breaking the relations exploited by our attacks. Note that this fix can be implemented in combination with the fix for the linkability of failure messages described in Section 7.1.

However, this solution still suffers from the following minor flaw. When replaying two times the same authentication challenge, even though the two concealed values in the two replies are different as argued above, the two MAC * from the two replies may be equal (i.e., when SQN UE has not been modified between the two replays). The attacker may exploit such equality to link a subscriber although we believe that the underlying attack is much less severe than our attacks. In order to solve this issue, one may mix R and R * in the replied MAC * message as follows:

MAC * ← f1(⟨SQN UE , R, R * ⟩, K IMSI ).

E.2 Asymmetrically Encrypt SQN UE (F3)

Although the use of asymmetric encryption methods was considered too costly and impractical during the 4G system design, it is now known that 5G will rely on it. A fix based on asymmetric encryption, similar to the one presented in [START_REF] Arapinis | New privacy issues in mobile telephony: fix and verification[END_REF], is depicted in Figure 8. Similarly to the fix F1, it can be adapted to hide the reason for the failure and can be improved using a random generated by the UE.

IfFig. 1 .

 1 Fig. 1. The AKA protocol. K denotes K IMSI .

  When the UE is in the attack area, it was known that it may be subject to tracking, location attack, and monitoring attacks.

Fig. 3 .

 3 Fig. 3. Sequence Number Inference Attack (where SQN 0 HN is the initial SQN for IMSI stored in the HN and [X] n denotes the n least significant bits of X).

Fig. 4 .

 4 Fig. 4. Our experimental setup, showing a smartcard reader, USRP (left), set of commercial USIM cards, and a test phone.

  t. K IMSI , replies Mac_failure if it is not the case; (ii) the authentication request is fresh (i.e. xSQN HN > SQN UE and xSQN HN < SQN UE + ∆), replies Sync_failure, AUTS otherwise (AUTS is explained next). The quantity ∆ is a threshold that is fixed according to an availability vs. security trade-off. If all checks hold then the UE computes the ciphering key CK and the integrity key IK and stores them to secure subsequent messages. It also computes the authentication response RES and sends it to the SN using Authentication Response message. Only RES is included in the message, other computed values like CK and IK are not transmitted. The SN authenticates the UE by verifying whether the received response matches with xRES. If so, the AKA protocol is successfully completed and subsequent communications can be secured using the secret keys IK and CK.

	Re-synchronization procedure. In case of a synchro-
	nization failure (case (i) and ¬(ii)), the UE replies
	with Sync_failure, AUTS. The AUTS message's pur-
	pose is to allow the HN to re-synchronize with the UE
	by replacing its own SQN HN by the sequence number of
	the UE (i.e., SQN UE + 1). For reasons explained above,
	SQN UE is concealed: CONC *	= SQN UE ⊕ AK * where
	AK *	= f5 *	(R, K IMSI ). Finally, AUTS = CONC * , MAC *
	where MAC *	= f1 *	(K IMSI , (SQN UE , R) allowing the
	HN to authenticate this message as coming from the
	intended UE.

k

  IMSI , IMSI, SQN UE

	User Equipment -UE	Attacker	Network (SN + HN )
		ID	K IMSI , IMSI, SQN 0 HN
		ID
		Ri, [...], AUTNi
			[...]
		SQN HN ← SQN HN + 1 = SQN 0 HN + (i + 1)

k

  IMSI , IMSI, SQN UEUser Equipment -UE Serving Network -SN Fix F1: Fix by symmetrically encrypting SQN UE solution suffers from a minor flaw: when the attacker triggers two times a synchronization failure by injecting the same authentication challenge while SQN UE has not changed, then the two replied CONC * will be equal, leaking to the attacker the information that SQN UE is still the same (we consider such an attack impractical though; more details in Appendix E.1).

	If (i) and ¬(ii)
	MAC *	← f1(⟨xSQN UE , R⟩, K IMSI )
	CK *	← f3(R, K IMSI )
	CONC *	← enc(SQN UE , CK *	)
	AUTS ← ⟨CONC * , MAC *	⟩
				Sync_Failure, AUTS
	Fig. 5.

Table 1 .

 1 Informal correspondence between terminologies counts all past AKA sessions and IND is a 5 bits long index. Essentially, IND indicates the SN for which SEQ should be used and the USIM stores possibly other SEQ corresponding to other SNs (this is called array mechanism in the specification

	Our acronym	In 3G	In 4G	In 5G	Description (if needed)
	IMSI	IMSI	IMSI	SUPI	International Mobile Subscriber Identity
	UE/Subscriber	MS	UE	UE	User Equipment (contains a USIM)
	SN	VLR+SGSN+...	eNodeB+MME+...	SEAF+AMF+gNB+...	Serving Network
	HN	HE+HLR+...	HSS+HLR+AuC+... AUSF+ARPF+UDM+SIDF+... Home Network

k

  IMSI , IMSI, SQN UE , ∆ IMSI ) CONC * ← SQN UE ⊕ AK * AUTS ← ⟨R * , CONC * , MAC * ⟩

				UE	SN
	If (i) and ¬(ii)
	new R *
	MAC *	← f1(⟨SQN UE , R⟩, K IMSI )
	AK *	← f5 *	(R Sync_Failure, AUTS
	Fig. 7. Fix F2: correctly randomizing AUTS

* , K

  ← f1(⟨SQN UE , R⟩, K IMSI ) CONC * ← aenc(SQN UE , pk O ) AUTS ← ⟨CONC * , MAC * ⟩

	If (i) and ¬(ii)
	Sync_Failure, AUTS

K IMSI , IMSI, pk O , SQN U E , ∆ UE pk O , sk O SN + HN MAC *

Fig. 8. Fix F3: asymmetrically encrypting SQN UE

Even though the specifications are not clear about the requirements of those functions[START_REF] Gpp | Security architecture and procedures for 5G System[END_REF][START_REF]3G security; Security architecture[END_REF][START_REF]3GPP System Architecture Evolution (SAE); Security architecture[END_REF], Milenage[START_REF] Gpp | 3G Security; Specification of the MILENAGE algorithm set: An example algorithm set for the 3GPP authentication and key generation functions f1, f1*, f2, f3, f4[END_REF] and TUAK[START_REF]Specification of the TUAK algorithm set: A second example algorithm set for the 3GPP authentication[END_REF] schemes are used in practice, which are based on block ciphers.

Note that our activity monitoring attack can also be exploited under those circumstances.

While they did not focus on the confidentiality of SQN , they still could have captured the traceability variants explained in Section 4.3.

Acknowledgment

We would like to thank the anonymous reviewers for valuable feedback. We are also thankful to Steve Babbage from the Vodafone Group for the fruitful discussions. This work was partially conducted when Ravishankar Borgaonkar was working at the University of Oxford, UK and when Lucca Hirschi was working at LSV, CNRS & ENS Cachan, France and then at ETH Zurich, Switzerland. This work was partially supported by a COST grant (COST-STSM-IC1306-33371) granted by the European Cooperation in Science and Technol-ogy (Crypto Action) and a mobility grant granted by the Doctoral School of the Paris-Saclay University.

A Notatations & Acronyms

We show in Table 1 an informal correspondence between our informal security architecture terminology and proper terminologies in 3G, 4G, and 5G networks.

B Generic SQN Inference Algorithm

This Section is dedicated to the description of our generic SQN inference algorithm parametrized by the increment γ that is used for updating SQN HN after each successful AKA session. In a nutshell, it is an extension of the algorithm described in Section 3.2.2 that works even when γ > 1. In particular, it is based on the same idea that consists in learning whether a remainder propagated or not at a specific position.

Informal description of the algorithm. We now give an informal presentation of this algorithm. While we have not reached a fixed point, we do the following.

-For all δ i from the sequence of {δ j } j given as input (let us call i its position in the sequence), we do the following.

-For all bit position p from 0 (least significant bit position) to 47 (the most significant bit position), we do the following. * We compute Γ = γ * 2 i that corresponds to the value that has been added to SQN 0 UE resulting to the sequence number in AUTS i where δ i = AUTS 0 ⊕ AUTS i . Using all already inferred bits of SQN 0 UE at positions from 0 to p -1, we infer if Γ + SQN 0 UE yields a remainder that propagates from bit position p to p + 1. If the latter could not be inferred, continue to the next iteration. If the latter could be inferred we let Γ ′ [p + 1] and Γ ′

[p] be the bits positions of Γ plus the (possible) remainder. Now, using that information and the Table 6, we may be able to infer the bit of SQN 0 UE at position p. The symbol † means that the given δ i is incoherent with previously analyzed δ j . This may happen if some δ i were not fetched correctly for instance.

Increment

Bits

Impossible to infer, just continue Fig. 6. Given the bits of the increment Γ at position p + 1 and p, and the bits of δ i at position p and p + 1, this table gives the inferred bit of SQN 0 UE at position p. † indicates an inconsistency.

When a fixed point has been reached (i.e., the two loops have been completed without being able to infer more bits of SQN 0 UE ), stop and return the inferred bits.

Discussion. Note that for increment value we sometimes observed (e.g., γ = 33), this algorithm allows inferring more bits than the algorithm described in Section 3.2.2 (i.e., twice when n = 6). Indeed, the binary representation of 33 is 100001 and thus, each time we analyze a certain δ i with its corresponding increment Γ = γ * 2 i , we are able to exploit the bit position i (because of the addition of 1 2 * 2 i ) and the bit position i + 6 (because of the addition of 100000 2 * 2 i ).

Finally, note that this algorithm can be made even more generic by dealing with AUTS fetched in different ways (e.g., yielding from the injection of consecutive challenges instead of the power of 2): it suffices to adapt the way we compute Γ.

C Other Variants of SQN Policies

According to non-normative specifications (Sections C.2 and C.3 from TS 33.102 [START_REF]3G security; Security architecture[END_REF]), SQN and its update policy can take different forms. We briefly explain how our attack can be easily adapted for those variants.

SQN can be made of two components SQN = SEQ IND where SEQ is a 43 bits long integer that


Alexander Kolpakov

Jun Murakami

Volume of a doubly truncated hyperbolic tetrahedron

Keywords: hyperbolic tetrahedron, Gram matrix, volume formula. 1 Introduction

The present paper regards the volume function of a doubly truncated hyperbolic tetrahedron. Starting from the previous results of J. Murakami, U. Yano and A. Ushijima, we have developed a unified approach to express the volume in different geometric cases via dilogarithm functions and to treat properly the many analytic strata of the latter. Finally, several numeric examples are given.

a Lambert cube has been investigated. The case of a general hyperbolic tetrahedron was considered in numerous papers [START_REF] Cho | On the volume formula for hyperbolic tetrahedra[END_REF][START_REF] Derevnin | A formula for the volume of a hyperbolic tetrahedron[END_REF][START_REF] Murakami | On the volume of hyperbolic and spherical tetrahedron[END_REF]. The case of a mildly truncated tetrahedron is due to J. Murakami and A. Ushijima [START_REF] Murakami | A volume formula for hyperbolic tetrahedra in terms of edge lengths[END_REF][START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF]. The paper [START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF] is the starting point where the question about intense truncations of a hyperbolic tetrahedron was posed. Thus, the case of a prism truncated tetrahedron remains unattended. As we shall see later, it brings some essential difficulties. First, the structure of the volume formula should change, as first observed in [START_REF] Kellerhals | On the volume of hyperbolic polyhedra[END_REF]. Second, the branching properties of the volume function come into sight. This phenomenon was first observed for tetrahedra in the spherical space and is usually related to the use of the dilogarithm function or its analogues, see [START_REF] Kolpakov | Volume formula for a Z 2 -symmetric spherical tetrahedron through its edge lengths[END_REF][START_REF] Murakami | A volume formula for hyperbolic tetrahedra in terms of edge lengths[END_REF][START_REF] Murakami | The volume formulas for a spherical tetrahedron[END_REF]. For the rest of the paper, a mildly (doubly) truncated tetrahedron is given in Fig. 1. Its dihedral angles are θ k and its corresponding edge lengths are k , k = 1, 6 * . Figure 1: Mildly (doubly) truncated tetrahedron A prism truncated tetrahedron is given in Fig. 2. The dashed edge connects the ultra-ideal vertices and corresponds to the edge 4 in the previous case. The dihedral angles remain the same, except that the altitude of the prism replaces the dihedral angle θ 4 . The altitude carries the dihedral angle µ and is orthogonal to the bases because of the truncation. Right dihedral angles in Fig. 1

Preliminaries

The following propositions reveal a relationship between the Lorentzian inner product of two vectors and the mutual position of the respective hyperplanes.

Proposition 1 Let u and v be two non-collinear points in H . Then the following holds:

i) The hyperplanes Π u and Π v intersect if and only if | u, v | < 1. The dihedral angle θ between them measured in Γ u ∩ Γ v is given by the formula cos θ = -u, v .
ii) The hyperplanes Π u and

Π v do not intersect in B n if and only if | u, v | > 1.
They intersect in Ext B n and admit a common perpendicular inside B n of length d given by the formula cosh d = ± u, v † .

iii) The hyperplanes Π u and Π v intersect on the ideal boundary ∂B n only, if and only if | u, v | = 1.

In case ii) we say the hyperplanes Π u and Π v to be ultra-parallel and in case iii) to be parallel.

Proposition 2 Let u be a point in B n and let Π v be a geodesic hyperplane whose normal vector v ∈ H is such that u, v < 0. Then the length d of the perpendicular dropped from the point u onto the hyperplane Π v is given by the formula sinh d = -u, v .

Let T be a generalised tetrahedron in H 3 with outward Lorentzian normals n i , i = 1, 4, to its faces and vertex vectors v i , i = 1, 4, as depicted in Fig. 2. Let G denote the Gram matrix for the normals G = n i , n j 4 i,j=1 . The conditions under which G describes a generalised mildly truncated tetrahedron are given by [START_REF] Mednykh | Elementary formulas for a hyperbolic tetrahedron[END_REF] and [START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF]. For a prism truncated tetrahedron, its existence and geometry are determined by the vectors ñi , i = 1, 6, where ñi = n i for i = 1, 4 and ñ5 = v 1 , ñ6 = v 2 . Hence the above matrix G does not have necessarily a Lorentzian signature. However, it will suffice for our purpose. In case T is prism truncated, as Fig. 2 shows, we obtain

G =     1 -cos θ 1 -cos θ 2 -cos θ 6 -cos θ 1 1 -cos θ 3 -cos θ 5 -cos θ 2 -cos θ 3 1 -cosh -cos θ 6 -cos θ 5 -cosh 1     , (1)
in accordance with Proposition 1. We will define the edge length matrix G of T by

G =     -1 -cos µ i sinh 5 i sinh 3 -cos µ -1 i sinh 6 i sinh 2 -i sinh 5 -i sinh 6 -1 -cosh 1 -i sinh 3 -i sinh 2 -cosh 1 -1     (2)
in order to obtain a Hermitian analogue of the usual edge length matrix for a mildly truncated tetrahedron (for the latter, see [START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF]). By [START_REF] Mednykh | Elementary formulas for a hyperbolic tetrahedron[END_REF] or [START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF], we have that

-g ij = c ij √ c ii √ c jj , (3)
where c ij are the corresponding (i, j) cofactors of the matrix G. The complex conjugation g ij = g ji , i, j = 1, 4, corresponds to a choice of the analytic strata for the square root function √ •.

Proposition 3 ( [START_REF] Mednykh | Elementary formulas for a hyperbolic tetrahedron[END_REF][START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF]) The vertex v i , i = 1, 4, of T is proper, ideal, or ultra-ideal provided that c ii > 0, c ii = 0, or c ii < 0, respectively.

Hence, Propositions 1-2 imply that the matrices G and G agree concerning the relationship of the geometric parameters of T . The matrix G has complex entries since the minors c ii , i = 1, 4, in formula (3) may have different signs by Proposition 3.

To perform our computations later on in a more efficient way, we shall introduce the parameters a k , k = 1, 6, associated with the edges of the tetrahedron T . If T is a prism truncated tetrahedron, then we set a k := e iθ k , k ∈ {1, 2, 3, 5, 6}, a 4 := e and then

G =      1 -a 1 +1/a 1 2 -a 2 +1/a 2 2 -a 6 +1/a 6 2 -a 1 +1/a 1 2 1 -a 3 +1/a 3 2 -a 5 +1/a 5 2 -a 2 +1/a 2 2 -a 3 +1/a 3 2 1 -a 4 +1/a 4 2 -a 6 +1/a 6 2 -a 5 +1/a 5 2 -a 4 +1/a 4 2 1      . ( 4
)
The meaning of the parameters becomes clear if one observes the picture of a mildly truncated tetrahedron T (see Fig. 2). In case two vertices v 1 and v 2 of T become ultra-ideal and the corresponding polar hyperplanes intersect (see [START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF] for more basic details), the edge v 1 v 2 becomes dual in a sense to the altitude of the resulting prism. Since in case of a mildly truncated tetrahedron we have a k = e iθ k according to [START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF], the altitude for now corresponds still to the parameter a 4 , in order to keep consistent notation.

Volume formula

Let U = U (a 1 , a 2 , a 3 , a 4 , a 5 , a 6 , z) denote the function

U = Li 2 (z) + Li 2 (a 1 a 2 a 4 a 5 z) + Li 2 (a 1 a 3 a 4 a 6 z) + Li 2 (a 2 a 3 a 5 a 6 z) (5)
-Li 2 (-a 1 a 2 a 3 z) -Li 2 (-a 1 a 5 a 6 z) -Li 2 (-a 2 a 4 a 6 z) -Li 2 (-a 3 a 4 a 5 z)
depending on seven complex variables a k , k = 1, 6 and z, where Li 2 (•) is the dilogarithm function. Let z -and z + be two solutions to the equation e z ∂U ∂z = 1 in the variable z. According to [START_REF] Murakami | On the volume of hyperbolic and spherical tetrahedron[END_REF], these are

z -= -q 1 -q 2 1 -4q 0 q 2 2q 2 and z + = -q 1 + q 2 1 -4q 0 q 2 2q 2 , (6)
where q 0 = 1+a 1 a 2 a 3 +a 1 a 5 a 6 +a 2 a 4 a 6 +a 3 a 4 a 5 +a 1 a 2 a 4 a 5 +a 1 a 3 a 4 a 6 +a 2 a 3 a 5 a 6 ,

q 1 = -a 1 a 2 a 3 a 4 a 5 a 6 a 1 - 1 a 1 a 4 - 1 a 4 + a 2 - 1 a 2 a 5 - 1 a 5 + a 3 - 1 a 3 a 6 - 1 a 6 , (7)
q 2 = a 1 a 2 a 3 a 4 a 5 a 6 (a 1 a 4 + a 2 a 5 + a 3 a 6 + a 1 a 2 a 6 + a 1 a 3 a 5 + a 2 a 3 a 4 + a 4 a 5 a 6 + a 1 a 2 a 3 a 4 a 5 a 6 ).
Given a function f (x, y, . . . , z), let f (x, y, . . . , z) | z=z - z=z + denote the difference f (x, y, . . . , z -) -f (x, y, . . . , z + ). Now we define the following function V = V (a 1 , a 2 , a 3 , a 4 , a 5 , a 6 , z) by means of the equality

V = i 4 U (a 1 , a 2 , a 3 , a 4 , a 5 , a 6 , z) -z ∂U ∂z log z z=z - z=z + . (8)
Let W = W (a 1 , a 2 , a 3 , a 4 , a 5 , a 6 , z) denote the function below, that will correct possible branching of V resulting from the use of (di-)logarithms:

W = 6 k=1 a k ∂V ∂a k - i 4 log e -4i a k ∂V ∂a k log a k . (9)
Given a generalised hyperbolic tetrahedron as in Fig. 2, truncated down to a quadrilateral prism with essential dihedral angles θ k , k ∈ {1, 2, 3, 5, 6}, altitude and dihedral angle µ along it, we set a k = e iθ k , k ∈ {1, 2, 3, 5, 6}, a 4 = e , as above. Then the following theorem holds.

Theorem 1 Let T be a generalised hyperbolic tetrahedron as given in Fig. 2.

Its volume equals

Vol T = -V + W - µ 2 .
Note. In the statement above, the altitude length is = log a 4 and the corresponding dihedral angle equals µ = -2 a 4

∂V ∂a 4 mod π.

3.1 Preceding lemmas. Before giving a proof to Theorem 1, we need several auxiliary statements concerning the branching of the volume function.

Lemma 1 The function W has a.e. vanishing derivatives ∂W ∂a k , k = 1, 6.

Proof. By computing the derivative of ( 9) with respect to each a k , k = 1, 6, outside of its branching points and by making use of the identities d dz log z = 1/z, e z e w = e z+w for all z, w ∈ C. Since the branching points of a finite amount of log(•) and Li 2 (•) functions form a discrete set in C, the lemma follows.

Lemma 2 The function (-V + W ) does not branch with respect to the variables a k , k = 1, 6, and z.

Proof. Let us consider a possible branching of the function defined by formula [START_REF] Kolpakov | Volume formula for a Z 2 -symmetric spherical tetrahedron through its edge lengths[END_REF]. Let U comprise only principal strata of the dilogarithm and let U correspond to another ones. Then we have

U | z=z ± = U | z=z ± +2πik ± 0 log(z ± ) + 2πik ± 1 log(a 1 a 2 a 4 a 5 z ± ) +2πik ± 2 log(a 1 a 3 a 4 a 6 z ± ) + 2πik ± 3 log(a 2 a 3 a 5 a 6 z ± ) +2πik ± 4 log(-a 1 a 2 a 3 z ± ) + 2πik ± 5 log(-a 1 a 5 a 6 z ± ) (10) +2πik ± 6 log(-a 2 a 4 a 6 z ± ) + 2πik ± 7 log(-a 3 a 4 a 5 z ± ) +4π 2 k ± 8 ,
with some k j ∈ Z, j = 0, 8. From the above formula, it follows that

z ± ∂U ∂z z=z ± log z ± = z ± ∂U ∂z z=z ± log z ± + 2πi 7 j=0 k ± j log z ± . (11)
Then, according to formulas (8), ( 10) -( 11), the following expression holds for the corresponding analytic strata of the function V :

V = V - π 2 6 j=1 m j log a j + iπ 2 2 m 7 , (12)
where m j ∈ Z, j = 1, 7 and we have used the formula log(uv) = log u + log v + 2πik, k ∈ Z. Hence, according to [START_REF] Szirmai | Horoball packings for the Lambert-cube tilings in the hyperbolic 3-space[END_REF], we compute

a j ∂V ∂a j = a j ∂V ∂a j - πm j 2 ,
for each j = 1, 6. The latter implies that

a j ∂V ∂a j - i 4 log e -4i a j ∂V ∂a j = a j ∂V ∂a j - i 4 log e -4i a j ∂V ∂a j - πm j 2 ,
for j = 1, 6, since we choose the principal stratum of the logarithm function log(•). Thus, by formula (9),

-V + W = -V + W + π 2 6 j=1 m j log a j - iπ 2 2 m 7 - π 2 6 j=1 m j log a j = -V + W - iπ 2 2 m 7 ,
with m j ∈ Z, j = 1, 7. The proof is completed.

3.2 Proof of Theorem 1. The scheme of our proof is the following: first we show that ∂ ∂θ k Vol T = -k 2 , k ∈ {1, 2, 3, 5, 6}, ∂ ∂µ Vol T = -2 and second we apply the generalised Schläfli formula [7, Equation 1] to show that the volume function and the one from Theorem 1 coincide up to a constant. Finally, the remaining constant is determined. Now, let us prove the three statements below:

(i) ∂ ∂θ 1 Vol T = -1 2 , (ii) ∂ ∂θ k Vol T = -k 2 for k ∈ {2, 3, 5, 6}, (iii) ∂ ∂µ Vol T = -2 .
Note that in case (ii) it suffices to show ∂ ∂θ 2 Vol T = -2 2 . The statement for another k ∈ {3, 5, 6} is completely analogous.

Let us show that the equality in case (i) holds. First, we compute

∂ ∂θ 1 U -z ∂U ∂z log z = i a 1 ∂ ∂a 1 U -z ∂U ∂z log z = = ia 1 ∂U ∂a 1 -log z ∂ ∂a 1 z ∂U ∂z
Upon the substitution z := z ± , we see that

∂ ∂a 1 z ± ∂U ∂z (a 1 , a 2 , a 3 , a 4 , a 5 , a 6 , z ± ) = 0,
by taking the respective derivative on both sides of the identity e z ± ∂U ∂z (a 1 ,a 2 ,a 3 ,a 4 ,a 5 ,a 6 ,z ± ) = 1, c.f. the definition of z ± and formula [START_REF] Mednykh | Elementary formulas for a hyperbolic tetrahedron[END_REF]. Finally, we get

∂V ∂θ 1 = - a 1 4 ∂U ∂a 1 z=z - z=z + = - 1 4 log φ(z -)ψ(z + ) φ(z + )ψ(z -) + iπ 2 k,
for a certain k ∈ Z, where the functions φ(•) and ψ(•) are

φ(z) = (1 + a 1 a 2 a 3 z)(1 + a 1 a 5 a 6 z), ψ(z) = (1 -a 1 a 2 a 4 a 5 z)(1 -a 1 a 3 a 4 a 6 z).
The real part of the above expression is

∂V ∂θ 1 = - 1 4 log φ(z -)ψ(z + ) φ(z + )ψ(z -) . (13)
Let us set ∆ = det G and δ = √ det G. We shall show that the expression

E = φ(z -)ψ(z + ) c 34 + δ a 1 -1/a 1 2 -φ(z + )ψ(z -) c 34 -δ a 1 -1/a 1 2 (14)
is identically zero for all a k ∈ C, k = 1, 6, which it actually depends on. In order to perform the computation, the following formulas are used:

z -= -q 1 -4δ 2q 2 , z + = -q 1 + 4δ 2q 2 ,
where ql = q l / 6 k=1 a k for l = 1, 2 (c.f. formulas ( 6) -( 7)). Note that one may consider the expression E as a rational function of independent variables a k , k = 1, 6, ∆ and δ, making the computation easier to perform by a software routine [START_REF] Research | Mathematica 8", a computational software routine[END_REF]. First, we have

1 δ ∂E ∂a 1 = 4a 1 Y q3 2 ∂∆ ∂a 1 ,
where Y = Y (a 1 , a 2 , a 3 , a 4 , a 5 , a 6 ) is a certain technical term explained in Appendix. Since ∂∆ ∂a 1 = 2δ ∂δ ∂a 1 , the above expression gives us

∂E ∂a 1 = 8a 1 ∆ q3 2 ∂δ ∂a 1 Y . (15)
Second, we obtain

∂E ∂δ = - 8a 1 ∆ q3 2 Y . (16)
Finally, we recall that δ is a function of a k , k = 1, 6, and the total derivative of E with respect to a 1 is

∂ ∂a 1 E | δ:=δ(a 1 ,a 2 ,a 3 ,a 4 ,a 5 ,a 6 ) = ∂E ∂a 1 + ∂E ∂δ ∂δ ∂a 1 = 0,
according to equalities ( 15)-( 16).

An analogous computation shows that ∂ ∂a k E | δ:=δ(a 1 ,a 2 ,a 3 ,a 4 ,a 5 ,a 6 ) = 0 for all k = 1, 6. Then by setting a k = 1, k = 1, 6, we get ∆ = -16 and so δ = 8i. In this case E = 0. Thus the equality E ≡ 0 holds for all a k ∈ C, k = 1, 6. Together with [START_REF] Ushijima | A volume formula for generalised hyperbolic tetrahedra[END_REF] it gives

∂V ∂θ 1 = - 1 4 log c 34 -δ a 1 -a -1 1 2 c 34 + δ a 1 -a -1 1 2 . ( 17
)
On the other hand, by formula (3), we have

g 34 = -cosh 1 = -c 34 √ c 33 √ c 44 .
Here, both c 33 and c 44 are positive by Proposition 3, since the vertices v 3 and v 4 are proper. The formula above leads to the following equation e 2 1 + 2 g 34 e 1 + 1 = 0, the solution to which is determined by

e 2 1 = c 34 + δ a 1 -a -1 1 2 c 34 -δ a 1 -a -1 1 2 , (18)
in analogy to [13, Equation 5.3]. Thus, equalities (17) -(18) imply

∂V ∂θ 1 = - 1 4 log e -2 1 = 1 2 .
Together with Lemma 1, this implies that claim (i) is satisfied. As already mentioned, in case (ii) it suffices to prove ∂ ∂θ 2 Vol T = -2 2 . The statement for another k ∈ {3, 5, 6} is analogous. By formula (3) we have that

g 24 = i sinh 2 = -c 24 √ c 22 √ c 44 .
Since the vertex v 2 is ultra-ideal and the vertex v 4 is proper, by Proposition 3, c 22 < 0 and c 44 > 0. Thus, sinh 2 = c 24 √ -c 22 c 44 .

The formula above implies e

-e 2 2 = c 24 + δ a 2 -a -1 2 2 c 24 -δ a 2 -a -1 2 2 . (21)
By analogy with (13), we get the formula

∂V ∂θ 2 = - 1 4 log φ(z -)ψ(z + ) φ(z + )ψ(z -) , (22)
where

φ(z) = (1 + a 1 a 2 a 3 z)(1 + a 2 a 4 a 6 z), ψ(z) = (1 -a 1 a 2 a 4 a 5 z)(1 -a 2 a 3 a 5 a 6 z).
Similar to case (i), the following relation holds:

φ(z -)ψ(z + ) φ(z + )ψ(z -) = c 24 -δ a 2 -a -1 2 2 c 24 + δ a 2 -a -1 2 2 .
Then formulas (21) -( 22) yield

∂V ∂θ 2 = - 1 4 log -1 e 2 2 = 2 2 .
The first equality of case (ii) now follows. Carrying out an analogous computation for ∂V ∂θ k , k = 3, 5, we obtain

∂V ∂θ 3 = 3 2 and ∂V ∂θ 5 = 5 2 .
Thus, all equalities of case (ii) hold.

As before, by formula (3), we obtain that Without loss of generality, the solution we choose is

-g 12 = cos µ = c 12 √ c 11 √ c 22 . ( 23
e iµ = -c 12 + c 2 12 -c 11 c 22 √ c 11 c 22 . (24)
By squaring (24) and by applying Jacobi's theorem to the corresponding cofactors of the matrix G, the formula below follows: Together with the equalities of cases (i)-(iii) it yields

e 2iµ = c 12 -δ a 4 -a -1 4 2 c 12 + δ a 4 -a -1
Vol T = -V + W - µ 2 + C , (27)
where C ∈ R is a constant. Finally, we prove that C = 0, and the theorem follows. Passing to the limit θ k → π 2 , k = 1, 6, the generalised hyperbolic tetrahedron T shrinks to a point, since geometrically it tends to a Euclidean prism. Thus, we have µ → π 2 and → 0. By setting the limiting values above, we obtain that a k = i, k ∈ {1, 2, 3, 5, 6}, a 4 = 1. Then z -= z + = 1 by equality [START_REF] Mednykh | Elementary formulas for a hyperbolic tetrahedron[END_REF], and hence V = 0. Since the dilogarithm function does not branch at ±1, ±i, we have W = 0. Since T shrinks to a point, Vol T → 0, that implies C = 0 by means of (27) and the proof is completed.

(θ 1 , θ 2 , θ 3 , θ 5 , θ 6 ) ( , µ) Volume Reference ( π

  -2 are not indicated by symbols. The other dihedral angles and the corresponding edge length are called essential.

Figure 2 :

 2 Figure 2: Prism (intensely) truncated tetrahedron T and its geometric parameters

) Since both vertices v 1

 1 and v 2 are ultra-ideal, by Proposition 3, the cofactors c 11 and c 22 are negative. Then (23) implies the equation e 2iµ + 2c 12 e iµ √ c 11 c 22 + 1 = 0.

12 -δ a 4 -a - 1 4 2 c 12 + δ a 4 -a -1 4 2 ,

 124121242 -)ψ(z + ) φ(z + )ψ(z -) ,(26)whereφ(z) = (1 + a 3 a 4 a 5 z)(1 + a 2 a 4 a 6 z), ψ(z) = (1 -a 1 a 2 a 4 a 5 z)(1 -a 1 a 3 a 4 a 6 z).Similar to cases (i) and (ii), we have the relationφ(z -)ψ(z + ) φ(z + )ψ(z -) = c ≤ µ ≤ π, we choose k = 0 and so ∂V ∂ = -µ 2 .The latter formula implies the equality of case (iii). Now, by the generalised Schläfli formula[START_REF] Milnor | The Schläfli differential equality[END_REF], dVol T = -

† we chose the minus sign if Γu ∩ Γv = ∅, otherwise we choose the plus sign.

* supported by the Schweizerischer Nationalfonds SNF no. 200021-131967/1 † supported by Grant-in-Aid for Scientific Research no. 22540236 1

Numeric computations

In Table 1 we have collected several volumes of prism truncated tetrahedron computed by using Theorem 1 and before in [START_REF] Derevnin | The Coxeter prisms in H 3 " in Recent advances in group theory and low-dimensional topology[END_REF][START_REF] Szirmai | Horoball packings for the Lambert-cube tilings in the hyperbolic 3-space[END_REF]. The altitude of a prism truncated tetrahedron is computed from its dihedral angles, as the remark after Theorem 1 states. All numeric computations are carried out using the software routine "Mathematica" [START_REF] Research | Mathematica 8", a computational software routine[END_REF].

Appendix

The term Y from Section 3.2 Let us first recall of the expressions q k , k = 0, 1, 2, that are polynomials in the variables a k , k = 1, 6 defined by formula ( 7) and the expressions ql , l = 1, 2, defined in the proof of Theorem 1 by ql = q l / 6 k=1 a k , l = 1, 2. Then, the following lemma holds concerning the technical term Y mentioned above, that actually equals Proof. By setting a 1 = a 6 := 0, we get q 0 = 1 + a 3 a 4 a 5 , q 1 = q 2 = 0 and Y | a 1 =a 6 :=0 = a 3 2 a 3 a 4 a 5 (a 3 a 4 + a 5 ) = a 3 2 (q 0 | a 1 =a 6 :=0 -1) (a 3 a 4 + a 5 ).

As well, we have q2 = a 2 (a 3 a 4 + a 5 ) and

The former equality proves that Y is not a polynomial in the variables q 0 , q 1 , q 2 . The latter shows that Y is not a polynomial in q 0 , q 1 , q2 either.