Sebastian Alexander Mödersheim
ABSTRACT
The abstraction and over-approximation of protocols and web services by a set of Horn clauses is a very successful method in practice. It has however limitations for protocols and web services that are based on databases of keys, contracts, or even access rights, where revocation is possible, so that the set of true facts does not monotonically grow with state transitions. We extend the scope of these over-approximation methods by defining a new way of abstraction that can handle such databases, and we formally prove that the abstraction is sound. We realize a translator from a convenient specification language to standard Horn clauses and use the verifier ProVerif and the theorem prover SPASS to solve them. We show by a number of examples that this approach is practically feasible for wide variety of verification problems of security protocols and web services
- }}A. Armando, L. Compagna. SAT-based Model-Checking for Security Protocols Analysis. Int. J. of Information Security, 6(1):3--32, 2007. Google Scholar
Digital Library
- }}N. Asokan, V. Shoup, M. Waidner. Asynchronous protocols for optimistic fair exchange. In IEEE Symposium on Research in Security and Privacy, 86--99. 1998.Google ScholarCross Ref
- }}AVISPA. Deliverable 2.3: The Intermediate Format, 2003. Available at www.avispa-project.org/publications.html.Google Scholar
- }}D. Basin, S. Modersheim, L. Vigano'. OFMC: A symbolic model checker for security protocols. Int. J. of Information Security, 4(3):181--208, 2005.Google ScholarDigital Library
- }}J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, S. Maffeis. Refinement types for secure implementations. In CSF, 17--32. 2008. Google ScholarDigital Library
- }}K. Bhargavan, C. Fournet, A. D. Gordon, R. Pucella. Tulafale: A security tool for web services. In FMCO, 197--222. 2003.Google Scholar
- }}B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In CSFW'01, 82--96. IEEE Computer Society Press, 2001. Google ScholarDigital Library
- }}B. Blanchet. Automatic verification of correspondences for security protocols. Journal of Computer Security, 17(4):363--434, 2009. Google ScholarCross Ref
- }}C. Bodei, M. Buchholtz, P. Degano, F. Nielson, H. R. Nielson. Static validation of security protocols. Journal of Computer Security, 13(3):347--390, 2005. Google ScholarDigital Library
- }}Y. Boichut, P.-C. Heam, O. Kouchnarenko, F. Oehl. Improvements on the Genet and Klay technique to automatically verify security protocols. In AVIS'04, 1--11. 2004.Google Scholar
- }}L. Bozga, Y. Lakhnech, M. Perin. Hermes: An automatic tool for the verification of secrecy in security protocols. In CAV'03, LNCS 2725, 219--222. Springer-Verlag, 2003.Google Scholar
- }}N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov. Undecidability of bounded security protocols. In Formal methods and security Protocols. 1999.Google Scholar
- }}S. Even, O. Goldreich. On the security of multi-party ping-pong protocols. In FOCS, 34--39. 1983. Google ScholarDigital Library
- }}J. Heather, G. Lowe, S. Schneider. How to prevent type flaw attacks on security protocols. In CSFW'00. IEEE Computer Society Press, 2000. Google ScholarDigital Library
- }}G. Lowe. Casper: a Compiler for the Analysis of Security Protocols. Journal of Computer Security, 6(1):53--84, 1998. Google ScholarDigital Library
- }}S. Modersheim. On the Relationships between Models in Protocol Verification. J. of Information and Computation, 206(2--4):291--311, 2008. Google ScholarDigital Library
- }}S. Modersheim. Verification based on set-abstraction using the AIF framework. Tech. Rep. IMM-Technical report-2010-09, DTU/IMM, 2010. Available at www.imm.dtu.dk/~samo.Google Scholar
- }}SEVECOM. Deliverable 2.1-App.A: Baseline Security Specifications, 2009. Available at www.sevecom.org.Google Scholar
- }}G. Steel. Towards a formal security analysis of the Sevecom API. In ESCAR. 2009.Google Scholar
- }}G. Steel. Abstractions for Verifying Key Management APIs. In SecReT. 2010.Google Scholar
- }}C. Weidenbach. Towards an automatic analysis of security protocols. In CADE, LNCS 1632, 378--382. Berlin, 1999. Google ScholarDigital Library
- }}C. Weidenbach, R. A. Schmidt, T. Hillenbrand, R. Rusev, D. Topic. System description: Spass version 3.0. In CADE, 514--520. 2007. Google ScholarDigital Library
Index Terms
- Abstraction by set-membership: verifying security protocols and web services with databases
Recommendations
Predicate abstraction with indexed predicates
Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We ...
Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces
A crucial problem in service-oriented computing is the specification and analysis of interactions among multiple peers that communicate via messages. We propose a design pattern that enables the specification of behavioral interfaces acting as ...
Predicate abstraction in a program logic calculus
Predicate abstraction is a form of abstract interpretation where the abstract domain is constructed from a finite set of predicates over the variables of the program. This paper explores a way to integrate predicate abstraction into a calculus for ...
Comments