BROWSE
Detail
Conference Paper
TLSVerifier: An Automated TLS software Verification Tool Using Model-Based Testing
Cited - time in 
Share 
Share
- Authors
- Jaedeok Lim, Minsuk Choi
- Issue Date
- 2025-12
- Citation
- International Symposium on Mobile Internet Security (MobiSec) 2025, pp.1-3
- Publisher
- KIISC
- Language
- English
- Type
- Conference Paper
- Abstract
- This paper presents TLSVerifier, an automated verification tool for the TLS protocol, which is widely employed in IoT services. As mission-critical IoT applications continue to expand across various social infrastructures, ensuring both the security and trustworthiness of data transmission and remote control has become indispensable. Among existing approaches, formal-method-based verification - which employs logical or mathematical reasoning – is regarded as the only viable solution to guarantee high assurance. However, its practical adoption has been limited due to the steep learning curve and the need for specialized expertise, and its application has been largely confined to the model(design) level rather than actual implementations. To address these limitations, this paper proposes an automated verification tool that enables users to easily perform high-assurance, formal-method-based verification of TLS implementations without prior knowledge of formal methods. The proposed tool provides both specification conformance verification based on RFC 5246 and RFC 8446, and security verification under the Dolev-Yao adversarial model.
- Keyword
- TLS formal verification, Automated verification, Model-based testing
- KSP Keywords
- Conformance verification, Data transmission, Dolev-Yao, Existing Approaches, Formal methods, Formal verification, IoT Applications, IoT services, Mathematical Reasoning, Mission-critical, Model-Based testing