{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T19:42:08Z","timestamp":1768419728664,"version":"3.49.0"},"reference-count":28,"publisher":"MDPI AG","issue":"5","license":[{"start":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T00:00:00Z","timestamp":1746489600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computers"],"abstract":"<jats:p>The validation of security protocols remains a complex and critical task in the cybersecurity landscape, often relying on labor-intensive testing or formal verification techniques with limited scalability. In this paper, we explore property-based testing (PBT) as a powerful yet underutilized methodology for the automated validation of security protocols. PBT enables the generation of large and diverse input spaces guided by declarative properties, making it well-suited to uncover subtle vulnerabilities in protocol logic, state transitions, and access control flows. We introduce the principles of PBT and demonstrate its applicability through selected use cases involving authentication mechanisms, cryptographic APIs, and session protocols. We further discuss integration strategies with existing security pipelines and highlight key challenges such as property specification, oracle design, and scalability. Finally, we outline future research directions aimed at bridging the gap between PBT and formal methods, with the goal of advancing the automation and reliability of secure system development.<\/jats:p>","DOI":"10.3390\/computers14050179","type":"journal-article","created":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T11:38:06Z","timestamp":1746531486000},"page":"179","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Property-Based Testing for Cybersecurity: Towards Automated Validation of Security Protocols"],"prefix":"10.3390","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8872-5721","authenticated-orcid":false,"given":"Manuel J. C. S.","family":"Reis","sequence":"first","affiliation":[{"name":"Engineering Department and IEETA, University of Tr\u00e1s-os-Montes e Alto Douro, Quinta de Prados, 5000-801 Vila Real, Portugal"}]}],"member":"1968","published-online":{"date-parts":[[2025,5,6]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"632154","DOI":"10.1155\/2014\/632154","article-title":"A Model Based Security Testing Method for Protocol Implementation","volume":"2014","author":"Fu","year":"2014","journal-title":"Sci. World J."},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Goldstein, H., Cutler, J.W., Dickstein, D., Pierce, B.C., and Head, A. (2024, January 14\u201320). Property-Based Testing in Practice. Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering, Lisbon, Portugal.","DOI":"10.1145\/3597503.3639581"},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Chen, Z., Rizkallah, C., O\u2019Connor, L., Susarla, P., Klein, G., Heiser, G., and Keller, G. (2022, January 6\u20137). Property-Based Testing: Climbing the Stairway to Verification. Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, Auckland, New Zealand.","DOI":"10.1145\/3567512.3567520"},{"key":"ref_4","unstructured":"Bates, M., and Near, J.P. (2024). DT-SIM: Property-Based Testing for MPC Security. arXiv."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/263244.263267","article-title":"Property-based testing: A new approach to testing for assurance","volume":"22","author":"Fink","year":"1997","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Beurdouche, B., Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.-Y., and Zinzindohoue, J.K. (2015, January 17\u201321). A Messy State of the Union: Taming the Composite State Machines of TLS. Proceedings of the 2015 IEEE Symposium on Security and Privacy, San Jose, CA, USA.","DOI":"10.1109\/SP.2015.39"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"853","DOI":"10.3390\/jcp4040040","article-title":"A Comprehensive Review and Assessment of Cybersecurity Vulnerability Detection Methodologies","volume":"4","author":"Bennouk","year":"2024","journal-title":"J. Cybersecurity Priv."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/2090147.2094081","article-title":"SAGE: Whitebox Fuzzing for Security Testing: SAGE has had a remarkable impact at Microsoft","volume":"10","author":"Godefroid","year":"2012","journal-title":"Queue"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"106700","DOI":"10.1016\/j.infsof.2021.106700","article-title":"Challenges and solutions when adopting DevSecOps: A systematic review","volume":"141","author":"Rajapakse","year":"2022","journal-title":"Inf. Softw. Technol."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"86","DOI":"10.30574\/wjaets.2023.8.2.0078","article-title":"Software security models and frameworks: An overview and current trends","volume":"8","author":"Korir","year":"2023","journal-title":"World J. Adv. Eng. Technol. Sci."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"1891","DOI":"10.21105\/joss.01891","article-title":"Hypothesis: A new approach to property-based testing","volume":"4","author":"MacIver","year":"2019","journal-title":"J. Open Source Softw."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Vazou, N., Bakst, A., and Jhala, R. (2015, January 1\u20133). Bounded refinement types. Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, Vancouver, BC, Canada.","DOI":"10.1145\/2784731.2784745"},{"key":"ref_14","unstructured":"Zalewski, M. (2011). The Tangled Web: A Guide to Securing Modern Web Applications, No Starch Press."},{"key":"ref_15","unstructured":"De Ruiter, J., and Poll, E. (2015, January 12\u201314). Protocol State Fuzzing of {TLS} Implementations. Proceedings of the 24th USENIX Security Symposium (USENIX Security 15), Washington, DC, USA. Available online: https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/de-ruiter."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"805","DOI":"10.1109\/TSE.2016.2532875","article-title":"A Survey on Metamorphic Testing","volume":"42","author":"Segura","year":"2016","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_17","unstructured":"Zeller, A., Gopinath, R., B\u00f6hme, M., Fraser, G., and Holler, C. (2025, April 23). The Fuzzing Book. Available online: https:\/\/www.fuzzingbook.org\/."},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Hu, V.C., Ferraiolo, D.F., and Kuhn, D.R. (2006). Assessment of Access Control Systems, National Institute of Standards and Technology.","DOI":"10.6028\/NIST.IR.7316"},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"1472","DOI":"10.1002\/spe.3199","article-title":"Declarative static analysis for multilingual programs using CodeQL","volume":"53","author":"Youn","year":"2023","journal-title":"Softw. Pract. Exp."},{"key":"ref_20","unstructured":"MacIver, D.R., and Donaldson, A.F. (2020, January 15\u201317). Test-Case Reduction via Test-Case Generation: Insights from the Hypothesis Reducer (Tool Insights Paper). Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP 2020), Berlin, Germany."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Cankar, M., Petrovic, N., Pita Costa, J., Cernivec, A., Antic, J., Martincic, T., and Stepec, D. (2023, January 15\u201319). Security in DevSecOps: Applying Tools and Machine Learning to Verification and Monitoring Steps. Proceedings of the Companion of the 2023 ACM\/SPEC International Conference on Performance Engineering, Coimbra, Portugal.","DOI":"10.1145\/3578245.3584943"},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/s10207-024-00914-z","article-title":"DevSecOps practices and tools","volume":"24","author":"Prates","year":"2024","journal-title":"Int. J. Inf. Secur."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Claessen, K., and Hughes, J. (2000, January 18\u201321). QuickCheck: A lightweight tool for random testing of Haskell programs. Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, Montreal, QC, Canada.","DOI":"10.1145\/351240.351266"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"2487","DOI":"10.1109\/TSE.2019.2953066","article-title":"Grammar Based Directed Testing of Machine Learning Systems","volume":"47","author":"Udeshi","year":"2021","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_25","unstructured":"Huang, L., Zhao, P., Chen, H., and Ma, L. (2024). Large Language Models Based Fuzzing Techniques: A Survey. arXiv."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Cachin, C., Guerraoui, R., and Rodrigues, L. (2011). Introduction to Reliable and Secure Distributed Programming, Springer.","DOI":"10.1007\/978-3-642-15260-3"},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.37256\/aie.5120243220","article-title":"Software Test Case Generation Using Natural Language Processing (NLP): A Systematic Literature Review","volume":"5","author":"Ayenew","year":"2024","journal-title":"Artif. Intell. Evol."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"102622","DOI":"10.1016\/j.lindif.2024.102622","article-title":"Experimental evidence for rule learning as the underlying source of the item-position effect in reasoning ability measures","volume":"118","author":"Schweizer","year":"2025","journal-title":"Learn. Individ. Differ."}],"container-title":["Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-431X\/14\/5\/179\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:27:59Z","timestamp":1760030879000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-431X\/14\/5\/179"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,6]]},"references-count":28,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2025,5]]}},"alternative-id":["computers14050179"],"URL":"https:\/\/doi.org\/10.3390\/computers14050179","relation":{},"ISSN":["2073-431X"],"issn-type":[{"value":"2073-431X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,6]]}}}