The 5G-AKA Authentication Protocol Privacy

I. INTRODUCTION

• AKA protocols establish a shared secret key between a subscriber and service provider, and sequence numbers make them stateful.In 3G and 4G, the subscriber-side USIM has limited computational power, so the protocols use symmetric cryptography without subscriber-side pseudorandom generation.Source: §I · p. 1
• Randomized asymmetric encryption in 5G-AKA prevents IMSI-catcher attacks, but linkability attacks against older AKA versions and an encrypted-identity replay attack still apply.The paper identifies attacks from,, and.Source: §I · pp. 1–2
• Prior formal analyses of AKA missed attacks after abstracting away protocol features, while a computational proof for a complete AKA protocol was lacking.The paper describes omissions involving xor, sequence-number updates, re-synchronization, and temporary identities.Source: §I · p. 2
• AKA+ is proposed as a modified 5G-AKA protocol that improves privacy while meeting the same design and efficiency constraints.The stated objectives include similar communication complexity and use of the same cryptographic primitives.Source: §I · pp. 1–2
• The paper introduces σ-unlinkability, a parametric privacy property intended to quantify protocol privacy more finely.The authors state that AKA+ satisfies this property and provides mutual authentication, with a proof in the Bana-Comon model.Source: §I · p. 2

A. Description of the Protocol

• 5G-AKA identifies the user through a temporary GUTI or a randomized public-key encryption of the SUPI; the HN processes the identity and can issue a fresh GUTI after successful authentication.A GUTI can replace the encrypted identity and avoid an asymmetric encryption computation.Source: A. Description of the Protocol · pp. 3–4

A. IMSI-Catcher Attack

• The IMSI-catcher attack obtains a UE’s permanent identity by requesting it, but asymmetric encryption of the identity in 5G-AKA prevents this attack.The section identifies the other known attacks as carrying over to 5G-AKA.Source: A. IMSI-Catcher Attack · p. 4, §III · p. 4

B. The Failure Message Attack

• A replayed authentication message distinguishes the target UE from another UE: the target sends a re-synchronization message, while the other sends “Auth-Failure.”The attacker can repeat the check to test for the tracked user’s presence.Source: B. The Failure Message Attack · pp. 4–5

C. The Encrypted IMSI Replay Attack

• Replaying a captured encrypted identity makes the target UE accept the resulting authentication message, while a different UE rejects it, breaking unlinkability.The attacker intercepts the UE's identifying message and replaces it with the previously captured encrypted identity.Source: C. The Encrypted IMSI Replay Attack · p. 5

D. Attack Against The PRIV-AKA Protocol

• The PRIV-AKA attack can permanently desynchronize the UE and HN, enabling the adversary to track the UE when it later aborts protocol runs.The attack exploits the HN incrementing its sequence number only after receiving the UE's confirmation; it requires unfinished HN sessions to remain open concurrently.Source: D. Attack Against The PRIV-AKA Protocol · p. 5
• The PRIV-AKA attack depends on two unfinished HN sessions for the same UE remaining open; closing unfinished sessions prevents that particular attack.However, closing an earlier session when a later session completes can itself reveal whether both sessions involve the same UE.Source: D. Attack Against The PRIV-AKA Protocol · p. 5

E. Sequence Numbers and Unlinkability

• The authors conjecture that sequence-number protocols without UE-side randomness cannot jointly provide functionality, authentication, and unlinkability.They offer no formal statement or proof, and note that both parties generating random challenges can satisfy all three requirements.Source: E. Sequence Numbers and Unlinkability · p. 6

IV. THE AKA+ PROTOCOL

• AKA+ is a fixed version of 5G-AKA designed to offer privacy against an active attacker and satisfy the protocol’s design and efficiency constraints.The authors state that it satisfies a weaker unlinkability notion, σ-unlinkability.Source: §IV · p. 6

A. Efficiency and Design Constraints

• AKA+ targets at most four messages per session, the 5G-AKA UE cryptographic primitives, and at most one UE random draw in specified sessions.The random draw is allowed only when no GUTI is available or re-synchronization is needed.Source: A. Efficiency and Design Constraints · p. 6

B. Key Ideas

• AKA+ conceals re-synchronization in the next randomized SUPI encryption, eliminating a distinct message that exposed whether authentication failed.The UE already generates randomness for that encryption, so this does not require additional random-number generation.Source: B. Key Ideas · pp. 6–7
• A fresh HN challenge accompanies permanent-identity use to prevent replay, while one-use temporary identities need no challenge; the protocol therefore separates SUPI and GUTI paths.The SUPI path uses four messages, while the GUTI path uses three.Source: B. Key Ideas · p. 7

C. Architecture and States

• A session runs SUPI or GUTI authentication followed by ASSIGN-GUTI; the three-message GUTI path avoids UE randomness and asymmetric encryption, making it faster.The GUTI path is recommended when a valid temporary identity is available.Source: C. Architecture and States · p. 7

D. The SUPI, GUTI and ASSIGN-GUTI Sub-Protocols

• The SUPI sub-protocol uses the permanent identity and supports re-synchronization, while the GUTI sub-protocol uses a temporary identity and requires synchronization to succeed.The SUPI route is expensive to run; the GUTI route is inexpensive.Source: a) The SUPI Sub-Protocol · p. 8, b) The GUTI Sub-Protocol · p. 8
• In the SUPI route, the HN sends a fresh challenge; the UE encrypts its identity and sequence number, then the HN checks identity, MAC, and sequence-number progression.The HN’s increasing-sequence check is described as crucial to the protocol.Source: a) The SUPI Sub-Protocol · p. 8
• In the GUTI route, the UE uses its temporary identity once, and the HN returns a challenge with concealed sequence-number information and a MAC.After successful checks, the UE and HN update sequence state and the HN generates a fresh temporary identity.Source: b) The GUTI Sub-Protocol · p. 8, N , GUTIID · p. 8
• After either authentication route succeeds, ASSIGN-GUTI sends the UE a concealed, authenticated fresh temporary identity for a faster GUTI session next time.The HN conceals the identity using a keyed function of the stored challenge, and the UE unconceals it.Source: c) The ASSIGN-GUTI Sub-Protocol · p. 9

V. UNLINKABILITY

• The unlinkability game lets an adversary interact with subscribers through virtual handlers and tests whether it can distinguish which identity a handler represents.A q-unlinkability adversary must make fewer than q oracle calls and guess the hidden bit with a non-negligible advantage.Source: §V · p. 9
• AKA+ is not ordinarily unlinkable: after intercepting a GUTI session’s last message, an attacker can distinguish a subscriber with no remaining GUTI from one that still has one.The attacker uses the different outcomes of a subsequent GUTI session to win the linkability game.Source: Figure 9 · p. 10, §V · p. 10
• AKA+ lacks forward secrecy: obtaining a UE’s long-term secret key allows decryption of its past messages, limiting the unlinkability goal to weak adversaries.The paper therefore removes the corruption oracle from its unlinkability definition.Source: §V · p. 10
• σ-unlinkability replaces DrawUE with DrawUEσ, which applies a state update to the selected subscriber before returning its virtual handler.For AKA+, σul invalidates the temporary identity, so a subscriber can run only the SUPI sub-protocol and identity changes can occur at those executions.Source: §V · p. 10
• AKA+ is σul-unlinkable for any number of agents and sessions if the asymmetric encryption is IND-CCA1 secure and the specified function families satisfy the joint PRF assumption.The paper notes a trade-off: SUPI sessions are more expensive but provide more privacy.Source: §V · pp. 10–11

B. A Subtle Attack

• Without the session-ID check, an older GUTI-session message can update HN state after a SUPI session, desynchronizing one candidate and enabling a distinguishing attack.The check detects whether another session occurred and prevents the sequence-number update in that case.Source: B. A Subtle Attack · p. 11

VI. MODELING IN THE BANA-COMON LOGIC

• The proof strategy builds axioms for computational properties, cryptographic hypotheses, and implementation assumptions, then derives the protocol-security formula from them.The paper uses Bana-Comon logic, where messages are terms and security properties are first-order formulas.Source: §VI · p. 11

A. Syntax and Semantics

• In the computational model, adversarial functions represent arbitrary PPTMs, protocol randomness remains on a hidden tape, and indistinguishability predicates use computational indistinguishability.The logic’s terms and formulas use function symbols and a predicate for indistinguishability between vectors of terms.Source: A. Syntax and Semantics · p. 11

B. Modeling of the AKA+ Protocol States and Messages

• The AKA+ model makes assumptions and implementation details explicit by representing subscriber state symbolically and mapping fixed oracle-call traces to symbolic states and messages.Messages depend on the preceding trace, and state updates specify which protocol variables change.Source: B. Modeling of the AKA+ Protocol… · pp. 11–12, A , GUTIID · p. 12

A , GUTIID

• The proof criterion is to derive indistinguishability of the adversary’s observed frames for every permitted pair of traces; the authors omit the proposition’s proof details.The proposition states that this establishes σul-unlinkability in computational models satisfying the axioms.Source: A , GUTIID · p. 13

C. Axioms

• The proof derives indistinguishability for related traces using axioms valid under IND-CCA1 asymmetric encryption and the stated PRF assumptions.The derivation is required for every trace pair in Rul.Source: C. Axioms · p. 13
• Security is established for any AKA+ implementation satisfying Ax, rather than through a complete specification of every protocol function.The specification is under-specified; the axioms impose requirements on implementations.Source: C. Axioms · p. 13
• The axiom set separates structural, implementation, and cryptographic assumptions, with cryptographic axioms relying on jointly PRF MAC functions.The five MAC functions share a secret key and are assumed computationally indistinguishable from random functions simultaneously.Source: C. Axioms · pp. 13–14
• Structural axioms support indistinguishability reasoning, while .= specifies functional correctness such as pair projection and decryption with the correct key.The structural rules include function-application lifting and replacement of equal terms.Source: C. Axioms · p. 14
• EUF-MACj and CRj axioms capture MAC unforgeability and collision resistance; Proposition 2 establishes their validity when the MAC functions are jointly PRF.The axioms are stated to be sound.Source: C. Axioms · p. 14

A. Mutual Authentication of the AKA+ Protocol

• Authentication is modeled as a correspondence between events, and acceptance conditions rely on MAC unforgeability and collision resistance.The proof derives necessary acceptance conditions using EUF-MACj and CRj axioms.Source: A. Mutual Authentication of the AKA+… · p. 15
• AKA+ provides authentication in both directions: network acceptance requires an honestly generated subscriber message, and user belief in network authentication implies the network initiated the protocol.The user-by-network guarantee is also stated as requiring the subscriber to have initiated the protocol with that network session.Source: A. Mutual Authentication of the AKA+… · p. 15
• For the network’s acceptance, the accepted message is characterized as honestly generated by a subscriber session that received the network’s challenge.Lemma 2 gives a necessary condition; Lemma 4 states an if-and-only-if characterization for acceptance by PN(j, 1).Source: A. Mutual Authentication of the AKA+… · p. 15
• For every trace pair in Rul, the authors derive indistinguishability, establishing AKA+’s σul-unlinkability.The proof proceeds by induction and matches left and right honest transcripts, sometimes using many-to-one matches or showing transcripts fail.Source: A. Mutual Authentication of the AKA+… · pp. 15–16
• When transcript matching fails, the proof either uses many-to-one matching or shows that some transcripts always fail due to desynchronization.The latter case requires tracking SQNID values across sessions.Source: A. Mutual Authentication of the AKA+… · p. 16

VIII. CONCLUSION

• 5G-AKA avoids IMSI-catcher attacks, but several known privacy attacks still apply; the paper also finds a desynchronization attack against PRIV-AKA.PRIV-AKA is a modified AKA version that had been claimed secure.Source: §VIII · p. 16
• AKA+ is presented as an efficient fixed version of 5G-AKA with improved privacy guarantees.The protocol is intended to satisfy 5G-AKA’s cost and efficiency constraints, as described in the paper’s abstract.Source: §VIII · p. 16
• The paper defines σ-unlinkability as a parametric privacy property requiring proof for a subset of standard unlinkability-game scenarios.This property supports a fine-grained quantification of protocol privacy, as stated in the abstract.Source: §VIII · p. 16
• The authors prove mutual authentication and σul-unlinkability for any number of agents and sessions in the Bana-Comon model.The paper describes that model as suited to formal analysis of stateful protocols.Source: §VIII · p. 16

APPENDIX I AXIOMS

• The axiom set is partitioned into structural, implementation, and cryptographic axioms, with term, position, context, and subterm definitions supporting the formalization.It also defines when a term appears only in specified contexts, such as a nonce occurring only under public- or secret-key functions.Source: Appendix I · p. 20

A. CCA1 Axioms

• Both CCA1s and CCA1 axioms are valid when the encryption scheme is IND-CCA1 secure; CCA1 is derived using CCA1s and transitivity.The CCA1s formulation includes a length-equality premise.Source: A. CCA1 Axioms · pp. 20–21

B. PRF-MAC Axioms

• The PRF-MAC axiom schema is valid for PRF functions after dropping a syntactic requirement that every hash occurrence use the key; the extension covers jointly PRF function families.The appendix translates these properties into axiom schemes for Mac1–Mac5 and f and f^r, valid when their functions are jointly PRF.Source: B. PRF-MAC Axioms · pp. 22–23

C. EUF-MAC Axioms

• SIMP-EUF-MAC axioms are valid for EUF-MAC-secure functions, and joint PRF security implies EUF-MAC security even when the key is shared across the function family.The appendix translates the joint-key property into EUF-MACj axioms, valid when each Macj is EUF-MAC secure with the key jointly used by the other Mac functions.Source: C. EUF-MAC Axioms · p. 24
• Under the assumed joint EUF-MAC security, the appendix's construction of an adversary from an invalid axiom instance yields a non-negligible winning probability and a contradiction.Source: C. EUF-MAC Axioms · p. 25

D. CR Axioms

• The CR axioms are valid when each MAC function is collision-resistant under jointly shared keys, and EUF-MAC security with jointly shared keys implies collision resistance.The appendix defines collision resistance against an adversary with access to the function and any functions sharing its key.Source: D. CR Axioms · p. 25

E. Cryptographic Axioms

• The cryptographic axioms are valid assuming IND-CCA1-secure asymmetric encryption and the stated joint PRF assumptions for f, f_r, and Mac1–Mac5.Source: E. Cryptographic Axioms · p. 25

F. Structural and Implementation Axioms

• The structural axioms are valid in any computational model, covering indistinguishability equivalence, term transformations, fresh sampling, and conditional branching.Implementation axioms separately collect equalities for conditionals, equality and decryption, lengths, injectivity, and sequence-number ranges.Source: F. Structural and Implementation Axioms · p. 26

G. P-EUF-MACs Axioms

• The partitioned P-EUF-MACj axioms are logical consequences of the base axioms, applying the EUF-MACj rule separately across a valid finite CS partition.Source: G. P-EUF-MACs Axioms · pp. 26–27

H. P-EUF-MAC Axioms

• The refined P-EUF-MACj axioms remain consequences of Ax while excluding MAC terms that occur only in boolean conditionals.The proof pulls out conditionals, labels their branches to retain their locations, applies EUF-MACj to the exposed MAC terms, and rewrites the conditionals back.Source: H. P-EUF-MAC Axioms · p. 27

I. Additional Axioms

• The indep-branch and contextual function-application rules, along with an additional axiom for all terms u and v, are derivable from Ax.The indep-branch rule follows by applying CS and Fresh; the contextual function rule pulls the function through the if-context before applying FA.Source: §I · p. 29
• Additional implementation equalities specify how functions distribute over conditionals and how nested, constant, or repeated tests can be simplified.Source: §I · p. 31
• Pair projections π_i return the corresponding component for pairs and triples.The passage defines π_i(⟨x1, x2⟩) = x_i for i ∈ {1, 2}, and π_i(⟨x1, x2, x3⟩) = x_i for i ∈ {1, 2, 3}.Source: §I · p. 31
• Equality axioms distinguish identical terms, unequal constants, and nonces absent from a term.The passage specifies eq(x, x) = true, eq(A, B) = false for distinct constants, and eq(t, n) = false when n is not in st(t).Source: §I · p. 31
• Length axioms equate lengths of corresponding terms, pairs, and subscriber identifiers.The listed equalities include len(u) = len(s), len(v) = len(t), len(⟨u, v⟩) = len(⟨s, t⟩), and len(ID1) = len(ID2) for subscriber identifiers.Source: §I · p. 31
• Ground-term arithmetic formulas entailed by Th(Z, 0, +, −, =, ≤) are assigned true.The passage states φ[⃗u] = true when ⃗u are ground terms and the indicated theory entails φ[⃗x].Source: §I · p. 31
• The axiom set is Aximpl = Axite ∪ Axeq ∪ Axlen ∪ Axinj ∪ AxSQN.The figure identifies the full set as the union of these five subsets.Source: Figure 15 · p. 31

A. Symbolic Protocol

• σul-unlinkability can be reduced to deriving φτ ∼φτ for each trace τ, using the most-anonymized trace that changes identities after NSID actions.The reduction relies on the stated assumption that implementations process messages according to the symbolic protocol; valid traces interleave runs of the UE and home-network transition systems.Source: A. Symbolic Protocol · p. 32

B. The AKA+ Protocol

• The AKA+ unlinkability model adds a read-only phantom variable syncID_U for each identity to track whether a successful SUPI session occurred since the last NSID action.Because syncID_U is not used by the protocol, unlinkability holds for AKA+ if and only if it holds for the extended protocol.Source: B. The AKA+ Protocol · p. 33

C. Invariants and Necessary Acceptance Conditions

• The invariant restricts use: nN occurs only in the HN public key pk(nN) and secret key sk(nN), and k_ID and k_ID_m occur only in key positions in Mac1–Mac5; A1 excludes nj from state before session start.Source: C. Invariants and Necessary Acceptance… · p. 34

D. Proof of Lemma 6

• The proof of Lemma 6 applies EUF-MAC and P-EUF-MAC2 alongside freshness, pair-injectivity, and MAC collision-resistance axioms.The proof text identifies INV-KEY as ensuring the syntactic side-conditions for EUF-MAC1.Source: D. Proof of Lemma 6 · pp. 36–37
• Lemma 6’s proof rules out replaying an old message when the earlier event has a different session index, and applies P-EUF-MAC3 and P-EUF-MAC4 in proving Acc3 and Acc4.The proof also invokes CR3 and CR4.Source: D. Proof of Lemma 6 · pp. 37–39

E. Authentication of the User by the Network

• AKA+ guarantees authentication of the user by the network.The appendix says this result subsumes Lemma 1.Source: E. Authentication of the User by the… · p. 39

F. Authentication of the Network by the User

• For any valid symbolic trace, successful user-side authentication implies that the user authenticated a network session.The proof states the stronger result for authentication that is neither fail nor ⊥.Source: F. Authentication of the Network by… · p. 41

G. Proof of Lemma 3

• The proof of Lemma 3 relies on Lemma 8.The supplied proof passages do not state the lemma’s result.Source: G. Proof of Lemma 3 · p. 43

H. Injective Authentication of the Network by the User

• The trace guarantees injective authentication of the network by the user.The passage states this result and introduces a formula for every identity and natural-number index, but the formula itself is not included.Source: H. Injective Authentication of the… · p. 43

APPENDIX III ACCEPTANCE CHARACTERIZATIONS

• The appendix develops necessary and sufficient conditions for user or network message acceptance, then uses GUTI concealment to derive stronger characterizations.It states that GUTI identity remains concealed until the subscriber starts a GUTI-protocol session.Source: APPENDIX III ACCEPTANCE… · p. 45

A. First Characterizations

• The first characterizations include Proposition 26’s B2 condition and Lemma 10’s Equ1 characterization for symbolic traces.The supplied passages identify these results but omit their complete formulas.Source: A. First Characterizations · pp. 45–46
• Proposition 27 states additional properties B3–B7 for valid symbolic traces and identities.The supplied passages list these properties but omit their complete formulas.Source: A. First Characterizations · p. 47
• Lemma 11 gives further acceptance characterizations Equ2 and Equ3 for the specified PUID and PN actions.The passages identify the actions and labels, but omit the full conditions.Source: A. First Characterizations · p. 50

G. Proof of Lemma 3

• Equ4 applies when ai = TUID(j, 1), with τ1 = _, TN(j0, 0) required to precede τ.The passage does not include the equation's expression.Source: A. First Characterizations · p. 50
• Equ5 applies when ai = TN(j, 1), with τ1 = _, TN(j, 0) preceding τ and ID ∈ Sid.The passage does not include the equation's expression.Source: A. First Characterizations · p. 50

B. Proof of Lemma 11

• The proof of Lemma 11 establishes (Equ2)–(Equ5) using (Acc2), (Acc1), (Acc3), and (Acc4), and concludes one step by injectivity of the pair.Source: B. Proof of Lemma 11 · pp. 51–52

C. GUTIID

• Lemma 12 states a conditional derivability result for valid traces involving user-ID and network actions, under a restriction on intervening actions.Its proof uses induction over the trace and a leak-term vector, applying freshness and PRF-f and PRF-MAC5 axioms in key cases.Source: C. GUTIID · pp. 53, 55, 56

D. Stronger Characterizations

• For every valid symbolic trace τ = _, ai and identity ID, Lemma 13 gives a stronger version of (Acc3); (StrAcc1) applies when ai = TUID(j, 1), with τ1 = _, TUID(j, 0) such that τ1 ≺ τ, and k ≡k ID.Source: D. Stronger Characterizations · p. 57
• The trace-ordering proof aims to apply the GUTI concealment lemma to derive a contradiction, then concludes the proof.It checks the lemma’s hypothesis against the intervening PUID, TUID, and FUID actions.Source: D. Stronger Characterizations · pp. 58–59
• Lemma 14 is stated for every valid symbolic trace τ = _, ai and identity ID; the cited passage does not include the lemma’s conclusion or acceptance-characterization cases.Source: D. Stronger Characterizations · p. 59

E. Proof of Lemma 14

• The proof establishes StrEqu1–StrEqu4 through case analyses over PUID, TUID, PN, and TN actions, using earlier equalities and trace-validity conditions.For StrEqu4, it also uses induction to show relevant sequence-number state cannot change to an incompatible value between the specified actions.Source: E. Proof of Lemma 14 · pp. 59, 60, 62

APPENDIX IV UNLINKABILITY

• Unlinkability is shown by induction on valid basic symbolic traces, deriving indistinguishability for each trace.Source: APPENDIX IV UNLINKABILITY · p. 66

A. Resistance against de-synchronization attacks

• To resist de-synchronization, AKA+ requires matching sequence-number range checks to remain indistinguishable across paired traces, including after protocol actions.Generic range checks with by-one increments can break this property; the proof therefore requires equality checks and by-one increments and strengthens the invariant to track sequence-number differences.Source: A. Resistance against… · p. 66
• A synchronization invariant tracks whether a successful SUPI execution occurred since the last NSID action, accounting for cases where paired identities are temporarily unsynchronized.The added syncID state is only for the proof and is not used by the protocol; a fresh GUTI requires an honest SUPI execution that re-synchronizes both sides.Source: A. Resistance against… · p. 66

B. Strengthened induction hypothesis

• For a CS partition, Proposition 28 establishes that the defined case expression is invariant under permutation of the index list.Its proof proceeds by induction on the list length.Source: B. Strengthened induction hypothesis · p. 67

• Lemma 15 supplies derivations for valid basic symbolic traces with at most C actions NS, which are used in the main theorem’s proof.Source: B. Strengthened induction hypothesis · p. 69
• The 5G-AKA protocol is σul-unlinkable for arbitrary numbers of agents and sessions when the asymmetric encryption is IND-CCA1 secure and f and f_r, and Mac1–Mac5, jointly satisfy the PRF assumption.Source: B. Strengthened induction hypothesis · p. 69
• The proof reduces unlinkability to deriving φτ ∼ φτ for every valid symbolic trace, using Proposition 19, Assumption 1, Lemma 15, and the Restr rule.Lemma 15 supplies a derivation relating φτ with the left reveal list to φτ with the right reveal list.Source: B. Strengthened induction hypothesis · p. 69

APPENDIX V PROOF OF PROPOSITION 30

• The proof separates traces with no qualifying earlier FUID event from those containing such an event before τ1.In the latter case, it establishes that the event has a different index and occurs before τ2.Source: Appendix V · p. 71
• For one case, the proof builds the derivation piece by piece from terms that decompose into matching parts of revealτ0.It describes these parts as waved, dotted-underlined, and dashed-underlined.Source: Appendix V · p. 72
• The conclusion combines the derivations from Parts 1, 2, and 3.The proof also presents graphical representations of the execution situations for two derivations.Source: Appendix V · pp. 70, 77

APPENDIX VI PROOF OF LEMMA 15

• The proof proceeds by induction over τ, with the base case reducing to indistinguishability of the elements in Item 2 of Definition 46.For the inductive case, it assumes the derivation for the trace prefix and splits on the final action.Source: APPENDIX VI PROOF OF LEMMA 15 · p. 79

B. Case ai = PN(j, 0)

• For ai = PN(j, 0), the case proof handles MAC1 and MAC2 terms by applying their PRF-MAC axioms to replace them with fresh nonces.The derivation then combines the resulting steps with earlier derivations and the induction hypothesis.Source: B. Case ai = PN(j, 0) · pp. 80, 81, 83, 84
• Part 6 handles the sync-diff, and the proof combines (77), (79), (65), and (76) to build a derivation.Source: B. Case ai = PN(j, 0) · pp. 84, 87
• In the case ai = PN(j, 0), Part 3 uses StrEqu4, extends the derivation with (85) and (86), applies FA and Dup, then concludes by induction.The preceding step identifies Part 2 as focusing on sync-diff.Source: B. Case ai = PN(j, 0) · pp. 88–89

ai = FN(j)

• For ai = FN(j), the proof reduces Formula (91) to successive partially randomized terms, replacing GUTI ⊕ PRF outputs with fresh nonces via PRF-fr and ⊕-independence.It rewrites accept terms using Equ1 to enable the PRF-fr step, then reverses those rewrites.Source: F. Case ai = FN(j) · pp. 91–92

ai = FUντ(ID)(j)

• For ai = FUντ(ID)(j), the proof uses trace validity, revealed GUTI pairs, and Der2 to derive the required equivalence.The reveal traces coincide except on the specified pairs.Source: F. Case ai = FN(j) · pp. 92–93

ai = TUντ(ID)(j, 0)

• For ai = TUντ(ID)(j, 0), the differing terms are handled directly using the corresponding m-suci cases.The passage characterizes this handling as trivial.Source: F. Case ai = FN(j) · pp. 93–94

ai = TN(j, 0)

• For ai = TN(j, 0), distinct identities’ accept tests form a CS partition, and PRF-f and PRF-MAC3 replacements with fresh nonces complete the derivation.The partition makes the network’s answer independent of the order of the accept tests.Source: F. Case ai = FN(j) · pp. 94–95

ai = TUντ(ID)(j, 1)

• For ai = TUντ(ID)(j, 1), the proof decomposes authentication terms and replaces Mac4 terms with fresh nonces using PRF-MAC4.Structural-equivalence rewrites prepare the terms for the PRF-MAC4 step.Source: F. Case ai = FN(j) · pp. 95–97

F. Case ai = FN(j)

• For each relevant TN(j0, 0) action after τ2, the proof applies PRF-MAC4 to replace Mac4_m(nj0) with a fresh nonce.The proof first establishes that the key-identifier inputs are distinct from nj0, enabling simultaneous application of the axiom.Source: F. Case ai = FN(j) · p. 98
• Because the reasoning requires only a valid trace, it also replaces the selected MAC4 outputs with fresh nonces for trace ζ.The proof does not require τ to be a basic trace of actions.Source: F. Case ai = FN(j) · p. 98

R + PRF-MAC4

• The induction handles separate cases where the TUID event occurs before or after the latest NSID reset.The proof labels these as Case 1 and Case 2.Source: R + PRF-MAC4 · pp. 98, 100
• For one interleaving, the proof uses that an unset identifier at τa is set at τ2, implying a successful SUPI or GUTI run between those events.The passage attributes this inference to Proposition 23.Source: R + PRF-MAC4 · p. 101
• The argument for Parts 1–3 uses only trace validity, so the same proof extends the result to all valid symbolic traces, not just basic traces.The passage states this extension explicitly.Source: R + PRF-MAC4 · p. 104