Questions about the model

Open I-mpossible opened this issue 5 years ago • 0 comments

Hi,

I'm reading NAS specification TS 24.501 and have some questions regarding the 5GReasoner model representation with the corresponding description in the specification. I list my question below in the following format:

<5GReasoner model from 5GReasoner/Model Checking/nuXmv/Isolation/NAS/FSM/UE-NAS-5G.dot>

Transition to deregistered

Q1.1: I found that the specification says the UE transit to state 5GMM-DEREGISTERED and doesn't talk about current state. Where is the information about current state derived?

Q1.2: The specification also doesn't mention partial_sec_ctx and complete_sec_ctx. How are those inferred?

5GReasoner:

ue_deregistered -> ue_deregistered [label="(auth_reject | reg_reject | nwk_dereg_req | service_reject) / ue_partial_sec_ctx_exist=false, ue_complete_sec_ctx_exist=false, ueregcompleted=false, ue_reg_count = 0"]
ue_reg_inited -> ue_deregistered [label = "(auth_reject | reg_reject | nwk_dereg_req | service_reject)/ue_partial_sec_ctx_exist=false, ue_complete_sec_ctx_exist=false, ueregcompleted=false, ue_reg_count = 0"]
ue_registered -> ue_deregistered [label = "(auth_reject | reg_reject | nwk_dereg_req | service_reject) / ue_partial_sec_ctx_exist=false, ue_complete_sec_ctx_exist=false, ueregcompleted=false, ue_reg_count = 0"]
ue_dereg_inited -> ue_deregistered [label = "(auth_reject | reg_reject | nwk_dereg_req | service_reject)/ue_partial_sec_ctx_exist=false, ue_complete_sec_ctx_exist=false, ueregcompleted=false, ue_reg_count = 0"]
ue_service_inited -> ue_deregistered [label = "(auth_reject | reg_reject | nwk_dereg_req | service_reject)/ue_partial_sec_ctx_exist=false, ue_complete_sec_ctx_exist=false, ueregcompleted=false, ue_reg_count = 0"]
ue_service_inited -> ue_deregistered [label = "(auth_reject | reg_reject | nwk_dereg_req | service_reject)/ue_partial_sec_ctx_exist=false, ue_complete_sec_ctx_exist=false, ueregcompleted = false, ue_reg_count = 0"]

auth_reject specification:

5.4.1.3.5 If the AUTHENTICATION REJECT message is received by the UE, the UE shall abort any 5GMM signalling procedure, stop any of the timers T3510, T3516, T3517, T3519 or T3521 (if they were running) and enter state 5GMM-DEREGISTERED.

reg_reject specification:

5.5.1.2.5 The UE shall take the following actions depending on the 5GMM cause value received in the REGISTRATION REJECT message. #3 (Illegal UE); or #6 (Illegal ME). The UE shall set the 5GS update status to 5U3 ROAMING NOT ALLOWED (and shall store it according to subclause 5.1.3.2.2) and shall delete any 5G-GUTI, last visited registered TAI, TAI list and ngKSI. The UE shall consider the USIM as invalid for 5GS services until switching off or the UICC containing the USIM is removed. The UE shall delete the list of equivalent PLMNs and enter the state 5GMM-DEREGISTERED. ...(The remaining parts are deleted as there are many different causes)

nwk_dereg_req specification:

5.5.2.3.2 Upon receiving the DEREGISTRATION REQUEST message, if the DEREGISTRATION REQUEST message indicates "re-registration required" and the de-registration request is for 3GPP access, the UE shall perform a local release of the PDU sessions over 3GPP access, if any. The UE shall stop the timer(s) T3346, T3396, T3584 and T3585, if it is running for the current PLMN. The UE shall send a DEREGISTRATION ACCEPT message to the network and enter the state 5GMM-DEREGISTERED for 3GPP access. Furthermore, the UE shall, after the completion of the de-registration procedure, and the release of the existing NAS signalling connection, initiate an initial registration. The UE should also re-establish any previously established PDU sessions over 3GPP access.

service_reject specification:

5.6.1.5 On receipt of the SERVICE REJECT message, if the UE is in state 5GMM-SERVICE-REQUEST-INITIATED and the message is integrity protected, the UE shall reset the service request attempt counter and stop timer T3517 if running. The UE shall take the following actions depending on the 5GMM cause value received in the SERVICE REJECT message. #3 (Illegal UE); #6 (Illegal ME); The UE shall set the 5GS update status to 5U3 ROAMING NOT ALLOWED (and shall store it according to subclause 5.1.3.2.2) and shall delete any 5G-GUTI, last visited registered TAI, TAI list and ngKSI. The UE shall consider the USIM as invalid for 5GS services until switching off or the UICC containing the USIM is removed. The UE shall enter the state 5GMM-DEREGISTERED. ...(Remaining parts deleted)

Security mode control procedure

Q2.1: I didn't find ue_partial_sec_ctx_exist and ue_complete_sec_ctx_exist in the specification. Why are they included in this state transition condition?

Q2.2: In the first example, the current states include all possible states. Here only ue_reg_inited and ue_registered are used. Why are these two current states considered only and where is the information about current and next states derived?

5GReasoner:

ue_reg_inited -> ue_reg_inited [label = "sm_command & ue_partial_sec_ctx_exist=true & ue_complete_sec_ctx_exist=false & smcmd_mac_failure & sec_cap_match/sm_reject, ue_sec_ctx_updated=false"]
ue_reg_inited -> ue_reg_inited [label = "sm_command & ue_partial_sec_ctx_exist=true  & ue_complete_sec_ctx_exist=false & !smcmd_mac_failure & !sec_cap_match/sm_reject, ue_sec_ctx_updated=false"]
ue_reg_inited -> ue_reg_inited [label = "sm_command & ue_partial_sec_ctx_exist=true &  ue_complete_sec_ctx_exist=true & smcmd_mac_failure & sec_cap_match/sm_reject, ue_sec_ctx_updated=false, ue_nas_ul_count = ((ue_nas_ul_count + 1) mod 32)"]
ue_reg_inited -> ue_reg_inited [label = "sm_command & ue_partial_sec_ctx_exist=true  & ue_complete_sec_ctx_exist=true & !smcmd_mac_failure & !sec_cap_match/sm_reject, ue_sec_ctx_updated=false, ue_nas_ul_count = ((ue_nas_ul_count + 1) mod 32)"]
ue_registered -> ue_registered [label = "sm_command & smcmd_mac_failure & sec_cap_match/ sm_reject, ue_sec_ctx_updated = false, ue_complete_sec_ctx_exist=true, ue_nas_ul_count = ((ue_nas_ul_count + 1) mod 32)"]
ue_registered -> ue_registered [label = "sm_command & !smcmd_mac_failure & !sec_cap_match/ sm_reject, ue_sec_ctx_updated=false, ue_complete_sec_ctx_exist=true, ue_nas_ul_count = ((ue_nas_ul_count + 1) mod 32)"]

Specification:

5.4.2.5 If the security mode command cannot be accepted, the UE shall send a SECURITY MODE REJECT message. The SECURITY MODE REJECT message contains a 5GMM cause that typically indicates one of the following cause values: #23 UE security capabilities mismatch. #24 security mode rejected, unspecified. If the UE detects that the received Replayed UE security capabilities IE has been altered compared to the latest values that the UE sent to the network, the UE shall set the cause value to #23 "UE security capabilities mismatch".

Deregistration request

Q3.1: If the cause is not switch off, the specification specifies two current state: 5GMM-REGISTERED and 5GMM-REGISTERED-INITIATED. Where are ue_dereg_inited and ue_service_inited in 5GReasoner derived?

Q3.2: If the cause is switch off, the specification doesn't specify current state. Where are current states derived?

5GReasoner:

ue_reg_inited -> ue_deregistered [label="uederegrequested & dereg_cause_switch_off/ deregreq_switchoff"]
ue_registered -> ue_deregistered [label="uederegrequested & dereg_cause_switch_off / deregreq_switchoff, ueregcompleted=false"]
ue_dereg_inited -> ue_deregistered [label="uederegrequested & dereg_cause_switch_off / deregreq_switchoff, ueregcompleted=false"] 
ue_service_inited -> ue_deregistered [label="uederegrequested & dereg_cause_switch_off/ deregreq_switchoff, ueregcompleted=false"]

ue_reg_inited -> ue_dereg_inited [label="uederegrequested & !dereg_cause_switch_off/ deregreq_notswitchoff"]
ue_registered -> ue_dereg_inited [label="uederegrequested & !dereg_cause_switch_off/ deregreq_notswitchoff"]
ue_dereg_inited -> ue_dereg_inited [label="uederegrequested & !dereg_cause_switch_off/ deregreq_notswitchoff"]
ue_service_inited -> ue_dereg_inited [label="uederegrequested & !dereg_cause_switch_off/ deregreq_notswitchoff"]

Specification:

5.5.2.2.1 If the de-registration request is not due to switch off and the UE is in the state 5GMM-REGISTERED or 5GMM-REGISTERED-INITIATED, timer T3521 shall be started in the UE after the DEREGISTRATION REQUEST message has been sent. The UE shall enter the state 5GMM-DEREGISTERED-INITIATED. If the UE is to be switched off, the UE shall try for a period of 5 seconds to send the DEREGISTRATION REQUEST message. During this period, the UE may be switched off as soon as the DEREGISTRATION REQUEST message has been sent.

Deregistration with limited service

Q4: I didn't find information about downgrade and emergence_service in specification. Where are they derived?

5GReasoner:

ue_reg_inited -> ue_dereg_limited [label="reg_reject_limited / ueregcompleted=falses, downgrade = false, ue_emergency_service_only=true"]

Specification:

5.5.1.2.5 #12 (Tracking area not allowed). The UE shall set the 5GS update status to 5U3 ROAMING NOT ALLOWED (and shall store it according to subclause 5.1.3.2.2) and shall delete 5G-GUTI, last visited registered TAI, TAI list and ngKSI. Additionally, the UE shall reset the registration attempt counter. The UE shall store the current TAI in the list of "5GS forbidden tracking areas for regional provision of service" and enter the state 5GMM-DEREGISTERED.LIMITED-SERVICE. If the UE is operating in single-registration mode, the UE shall handle the EMM parameters EMM state, EPS update status, 4G-GUTI, TAI list, eKSI and attach attempt counter as specified in 3GPP TS 24.301 [15] for the case when the EPS attach request procedure is rejected with the EMM cause with the same value.

Jan 07 '21 14:01 I-mpossible