1 Introduction
2 Network evolution
3 Overview of future heterogeneous networks
-
The central A3C server (CA3C): This is the central authentication, authorization; accounting and cost (A3C) server in the CEP. The CA3C holds the service level of agreements (SLAs) along with the network level of agreements (NLAs), which describe the clients' terms for using the service and accessing networks, respectively.
-
The central QoS broker (CQoSB): is responsible for negotiating QoS in case of cross-CEP handover.
-
The domain A3C server (DA3C): The DA3C is responsible for handling users' service aspects. Initially, it extracts users' profile information from the CA3C and uses this information for authorizing the users' requests to access services.
-
The domain QoS broker (DQoSB): manages the resources of the attached peripheral networks with respect user preferences and network availability, it also makes a per-flow admission control decision.
-
The access router (AR): This is the link between the domain and the peripheral networks; it enforces the admission control decision, taken by the DQoSB. Since the AR acts as a relay between the mobile terminal (MT) in the peripheral network and the DA3C, using security terminology, the AR will be referred to as the authenticator (Auth).
-
The registration model: describes the procedure followed when the MT first attaches to the peripheral network. This model basically involves authenticating the MT to use the network, then enforcing the access control policies based on the MT's SLA. This article investigates different AKA protocols and proposes a novel one to be integrated with the registration model.
-
The connection initiation model: deals with the case when the MT starts a connection to a server SP. It involves authorizing the connection request in both the source and the destination networks and making sure that it complies with the pre- agreed on QoS. Once this is achieved, layer two resources in both networks are prepared to accommodate the connection.
-
The handover model: This step explains the QoS provision in the case of inter and intra administrative domain handover. This step deploys the authentication and key agreement (AKA) protocol to achieve pre-authentication and launching the security materials in the target network also in this step, the QoS- context is transferred and used by the access control mechanism in the new network.
3.1 Vertical handover vs horizontal handover
3.2 Vertical handover mechanisms in heterogeneous environments
-
MIH event services (MIES) detect changes in link layer, report them to the upper layers [20]. These events might be used as indicators for a potential handover.
-
Media independent command service (MICS) provides a set of commands that enables the upper layers (policy or mobility management layers) to control the status of the link such as switching it on or off. Additionally, some of the MICS commands enable the upper layer to ask the link layer about its status before making the handover decision, this is very crucial to support proactive, mobile-initiated handover.
-
Media independent information service (MIIS) provides information such as topology, location and link layer parameters (data rate, throughput, etc.) about different networks in the vicinity. This information, if provided beforehand, will aid the mobility management protocol on the handover' decision.
4 Secure vertical handover in heterogeneous environment
4.1 The handover key working group (HOKEY WG)
4.1.1 ERP analysis
-
Although the ERP is based on the EAP platform, it introduces new messages such as EAP-Finish/Reauth that includes a DSRK and the new domain name. This implies that, all the network entities such as the APs has to be updated or replaced to support this extra message.
-
The ERP presumes that the MT will get the domain name either implicitly when receiving the announcement or explicitly by soliciting for it. The authors believe that this step should be part of the handover procedure rather than a part of the security mechanism. Additionally, it is not clear how the MT would communicate with the EAP Re-authentication server in the target network.
-
Although, the security consideration section of the [23] provides some analysis of the protocol features, the protocol lacks formal analysis such as using a formal methods approach.
-
Implementing the proposed solution requires the network components to support EAP platform, this assumption might be feasible in heterogeneous environment, where the network infrastructure is owned by multiple operators.
4.2 The 3rd generation partnership project (3GPP)
4.3 The handover AKA protocol of the mobile ethernet
4.4 Verifying security protocols using formal methods and Casper/FDR tool
Header | Description |
---|---|
# Free variables | Defines the agents, variables and functions in the protocol |
# Processes | Represents each agent as a process |
# Protocol description | Shows all the messages exchanged between the agents |
# Specification | Specifies the security properties to be checked |
# Actual variables | Defines the real variables, in the actual system to be checked |
# Functions | Defines all the functions used in the protocol |
# System | Lists the agents participating in the actual system with their parameters instantiated |
# Intruder information | Specifies the intruder's knowledge and capabilities |
4.5 Desired security features for AKA protocols
5 Secure vertical handover in mobile ethernet
-
The authentication information server (AIS): manages the subscriber's information, the AIS corresponds to the core A3C (CA3C) server in Figure 3.
-
The authentication server (AS): authenticates the subscribers based on information retrieved from the AIS. The AS corresponds to the domain A3C (DA3C) server in Figure 3.
-
The entry points (EPs): represent one end point for wireless communication and represent APs or ARs.
-
The mobile device (M): is the MT accessing the network.
5.1 The protocol description
Notation | Description |
---|---|
M | The mobile node |
AIS | The authentication information server |
AS | The authentication server |
R1, R2 | Random values |
E(K, Msg) | Encrypted Msg by key K |
D(K, Msg) | Decrypted Msg by key K |
PRF, PRF2 | Pseudo-random function |
MS | Master secret key MS = PRF(UUK, R1 | R2) |
AK | Authentication key AK = PRF(MS, R1 | R2) |
SK | Secret key used for encryption SK = PRF2(MS, R1 | R2) |
HOAID | Handover authentication ID, an security token for speeding up the authentication in case of handover: HOAID = E(AK, R1 || R2) |
5.2 The formal verification of the mobile ethernet protocol
Secret (M, SK, [AS, EP])
specifies the SK as a secret between M, EP and AS. The lines starting with Agreement define the protocol's authenticity properties; for instance Agreement (AS, M, [AK, R1])
specifies that, the AS is correctly authenticated to M using the random number R1 and the AK. The Aliveness assertion checks the availability of the participants, e.g., the first Aliveness check Aliveness (EP, M)
states that when M completes a run of the protocol, apparently with EP, then EP has previously been running the same protocol. Note that EP may have thought he was running the protocol with someone other than M [17]. A stronger definition of the above Aliveness is specified by the Weak Agreement, for instance WeakAgreement (EP,M)
assertion could be interpreted as follows: if M has completed a run of the protocol with EP, then EP has previously been running the protocol, apparently with M. Generally, failing to meet the WeakAgreement assertions implies the failure to meet the Aliveness ones.Secret (M, AK, [AS])
Secret (AS, AK, [M])
Secret (M, SK, [AS, EP])
Agreement (AS, M, [AK, R1])
WeakAgreement (M, EP)
WeakAgreement (EP, M)
Aliveness (EP, M)
Aliveness (M, EP)
WeakAgreement (M, EP)
and Aliveness (M, EP)
assertions.0. -> m : ep, as
1a. m -> I_ep : accReq
1b. I_m -> ep : accReq
2. ep -> I_m : authReq
3. I_m -> ep : Garbage
4. ep -> I_as : Garbage, h (Garbage)
5. I_as -> ep : Garbage
6. ep -> I_m : Garbage
WeakAgreement (EP, M)
and Aliveness (EP, M)
assertions. In this attack (Figure 5), the intruder intercepts and replays the messages between M and EP as in messages 1a, 1b, 2a, 2b, and 3. Once the intruder intercepts message 3, it impersonates EP and completes running the protocol as in messages 4, 5, and 6. Thus, the mobile device will complete running the protocol believing that, it was with EP, while it was with the intruder instead.
0. -> m : ep, as
1a. m -> I_ep : accReq
1b. I_m -> ep : accReq
2a. ep -> I_m : authReq
2b. I_ep -> m : authReq
3. m -> I_ep : {m, r1, hoaid1}{sk}
4. I_ep -> as : {m, r1, hoaid1}{sk}, h({m, r1, hoaid1}{sk})
5. as -> I_ep : {r2, {r1}{ak}}{sk}
6. I_ep -> m : {r2, {r1}{ak}}{sk}
5.3 Protocol analysis and security consideration
-
Mutual entity authentication: In the first discovered attack, the intruder manages to impersonate M to run the protocol with EP. Also, in the second attack, the intruder impersonates EP to run the protocol with the mobile device. These attacks imply that, the protocol does not fulfill this security requirement. These attacks could be ascribed due to the fact that the protocol does not consider verifying the identity of the participants.
-
Mutual key authentication: the AS is authenticated to M by proving the possession of the random value R1 and the authentication key (AK). We got Casper to check this using the Secret (M, AK, [AS]) and Secret (AS, AK, [M]) assertion checks. Since no attack was found against the key secrecy, this property is met.
-
Mutual key confirmation: Casper verifies one direction of this requirement by using the decryptable (m, K) which checks if the message (m) is decryptable by the key (K). We performed a similar check after message 6 as shown in the Protocol Description heading to verify that the valid AK is possessed by the AS. If the check fails the protocol aborts. For the mutual authentication, it was presumed in [7] that, the AK along with the security context were transferred from the old AS before the protocol starts, thus there is no need to check this using Casper.
-
Key freshness: Since the keying materials are transferred from the old AS, this property could be verified by considering the key derivation functions (KDFs) for the MS = PRF (UUK, R 1|R 2), AK = PRF (MS, R 1|R 2) and SK = PRF 2(MS, R 1|R 2) in the initial AKA protocol. We could claim that, this property is guaranteed since fresh random values R1, R2 are included in the KDFs of the MS, AK and SK keys.
-
Unknown key share: The second, discovered attack implies that the UKS was not met. Despite of the fact that, the mobile device (M) and the AS share the AK, the M mistakenly believes that the intruder holds this key as well. Casper/FDR indicates this fact by highlighting an attack against the
WeakAgreement(EP,M)
andAliveness(EP,M)
assertions in the # Specifications header. -
Key compromise impersonation resilience: this property could be modeled by specifying the long-term keys as crackable and then checking the authenticity assertions. By specifying the MS key to crackable and checking the
Agreement(AS, M, [AK, R1])
assertion, Casper verifies no breach against this authenticity feature.
6 The proposed solution
6.1 Defining the security system
6.2 The key hierarchy
6.3 The initial version of the protocol
Notation | Description |
---|---|
MT | The mobile terminal |
SrcAuth | Is the access router in the source peripheral network |
DesAuth | Is the access router in the destination peripheral network |
AuthID | The authenticator unique ID has the format AuthID@domainname |
SrcDA3C | The DA3C server in the source domain |
DesDA3C | The DA3C server in the destination domain |
CA3C | Core-endpoint entity, which has QoS and security related responsibilities |
Srcse1(SrcDA3C) | Pre-shared secret key between the CA3C and the SrcDA3C |
Desse1(DesDA3C) | Pre-shared secret key between the CA3C and the DesDA3C |
Srcse2(SrcAuth) | Pre-shared secret key between the SrcDA3C and the authenticator (SrcAuth) |
Desse2(DesAuth) | Pre-shared secret key between the DesDA3C and the authenticator (DesAuth) |
uk(MT) | Unique secret key shared between the CA3C and the MT |
DSMS | Domain specific- master key DSMS= F1 (uk(MT), seq1, auth-domain name) |
SrcAK, DesAK | The authentication key in the source and destination domains |
SrcSK, DesSK | The secret key in the source and destination networks, respectively. These are used to encrypt the connections between the MT and the authenticators |
F1, F2, F3 | Irreversible key derivation functions |
InitAuth flag | A flag set only in the initial authentication. In case of handover, this flag will not be set |
HoAckm | Joining/handover acknowledgement message used by the DA3C server to inform the CA3C in the CEP about a successful authentication |
seq1, seq2 | Sequence numbers |
{m}
K
| Encrypting the message (m) using the key (K) |
6.3.1 Formal verification
Secret (MT, DesAK, [DesDA3C])
Secret (DesAuth, DesSK, [MT, DesDA3C])
Agreement (MT, DesDA3C, [seq2])
Agreement (DesDA3C, MT, [seq1, DesAK])
WeakAgreement (MT, DesAuth)
WeakAgreement (DesAuth, MT)
WeakAgreement (DesAuth, DesDA3C)
WeakAgreement (DesDA3C, DesAuth)
Aliveness (MT, DesAuth)
Aliveness (DesAuth,MT)
Secret(DesAuth, DesSK,[MT, DesDA3C])
assertion, where the Intruder launches a replay attack and eventually manages to get the secret key (SK). The message sequence involved in the attack is given below.0. -> mt : srcAuth, desAuth, srcDA3C
1a. desAuth -> I_mt : adv, desDA3C
1b. I_desAuth -> mt : adv, desDA3C
2a. mt -> I_desAuth : accReq
2b. I_mt -> desAuth : accReq
3a. desAuth -> I_mt : authReq
3b. I_desAuth -> mt : authReq
4a. mt -> I_srcAuth : {SEQ1, authID, mt,
initauth}{srcSK}
4b. I_mt -> srcAuth : {SEQ1, authID, mt,
initauth}{srcSK}
5a. srcAuth -> I_srcDA3C : SEQ1, authID, mt,
initauth
5b. I_srcAuth -> srcDA3C : SEQ1, authID, mt,
initauth
6a. srcDA3C -> I_ca3c : {SEQ1, authID, mt,
initauth}{Srcse1(srcDA3C)}
6b. I_srcDA3C -> ca3c : {SEQ1, authID, mt,
initauth}{Srcse1(srcDA3C)}
7a. ca3c -> I_desDA3C : {DSMS, {SEQ1, authID, mt, initauth}{DSMS}}{Desse1(desDA3C)}
7b. I_ca3c -> desDA3C : {DSMS, {SEQ1, authID, mt, initauth}{DSMS}}{Desse1(desDA3C)}
8a. desDA3C -> I_desAuth : {SEQ2, SEQ1}{DesAK}
9a. I_desAuth -> mt : {SEQ2, SEQ1}{DesAK}
10a. mt -> I_desAuth : {SEQ2}{DesAK}
8b. I_desDA3C -> desAuth : {SEQ2, SEQ1}{DesAK}
9b. desAuth -> I_mt : {SEQ2, SEQ1}{DesAK}
10b. I_mt -> desAuth : {SEQ2}{DesAK}
11a. I_desAuth -> desDA3C : {SEQ2}{DesAK}
11b. desAuth -> I_desDA3C : {SEQ2}{DesAK}
12. desDA3C -> I_ca3c : {hoAckm}{Desse1(desDA3C)}
13a. desDA3C -> I_desAuth : DesSK
13b. I_desDA3C -> desAuth : DesSK
14. desAuth -> I_mt : {accRes}{DesSK}
The intruder knows DesSK
-
The intruder intercepts the messages between the MT and the DesAuth as in messages 1a, 1b, 2a, 2b, 3a, and 3b. The MT responds by starting the protocol in the normal sequence and sends message 4a.
-
The intruder passively intercepts and replays the messages in the destination domain as messages (4a, 4b, 5a, 5b, 6a, 6b, 7a, and 7b). Upon intercepting message 8a, the intruder starts a new session and thus the intruder plays two roles as follows:
-
To complete the protocol and close it stealthy, the intruder passes the DesSK in message 13b to the DesAuth, which composes the AccReq towards the MT in message 14. This message will be blocked by the intruder.
WeakAgreement (Des- Auth, DesDA3C)
assertion, where the Intruder launches a replay attack and successfully impersonates the DesAuth. The message sequence involved in the attack is given below.0. -> mt : srcAuth, desAuth, srcDA3C
1a. desAuth -> I_mt : adv, desDA3C
1b. I_desAuth -> mt : adv, desDA3C
2a. mt -> I_desAuth : accReq
2b. I_mt -> desAuth : accReq
3a. desAuth -> I_mt : authReq
3b. I_desAuth -> mt : authReq
4a. mt -> I_srcAuth : {SEQ1, authID, mt,
initauth}{srcSK}
4b. I_mt -> srcAuth : {SEQ1, authID, mt,
initauth}{srcSK}
5a. srcAuth -> I_srcDA3C : SEQ1, authID, mt,
initauth
5b. I_srcAuth -> srcDA3C : SEQ1, authID, mt,
initauth
6a. srcDA3C -> I_ca3c : {SEQ1, authID, mt,
initauth}{Srcse1(srcDA3C)}
6b. I_srcDA3C -> ca3c : {SEQ1, authID, mt,
initauth}{Srcse1(srcDA3C)}
7a. ca3c -> I_desDA3C : {DSMS, {SEQ1, authID,
mt, initauth}{DSMS}}{Desse1(desDA3C)}
7b. I_ca3c -> desDA3C : {DSMS, {SEQ1, authID,
mt, initauth}{DSMS}}{Desse1(desDA3C)}
8. desDA3C -> I_desAuth : {SEQ2, SEQ1}{DesAK}
9. I_desAuth -> mt : {SEQ2, SEQ1}{DesAK}
10. mt -> I_desAuth : {SEQ2}{DesAK}
11. I_desAuth -> desDA3C : {SEQ2}{DesAK}
12. desDA3C -> I_ca3c : {hoAckm}{Desse1(desDA3C)}
13. desDA3C -> I_desAuth : DesSK
6.4 The second version protocol
Agreement(DesDA3C, MT, [seq1, DesAK])
assertion.
0. -> mt : srcAuth, desAuth, srcDA3C
1a. desAuth -> I_mt : adv, desDA3C
1b. I_desAuth -> mt : adv, desDA3C
2a. mt -> I_desAuth : accReq
2b. I_mt -> desAuth : accReq
3a. desAuth -> I_mt : authReq
3b. I_desAuth -> mt : authReq
4a. mt -> I_srcAuth : {SEQ1, authID, mt,
initauth}{srcSK}
4b. I_mt -> srcAuth : {SEQ1, authID, mt,
initauth}{srcSK}
5a. srcAuth -> I_srcDA3C : {SEQ1, authID, mt,
initauth}{Srcse2(srcAuth)}
5b. I_srcAuth -> srcDA3C : {SEQ1, authID, mt,
initauth}{Srcse2(srcAuth)}
6a. srcDA3C -> I_ca3c : SEQ1, authID, mt,
initauth
6b. I_srcDA3C -> ca3c : SEQ1, authID, mt,
initauth
7a. ca3c -> I_desDA3C : DSMS, {SEQ1, authID, mt, initauth}{DSMS}
7b. I_ca3c -> desDA3C : DSMS, {SEQ1, authID,
Mallory, initauth}{DSMS}
8a. desDA3C -> I_desAuth : {{SEQ2, SEQ1}{DesAK}}
{Desse2(desAuth)}
8b. I_desDA3C -> desAuth : {{SEQ2, SEQ1}{DesAK}}
{Desse2(desAuth)}
9a. desAuth -> I_mt : {SEQ2, SEQ1}{DesAK}
9b. I_desAuth -> mt : {SEQ2, SEQ1}{DesAK}
10a. mt -> I_desAuth : {SEQ2}{DesAK}
10b. I_mt -> desAuth : {SEQ2}{DesAK}
11a. desAuth -> I_desDA3C : {{SEQ2}{DesAK}}
{Desse2(desAuth)}
11b. I_desAuth -> desDA3C : {{SEQ2}{DesAK}}
{Desse2(desAuth)}
12. desDA3C -> I_ca3c : hoAckm
13a. desDA3C -> I_desAuth : {DesSK}{Desse2
(desAuth)}
13b. I_desDA3C -> desAuth : {DesSK}{Desse2
(desAuth)}
14a. desAuth -> I_mt : {accRes}{DesSK}
14b. I_desAuth -> mt : {accRes}{DesSK}
-
Similar to the previous attacks, the intruder intercepts the preliminary messages between the MT and the authenticator of the destination networks as in messages (1a-3b). Then, it intercepts and replays messages (4a-7a) in the source domain.
-
The intruder fakes message 7a by replacing the MT with its identity (Mallory), and passes it to the DesDA3C as message 7b. The DesDA3C, mistakenly believing that the CA3C has identified Mallory, generates the DesAK and composes message 8a, which will be intercepted by the intruder.
-
The intruder intercepts and replays messages (9a, 9b, 10a, 10b, 11a, and 11b) in the destination domain. Once the DesDA3C verifies the contents of message 11b, it mistakenly authenticates the intruder, acknowledges the successful authentication and sends the secret key DesSK as messages 12, 13a, respectively. However, these messages will be blocked by the intruder.
-
At this stage, the intruder wants to finish the attack stealthy, so it passes the intercepted DesSK to the DesAuth to generate the AccRes message and finishes the protocol in message 13b, 14a, and 14b.
6.5 The final protocol
6.6 AKA protocol formal verification
-
Mutual entity authentication: Casper provides no direct specification to model this property. In order to show how our protocol could meet this requirement, we explicitly, and by considering the protocol transactions, could argue that this requirement could be met to a certain extent in our protocol. When making the initial contract, the MT and the CA3C share a unique key uk(MT), which acts as the root in the key hierarchy and is never used for encryption. We assume this key has been derived by running a KDF over identity-related information of the MT and the CA3C, and since it is never exposed and is stored in the MT's SIM card, it is unlikely for an intruder to get that key; thus, possessing this key verifies the identity of the party.
-
Mutual key authentication: the mutual authentication between the MT and the DesDA3C is based on the secrecy of the freshly derived DesAK. We got Casper to check this using the Secret (MT, DesAK, [DesDA3C]) and Secret (DesDA3C, DesAK, [MT]) assertion checks. Since Casper/FDR found no attacks against the secrecy of the DesAK, this implies that, only other party apart form the intended ones could possess this key.
-
Mutual key confirmation: Casper verifies this requirement by using the DECRYPTABLE (m, K) which checks if the message (m) is decryptable by the key (K). We performed a similar check after messages 9 and 11 as shown in the Protocol Description heading to verify that the valid AK is possessed by the other party. If any of the checks fails the protocol aborts.
-
Key freshness: since there is no direct function with Casper to simulate this feature, we included a freshly generated sequence seq1 in the KDF as explained in the key derivation subsection; thus the fact that Casper does not detect any attack on the secrecy of the secret and AKs implies that key freshness is not violated.
-
Unknown-key share resilience: we check this property using the Aliveness assertions. Additionally, we could address this attack by making a binding between the keys and the identity of the parties. The proposed AKA protocol has achieved this by the identity of the MT and the CA3C in the derivation of the uk(MT). Also, the authenticator's ID and the domain name are included in the KDFs of the Secret and AKs.
-
Key compromise impersonation resilience: this property could be modeled by specifying the long-term keys as crackable and then checking the authenticity assertions.
6.7 Protocol analysis and security consideration
The security property | The AKA of mobile ethernet | Initial version | Second version | Refined proposal |
---|---|---|---|---|
Mutual entity authentication | No | Yes | Yes | Yes |
Mutual key authentication/keys' secrecy | Yes | No | Yes | Yes |
Mutual key confirmation | Yes | No | Yes | Yes |
Key freshness | Yes | Yes | Yes | Yes |
Unknown-key share resilience | No | No | No | Yes |
Key compromise impersonation resilience | Yes | Yes | Yes | Yes |
Defining key scope | No | Yes | Yes | Yes |
7 Further work
8 Conclusion
Appendix A: Code for formal analysis of the handover AKA protocol for mobile ethernet
M: MobileTerminal
EP : AccessRouterAuthenticator
AS : DomainA3CServer
AuthID : Identity
Initauth : Flags
R1 : initialSeq
R2 : Sequence
HOAID1: OldToken
HOAID2: NewToken
AK : AuthenticationKeys
SK : SecretKeys
MS: Domainspecifickey
F: AuthenticationKeys × initialSeq × Sequence ->
NewToken
h : HashFunction
AccReq, AccRes,AuthReq, Adv: Messages
HoAckm : AcknowledgementMessage
InverseKeys = (AK, AK), (SK, SK), (MS, MS), (F,F)
INITIATOR(M, EP, R1,AuthID,Initauth, AccReq, AuthReq, MS, AK, SK, HOAID1)
Authenticator(EP,AS, AuthReq, Adv,AccRes)
DomainSERVER(AS,M, R2, HoAckm, MS, AK, SK, HOAID1)
0. -> M : EP, AS
1. M -> EP: AccReq
2. EP -> M : AuthReq
3. M -> EP : {M,R1, HOAID1}{SK}%w
4. EP -> AS : w%{M,R1,HOAID1}{SK}, h(w%{M,R1,
HOAID1}{SK})
5. AS -> EP: {R2,{R1}{AK}%z}{SK}%v
6. EP -> M : v%{R2,{R1}{AK}%z}{SK}
Secret (M,AK,[AS])
Secret (AS,AK,[M])
Secret (M,SK,[AS, EP])
Agreement (AS, M, [AK, R1])
WeakAgreement (M, EP)
WeakAgreement (EP,M)
Aliveness (EP, M)
Aliveness (M, EP)
m, Eve: MobileTerminal
ep : AccessRouterAuthenticator
as : DomainA3CServer
Authid : Identity
InitAuth : Flags
hoaid1: OldToken
hoaid2: NewToken
r1 : initialSeq
r2 : Sequence
ak : AuthenticationKeys
sk : SecretKeys
ms: Domainspecifickey
accReq, accRes,authReq, adv: Messages
hoackm : AcknowledgementMessage
InverseKeys = (ms, ms), (ak, ak), (sk, sk)
symbolic F
INITIATOR (m,ep, r1,Authid,InitAuth, accReq, authReq, ms, ak,sk,hoaid1)
Authenticator (ep, as, authReq,adv, accRes)
DomainSERVER (as,m, r2,hoackm, ms,ak,sk,hoaid1)
Intruder = Mallory
IntruderKnowledge = m, as, Mallory, Authid, ep
Crackable = Domainspecifickey
Appendix B: Code for formal analysis of the proposal handover AKA protocol
MT: Agent
SrcAuth : SrcAccessRouterAuthenticator
DesAuth : DesAccessRouterAuthenticator
SrcDA3C : SrcDomainA3CServer
DesDA3C : DesDomainA3CServer
CA3C : CentralA3CServer
AuthID : Identity
Initauth : Flags
seq1 : initialSeq
seq2 : Sequence
Srcse1 : SrcDomainA3CServer-> PresharedKeys
Desse1 : DesDomainA3CServer-> PresharedKeys
Srcse2 : SrcAccessRouterAuthenticator-> PresharedKeys
Desse2 : DesAccessRouterAuthenticator-> PresharedKeys
uk : Agent-> PresharedKeys
SrcAK, DesAK : AuthenticationKeys
SrcSK, DesSK : SecretKeys
DSMS: Domainspecifickey
AccReq, AccRes,AuthReq, Adv: Messages
HoAckm : AcknowledgementMessage
F1: PresharedKeys × initialSeq × Identity
-> Domainspecifickey
F2: initialSeq × Domainspecifickey ->
AuthenticationKeys
F3: initialSeq × Domainspecifickey × Identity ->
SecretKeys
InverseKeys = (SrcAK, SrcAK), (uk, uk), (SrcSK, SrcSK),
(DSMS, DSMS), (Srcse1,Srcse1),(Srcse2, Srcse2),
(Desse1,Desse1),(Desse2, Desse2),(DesAK,DesAK),(DesSK, DesSK), (F1, F1), (F2,F2),(F3,F3)
INITIATOR(MT,seq1,AuthID,Initauth, SrcAK, SrcSK, AccReq) knows uk(MT)
SrcAuthenticator(SrcAuth,MT,SrcDA3C,SrcSK, AuthReq)
knows Srcse2(SrcAuth)
DesAuthenticator(DesAuth,MT, DesDA3C, AuthReq, Adv,
AccRes) knows Desse2(DesAuth)
SrcAAASERVER(SrcDA3C,CA3C, SrcAuth, SrcAK, SrcSK) knows Srcse1(SrcDA3C), Srcse2(SrcAuth)
DesAAASERVER(DesDA3C,CA3C,DesAuth, seq2,HoAckm) knows Desse1(DesDA3C), Desse2(DesAuth)
CentralSERVER(CA3C, SrcDA3C, DesDA3C) knows
Srcse1(SrcDA3C), Desse1(DesDA3C), uk(MT)
0. -> MT : SrcAuth, DesAuth, SrcDA3C
1. DesAuth -> MT :Adv, DesDA3C
2. MT -> DesAuth: AccReq
3. DesAuth -> MT : AuthReq
4. MT -> SrcAuth : {seq1,AuthID, MT, Initauth}{SrcSK}
5. SrcAuth -> SrcDA3C : {seq1,AuthID, MT, Initauth}{
Srcse2(SrcAuth)}
6. SrcDA3C -> CA3C : {seq1,AuthID, MT, Initauth}{
Srcse1(SrcDA3C)}
7. CA3C -> DesDA3C : {DSMS, {seq1,AuthID, MT, Initauth}
{DSMS}}{Desse1(DesDA3C)}
8. DesDA3C -> DesAuth: {({seq2, seq1}{DesAK}%z)%x}
{Desse2(DesAuth)}
9. DesAuth -> MT : x%({seq2, seq1}{DesAK}%z)
10. MT -> DesAuth : ({seq2}{DesAK}%y)%q
11. DesAuth -> DesDA3C: {(q% seq2}{DesAK})%y}
{Desse2(DesAuth)}
12. DesDA3C -> CA3C : {HoAckm}{Desse1(DesDA3C)}
13. DesDA3C -> DesAuth :{DesSK}{Desse2(DesAuth)}
14. DesAuth -> MT : {AccRes}{DesSK}
Secret(MT,DesAK,[DesDA3C])
Secret(DesAuth,DesSK,[MT, DesDA3C])
Secret(SrcAuth,SrcSK,[MT, SrcDA3C])
Agreement(MT, DesDA3C, [seq2])
Agreement(DesDA3C, MT, [seq1, DesAK])
WeakAgreement(MT, DesAuth)
WeakAgreement(DesAuth, MT)
WeakAgreement(DesAuth, DesDA3C)
WeakAgreement(DesDA3C, DesAuth)
Aliveness(MT, DesAuth)
Aliveness(DesAuth, MT)
mt, Mallory: Agent
srcAuth : SrcAccessRouterAuthenticator
desAuth : DesAccessRouterAuthenticator
srcDA3C : SrcDomainA3CServer
desDA3C : DesDomainA3CServer
ca3c : CentralA3CServer
authID : Identity
initauth : Flags
SEQ1 : initialSeq
SEQ2 : Sequence
srcAK, desAK : AuthenticationKeys
srcSK, desSK : SecretKeys
dsms: Domainspecifickey
accReq : AccessReqmessages
accRes: AccessResmessages
authReq: Authmessage
adv:AdvMessages
hoAckm : AcknowledgementMessage
InverseKeys = (dsms, dsms), (srcAK, srcAK), (srcSK, srcSK), (desAK, desAK), (desSK, desSK)
symbolic Srcse1,Srcse2,Desse1,Desse2,uk, F1, F2, F3
INITIATOR(mt,SEQ1,authID,initauth, srcAK, srcSK,accReq)
SrcAuthenticator(srcAuth, mt,srcDA3C,srcSK, authReq)
DesAuthenticator(desAuth, mt, desDA3C, authReq,adv, accRes)
SrcAAASERVER(srcDA3C,ca3c,srcAuth, srcAK, srcSK)
DesAAASERVER(desDA3C,ca3c,desAuth, SEQ2,hoAckm)
CentralSERVER(ca3c, srcDA3C, desDA3C)
Intruder = Mallory
IntruderKnowledge = {mt, srcDA3C,desDA3C, Eve, ca3c, authID, srcAuth,desAuth, uk(Eve)}
Crackable = PresharedKeys
Crackable = Domainspecifickey