Post-Compromise Security with Application-Level Key-Controls – Comprehensive Study of the 5G AKMA protocol–

“We propose PCS_AC – a new computational framework for post-compromise security (PCS), which caters not only for the traditional PCS-corruption of key material, but also for PCS adversarial controls of application-level functionality. Given our discrete measures for PCS “healing”, we mechanise PCS_AC also in symbolic models, in the two state-of-the-art protocol verifiers Proverif and Tamarin, balancing different tool-assistance aspects in each. We apply PCS_AC to the 5G procedure called AKMA (Authentication and Key Management for Application), showing new PCS-attacks therein and proposing patches, including a backwards-compatible one. We implement and test AKMA as well as of one of its PCS-driven patches, on top of Fraunhofer’s Open5GCore.”

UNDER REVIEW