Symbolic Execution of Security Protocol Implementations: Handling Cryptographic Primitives


Mathy Vanhoef and Frank Piessens, imec-DistriNet, KU Leuven


We show how to efficiently simulate cryptographic primitives during symbolic execution. This allows analysis of security protocol implementations, and revealed several flaws in implementations of WPA2's 4-way handshake.

Traditional symbolic execution engines cannot handle cryptographic primitives, because analyzing them results in complex symbolic expressions that cannot be handled by the SMT solver. We prevent this by simulating their behaviour under the Dolev-Yao model. This enables efficient symbolic execution of security protocols implementations, making it possible to detect common programming mistakes in them. We also show how to detect misuse of cryptographic primitives. That is, we can detect trivial timing side-channels, and we can identify decryption oracles where unauthenticated decrypted data influences the program's behaviour. We apply our technique on three client-side implementations of WPA2's 4-way handshake. This uncovered timing side-channels when verifying authentication tags, a denial-of-service attack, a stack-based buffer overflow, and also revealed a non-trivial decryption oracle. We confirmed all vulnerabilities in practice, and discuss them in detail.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {220590,
author = {Mathy Vanhoef and Frank Piessens},
title = {Symbolic Execution of Security Protocol Implementations: Handling Cryptographic Primitives},
booktitle = {12th {USENIX} Workshop on Offensive Technologies ({WOOT} 18)},
year = {2018},
address = {Baltimore, MD},
url = {},
publisher = {{USENIX} Association},