Abstract Interpretation for Proving Secrecy Properties in Security Protocols
Kamel Adi, Mourad Debbabi · Electronic Notes in Theoretical Computer Science · 2003
A cryptographic protocol is a distributed program that can be executed by several actors. Since several runs of the protocol within the same execution are allowed, models of cryptoprotocols are often infinite. Sometimes, for verification purposes, only a finite and approximated model is needed. For this, we consider the problem of computing such an approximation and we propose to simulate the required partial execution in an abstract level. More precisely, we define an abstract finite category G a as an abstract game semantics for the SPC calculus, a dedicated calculus for security protocols. The abstract semantics is then used to build a decision procedure for secrecy correctness in security protocols.