Noomene Ben Henda
ABSTRACT
In telecommunication networks, it is common that security protocol procedures rely on context information and other parameters of the global system state. Current security ver- ification tools are well suited for analyzing protocols in iso- lation and it is not clear how they can be used for protocols intended to be run in more“dynamic”settings. Think of pro- tocol procedures sharing parameters, arbitrarily interleaved or used as building blocks in more complex compound proce- dures. SPIN is a well established general purpose verification tool that has good support for modeling such systems. In contrast to specialized tools, SPIN lacks support for crypto- graphic primitives and intruder model which are necessary for checking security properties. We consider a special class of security protocols that fit well in the SPIN framework. Our modeling method is systematic, generic and efficient enough so that SPIN could find all the expected attacks on several of the classical key distribution protocols.
- 3GPP The Mobile Broadband Standard. http://www.3gpp.org/specifications/.Google Scholar
- 10th Computer Security Foundations Workshop (CSFW ’97), June 10-12, 1997, Rockport, Massachusetts, USA. IEEE Computer Society, 1997.Google Scholar
- 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada. IEEE Computer Society, 2001.Google Scholar
- M. Abadi, B. Blanchet, and C. Fournet. Just fast keying in the pi calculus. In D. A. Schmidt, editor, ESOP, volume 2986 of Lecture Notes in Computer Science, pages 340–354. Springer, 2004.Google Scholar
- M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In C. Hankin and D. Schmidt, editors, POPL, pages 104–115. ACM, 2001. Google ScholarDigital Library
- B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In CSFW {3}, pages 82–96. Google ScholarDigital Library
- B. Blanchet. Automatic verification of correspondences for security protocols. Journal of Computer Security, 17(4):363–434, 2009. Google ScholarDigital Library
- C. Cremers and S. Mauw. Operational Semantics and Verification of Security Protocols. Information Security and Cryptography. Springer, 2012. Google ScholarDigital Library
- C. J. F. Cremers. The scyther tool: Verification, falsification, and analysis of security protocols. In A. Gupta and S. Malik, editors, CAV, volume 5123 of Lecture Notes in Computer Science, pages 414–418. Springer, 2008. Google ScholarDigital Library
- C. J. F. Cremers. Session-state reveal is stronger than ephemeral key reveal: Attacking the naxos authenticated key exchange protocol. In M. Abdalla, D. Pointcheval, P.-A. Fouque, and D. Vergnaud, editors, ACNS, volume 5536 of Lecture Notes in Computer Science, pages 20–33, 2009. Google ScholarDigital Library
- C. J. F. Cremers. Key exchange in ipsec revisited: Formal analysis of ikev1 and ikev2. In V. Atluri and C. D´ıaz, editors, ESORICS, volume 6879 of Lecture Notes in Computer Science, pages 315–334. Springer, 2011. Google ScholarDigital Library
- D. E. Denning and G. M. Sacco. Timestamps in key distribution protocols. Commun. ACM, 24(8):533–536, 1981. Google ScholarDigital Library
- D. Dolev and A. C.-C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–207, 1983. Google ScholarDigital Library
- N. A. Durgin, P. Lincoln, and J. C. Mitchell. Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security, 12(2):247–311, 2004. Google ScholarCross Ref
- G. J. Holzmann. The model checker spin. IEEE Trans. Software Eng., 23(5):279–295, 1997. Google ScholarDigital Library
- M. Jakobsson and S. Wetzel. Security weaknesses in bluetooth. In Proceedings of the 2001 Conference on Topics in Cryptology: The Cryptographer’s Track at RSA, CT-RSA 2001, pages 176–191, London, UK, UK, 2001. Springer-Verlag. Google ScholarDigital Library
- A. S. Khan, M. Mukund, and S. P. Suresh. Generic verification of security protocols. In P. Godefroid, editor, SPIN, volume 3639 of Lecture Notes in Computer Science, pages 221–235. Springer, 2005. 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
- G. Lowe. Casper: A compiler for the analysis of security protocols. In CSFW {2}, pages 18–30. Google ScholarDigital Library
- G. Lowe. A hierarchy of authentication specification. In CSFW {2}, pages 31–44. Google ScholarDigital Library
- P. Maggi and R. Sisto. Using spin to verify security properties of cryptographic protocols. In D. Bosnacki and S. Leue, editors, SPIN, volume 2318 of Lecture Notes in Computer Science, pages 187–204. Springer, 2002. Google ScholarDigital Library
- S. Meier, B. Schmidt, C. Cremers, and D. A. Basin. The tamarin prover for the symbolic analysis of security protocols. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of Lecture Notes in Computer Science, pages 696–701. Springer, 2013. Google ScholarDigital Library
- R. M. Needham and M. D. Schroeder. Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993–999, 1978. Google ScholarDigital Library
- M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is np-complete. In CSFW {3}, pages 174–. Google ScholarDigital Library
- C. Tang, D. A. Naumann, and S. Wetzel. Symbolic analysis for security of roaming protocols in mobile networks - {extended abstract}. In M. Rajarajan, F. Piper, H. Wang, and G. Kesidis, editors, SecureComm, volume 96 of Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, pages 480–490. Springer, 2011.Google Scholar
- M. Tatebayashi, N. Matsuzaki, and D. B. N. Jr. Key distribution protocol for digital mobile communication systems. In G. Brassard, editor, CRYPTO, volume 435 of Lecture Notes in Computer Science, pages 324–334. Springer, 1989. Google ScholarDigital Library
Index Terms
- Generic and efficient attacker models in SPIN
Recommendations
Verification of security protocols with lists: From length one to unbounded length
Security and Trust PrinciplesWe present a novel, simple technique for proving secrecy properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. More specifically, our technique relies on the Horn clause approach used in the ...
Bounding messages for free in security protocols - extension to various security properties
While the verification of security protocols has been proved to be undecidable in general, several approaches use simplifying hypotheses in order to obtain decidability for interesting subclasses. Amongst the most common is type abstraction, i.e. ...
Modeling the optimized link-state routing protocol for verification
TMS/DEVS '12: Proceedings of the 2012 Symposium on Theory of Modeling and Simulation - DEVS Integrative M&S SymposiumThe exhaustive property verification of mobile ad hoc routing protocols has proven difficult, especially for proactive protocols. Several attempts to produce tractable models have failed. This article presents the application of formal methods to verify ...
Comments