A Proof of Security of a Mesh Security Architecture

The IEEE 802.11s standard is tasked to provide ways of establishing and securing a wireless mesh network. One proposal establishes a Mesh Security Architecture (MSA), with an interesting key hierarchy and full protocol definitions. This paper proves the correctness and security of the MSA proposal and its corresponding protocols. The authors also propose and prove the security of an additional protocol (An abbreviated handshake) which offers a substantial efficiency improvement in certain instances. To prove the entire architecture secure, the authors utilize Protocol Composition Logic (PCL) to prove each protocol secure.