Paper 2026/1961
A Formal Security Analysis of a MACsec Key Agreement Protocol Using Tamarin
, TUBITAK BILGEMAbstract
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.
- Keywords
- TamarinMACsecMKACryptographic prothocolsFormal analysis
- Contact author(s)
- halil kaplan @ tubitak gov tr
- History
- 2026-09-13: approved
- 2026-09-10: received
- See all versions
- Short URL
- https://ia.cr/2026/1961
- License
-
CC BY
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}
}
