ABSTRACT
The verification problem for security protocols is undecidable, but it is feasible to verify protocols by abstract interpretation. This paper presents a method based on local abstraction and refinement for verifying security protocols terminably. Local abstraction produces a safe approximation of the security protocol, modeled as a set of Horn logic rules. Refinement removes false attacks introduced by local abstraction. In contrast with methods based on global abstraction, our method abstracts only certain rules that can lead to non-termination when computing fixpoints, that is, it does not abstract all rules. We implement this method in a verification tool SPVT and are able to verify well-known protocols. Moreover, our experiments indicate that local abstraction is less costly than global abstraction.
- M. Backes, A. Cortesi, and M. Maffei. Causality-based abstraction of multiplicity in security protocols. In Proceedings of 20th IEEE Computer Security Foundation Symposium (CSF), June 2007. Google ScholarDigital Library
- B. Blanchet. ProVerif Automatic Cryptographic Protocol Verifier User Manual. CNRS, Département d'Informatique École Normale Supérieure, Paris.Google Scholar
- B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82--96, 2001. Google ScholarDigital Library
- B. Blanchet. From secrecy to authenticity in security protocols. In M. Hermenegildo and G. Puebla, editors, 9th International Static Analysis Symposium (SAS'02), volume 2477 of Lecture Notes in Computer Science, pages 342--359, Madrid, Spain, September 2002. Springer Verlag. Google ScholarDigital Library
- B. Blanchet and A. Podelski. Verification of cryptographic protocols: tagging enforces termination. Theoretical Computer Science, 333(1--2):67--90, March 2005. Google ScholarDigital Library
- L. Bozga, Y. Lakhnech, and M. Périn. HERMES: An automatic tool for verification of secrecy in security protocols. In CAV, pages 219--222, 2003.Google Scholar
- L. Bozga, Y. Lakhnech, and M. Périn. Pattern-based abstraction for verifying secrecy in protocols. Int. J. Softw. Tools Technol. Transf., 8(1):57--76, 2006. Google ScholarDigital Library
- J. A. Clark and J. L. Jacob. A survey of authentication protocol literature. Technical Report 1.0, 1997.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, California, 1977. ACM Press, New York, NY. Google ScholarDigital Library
- N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In N. Heintze and E. Clarke, editors, Proceedings of the Workshop on Formal Methods and Security Protocols -- FMSP, Trento, Italy, July 1999.Google Scholar
- M. Li, Z. Li, H. Chen, and T. Zhou. A novel derivation framework for definite logic program. In P. Panangaden, Y. Chen, and G. Zhang, editors, FICS 2008, volume 212, pages 71--85, Amsterdam, The Netherlands, The Netherlands, June 2008. Elsevier Science Publishers B. V.Google Scholar
- M. Li, T. Zhou, Z. Li, and H. Chen. An abstraction and refinement framework for verifying security protocols based on logic programming. In I. Cervesato, editor, ASIAN 2007, volume 4846 of Lecture Notes in Computer Science, pages 166--180, Berlin Heidelberg, 12 2007. Springer-Verlag. Google ScholarDigital Library
- G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In T. Margaria and B. Steffen, editors, TACAS, volume 1055 of Lecture Notes in Computer Science, pages 147--166. Springer, 1996. Google ScholarDigital Library
- F. Oehl, G. Cece, O. Kouchnarenko, and D. Sinclair. Automatic approximation for the verification of cryptographic protocols, 2003.Google Scholar
Index Terms
Local abstract verification and refinement of security protocols
Recommendations
A counterexample-guided abstraction-refinement framework for markov decision processes
The main challenge in using abstractions effectively is to construct a suitable abstraction for the system being verified. One approach that tries to address this problem is that of counterexample guided abstraction refinement (CEGAR), wherein one ...
Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks
As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for verifying DNNs with formal guarantees, ...
SAT-Based Verification of Security Protocols Via Translation to Networks of Automata
Model Checking and Artificial IntelligenceIn this paper we show a novel method for modelling behaviours of security protocols using networks of communicating automata in order to verify them with SAT-based bounded model checking. These automata correspond to executions of the participants as ...
Comments