Abstract
First-order logic resolution is a standard way to automate the verification of security protocols. However, it sometimes fails to produce security proofs for secure protocols because of the detection of false attacks. For the verification of a bounded number of sessions, false attacks can be avoided by introducing rigid variables. Unfortunately, this yields complicated resolution procedures. We show here that there is a simple translation of the security problem for a bounded number of sessions into first-order logic, that does not introduce false attacks. This is shown by translating clauses involving rigid variables into classical first-order clauses, while preserving satisfiability. We illustrate this approach by giving a complete and terminating strategy for a first-order logic fragment resulting from the above translation, that yields a decision procedure for a bounded number of sessions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allamigeon, X., Blanchet, B.: Reconstruction of Attacks against Cryptographic Protocols. In: 18th IEEE Work. on Computer Security Foundations, pp. 140–154 (2005)
Andrews, P.B.: Theorem proving via general matings. Journal of the ACM 28(2), 193–214 (1981)
Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Handbook of Automated Reasoning, ch. 2, pp. 19–99. Elsevier/MIT Press (2001)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Work. on Computer Security Foundations, pp. 82–96 (2001)
Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pp. 243–320. Elsevier/MIT Press (1990)
Cervesato, I., Durgin, N.A., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: 12th IEEE Work. on Computer Security Foundations, pp. 55–69 (1999)
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: 18th IEEE Symp. on Logic in Computer Science (LICS 2003), pp. 261–270 (2003)
Cohen, A.: Combined CPV-TLV Security Protocol Verifier. Master’s thesis, New York University (2004)
Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Science of Computer Programming 50(1–3), 51–71 (2004)
Comon-Lundh, H., Cortier, V., Zalinescu, E.: Deciding security properties for cryptographic protocols. Application to key cycles. ACM Transactions on Computational Logic (to appear)
Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: 18th IEEE Symp. on Logic in Computer Science (LICS 2003), pp. 271–280 (2003)
Delaune, S., Lin, H., Lynch, C.: Protocol verification via rigid/flexible resolution. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS(LNAI), vol. 4790, pp. 242–256. Springer, Heidelberg (2007)
Fermüller, C.G., Leitsch, A., Hustadt, U., Tamet, T.: Resolution decision procedure. In: Handbook of Automated Reasoning, ch. 25. Elsevier and MIT Press (2001)
Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions, composed keys is NP-complete. Theoretical Computer Science 1-3(299), 451–475 (2003)
Shmatikov, V.: Decidable analysis of cryptographic protocols with products and modular exponentiation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 355–369. Springer, Heidelberg (2004)
Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS, vol. 1632, pp. 314–328. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
feldt, R.A., Comon-Lundh, H. (2009). Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds) Formal to Practical Security. Lecture Notes in Computer Science, vol 5458. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02002-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-02002-5_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02001-8
Online ISBN: 978-3-642-02002-5
eBook Packages: Computer ScienceComputer Science (R0)