Paper 2026/1961 Original: eprint.iacr.org/2026/1961 ↗
A Formal Security Analysis of a MACsec Key Agreement Protocol Using Tamarin
Abstract
MACsec Key Agreement (MKA) is the IEEE 802.1X key-management protocol used to establish and maintain Secure Associations for MACsec deployments. Although MKA is widely deployed, machine-checked analyses of its core key-agreement logic remain scarce. This paper presents a formal analysis of a simplified two-party MKA exchange using the Tamarin prover. We model the initial session establishment and a subsequent rekey round, and verify secrecy, authentication, agreement, ordering, and freshness properties. The analysis confirms these guarantees under a Dolev--Yao adversary when the pre-shared Connectivity Association Key (CAK) is not compromised. We also identify a structural weakness: a malicious or compromised Key Server can inject an arbitrary Secure Association Key (SAK) that the Server accepts. This finding clarifies the trust assumptions of MKA and motivates additional verification or binding mechanisms for partially trusted deployments.
Metadata
- Available format(s)
PDF- Category
- Cryptographic protocols
- Publication info
- Preprint.
- History
- 2026-09-10: last updated
- 2026-09-10: published
- Short URL
- https://ia.cr/2026/1961
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2026/1961,
author = {Halil İbrahim Kaplan},
title = {A Formal Security Analysis of a MACsec Key Agreement Protocol Using Tamarin},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/1961},
year = {2026},
url = {https://eprint.iacr.org/2026/1961}
}