In this paper, we present a methodology for performing thorough analysis of TLS protocol implementations using dynamic symbolic execution. This method explores all possible inputs by treating entire messages as symbolic using KLEE. We are able to analyse the message parsing logic in detail, showing fulfilment of requirements from the protocol specification. This has previously not been performed for whole messages in complex protocols such as TLS. We tackle several problems that cause state space explosion by providing appropriate abstractions of implementation primitives. Additionally, we explore how protocol design choices impact the feasibility of analysis and argue for a strict TLS specification. We have applied our method to the ServerHello message parsing in several versions of the WolfSSL TLS 1.3 implementation. Our analysis revealed two vulnerabilities in the client implementation which were both assigned CVEs, one of them marked as high severity.