5G Proximity-based Service (ProSe) UE-to-Network (U2N) Relay can help a remote 5G User Equipment (UE) out of coverage connect with the network. The 3GPP committee has provided the standard Authentication and Key Agreement (AKA) protocols to achieve secure access for a Remote UE and establish a secure link between a Remote UE and a U2N Relay. However, the security of these AKA protocols is a remaining issue. At first, we present two detailed 5G ProSe AKA protocols over Control Plane (CP) and User Plane (UP) for U2N Relay communication referring to multiple related standards, then transform the security requirements for 5G ProSe U2N Relay communication as formal security properties, and provide two formal faithful security models for the 5G ProSe AKA protocols. We adopt the state-of-the-art formal verification tool Tamarin to achieve automated security analysis on two models through new proof strategies, and then find some significant and unexpected flaws. Finally, we propose corresponding measures that have least impact on standards based on the analysis on the attacks. Given that the version of Release 17 (R17) of the 3GPP standard has just been frozen, our work can provide a reference for the subsequent evolution of the protocols in 5G ProSe.

5G Vehicular to everything (5G-V2X) has grown more vigorously than ever before, and services massive vehicles can obtain provided by content providers via the network in all fields are widely acknowledged, such as listening to news channels and traffic channels. In the 5G-V2X network, content providers can provide service messages to a group of vehicles belonging to a specific area in point-to-multipoint transmission mode. However, various challenges are in front of the way when vehicles obtain multicast services due to the unique features of 5G-V2X, such as massive vehicles and strong mobility. In this paper, we present a typical vehicle multicast service model in 5G-V2X and propose a group-based multicast service authentication and data transmission scheme based on this model. In the scheme, massive vehicles within the same RAN coverage are constructed into a group and connected to the content provider to gain access to a multicast service using the distributed keys securely by the 5G home network. Subsequently, the multicast service key for protecting the multicast service data is distributed to each vehicle so that the multicast service data can be securely transmitted to vehicles in point-to-multipoint mode. The security analysis results using the formal verification tool and informal security analysis show that the proposed scheme supports the multicast services authentication and authorization, multicast service data protection, key distribution protection, anonymity, unlinkability, and protocol attack resistance. The performance analysis results regarding signaling, computational and communication overheads show that the proposed scheme outperforms other related schemes.