On protocol security via computability logic

Experience in cybersecurity shows that communication protocol design is exceptionally error-prone: security weaknesses often arise less from defects in cryptographic primitives than from flawed protocols, owing to the incorrect logical interplay among agents and potential adversaries in a network. Empirical evidence likewise suggests that `verification is only as sound as the language we used for it'. We propose computability logic (CoL) as a formal foundation for modelling, analysing and verifying secure communication protocols by treating specifications as interactive games between computational agents. We argue that CoL naturally captures protocol dynamics and formally identifies structural invariants that underlie classes of vulnerabilities and attacks. Moreover, its constructive character favours automated strategy extraction and synthesis of correct-by-construction executable artefacts from verification proofs while preserving the game-theoretic, interactive nature of protocols. We consider a CL4-based case study we presented at ITASEC 2026 to show the feasibility of our approach on representative protocol patterns, and outline theoretical and practical directions for extending the method to broader protocol families. This work in progress aims to advance logical verification methods for real-world secure communication.