Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
DOI:
https://doi.org/10.6092/issn.1972-5787/3720Keywords:
PVS, formalization of security properties, automated theorem proving, algebraic specificationAbstract
In this work, we present an algebraic approach for modeling the two-party cascade protocol of Dolev-Yao and for fully formalizing its security in the specification language of the Prototype Verification System PVS. Although cascade protocols could be argued to be a very limited model, it should be stressed here that they are the basis of more sophisticated protocols of great applicability, such as those which allow treatment of multiparty, tuples, nonces, name-stamps, signatures, etc. In the current algebraic approach, steps of the protocol are modeled in a monoid freely generated by the cryptographic operators. Words in this monoid are specified as finite sequences and the whole protocol as a finite sequence of protocol steps, that are functions from pairs of users to sequences of cryptographic operators. In a previous work, assuming that for balanced protocols admissible words produced by a potential intruder should be balanced, a formalization of the characterization of security of this kind of protocols was given in PVS. In this work, the previously assumed property is also formalized, obtaining in this way a complete formalization which mathematically guarantees the security of these protocols. Despite such property being relatively easy to specify, obtaining a complete formalization requires a great amount of effort, because several algebraic properties, that are related to the preservation of the balancing property of the admissible language of the intruder, should be formalized in the granularity of the underlying data structure (of finite sequences used in the specification). Among these properties, the most complex are related to the notion of linkage property, which allows for a systematic analysis of words of the admissible language of a potential saboteur, showing how he/she is unable to isolate private keys of other users under the assumption of balanced protocols. The difficulties that arose in conducting this formalization are also presented in this work.
References
A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P. C. He ́am, O. Kouchnarenko, J. Mantovani, S. M ̈odersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Vigan`o, and L. Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. In Proceedings of the 17th international conference on Computer Aided Verification, volume 3576 of Lecture Notes in Com- puter Science, pages 281–285. Springer Verlag, 2005.
M. Abadi, B. Blanchet, and H. Comon-Lundh. Models and proofs of protocol security: A progress report. In 21st International Con- ference on Computer Aided Verification (CAV’09), volume 5643 of Lecture Notes in Computer Science, pages 35–49. Springer Verlag, 2009.
M. Abadi and V. Cortier. Deciding knowledge in security protocols under equational theories. Theoretical Computer Science, 367(1- 2):2–32, 2006. 1.2 D. Basin, C. Cremers, and C. Meadows. Model Checking Security Protocols, chapter 24. Springer Verlag, 2011. To appear.
N. Bena ̈ıssa. Modelling Attacker’s Knowledge for Cascade Cryp- tographic Protocols. In ABZ ’08: Proc. of the 1st Int. Conf. on Abstract State Machines, B and Z, volume 5238 of Lecture Notes in Computer Science, pages 251–264. Springer Verlag, 2008.
G. Barthe, B. Gr ́egoire, S. Heraud, and S. Zanella-B ́eguelin. Computer-Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology – CRYPTO 2011, volume 6841 of Lec- ture Notes in Computer Science, pages 71–90. Springer Verlag, 2011.
G. Barthe, B. Gr ́egoire, and S. Zanella B ́eguelin. Formal certifica- tion of code-based cryptographic proofs. In 36th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages POPL, pages 90–101, 2009.
M. Backes and C. Jacobi. Cryptographically Sound and Machine-Assisted Verification of Security Protocols. In 20th Annual Symposium on Theoretical Aspects of Computer Science (STACS), volume 2607 of Lecture Notes in Computer Science, pages 675–686. Springer Verlag, 2003.
Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In 14th IEEE Computer Security Foundations Work- shop (CSFW), pages 82–96. IEEE Computer Society, 2001.
A. D. Brucker and S. M ̈odersheim. Integrating Automated and In- teractive Protocol Verification. In Formal Aspects in Security and Trust, 6th International Workshop, FAST 2009, volume 5983 of Lec- ture Notes in Computer Science, pages 248–262. Springer Verlag, 2009.
I. Cervesato. The Dolev-Yao Intruder is the Most Powerful At- tacker. In Proceedings of the Sixteenth Annual Symposium on Logic in Computer Science - LICS’01, pages 16–19. IEEE Computer So- ciety Press, 2001.
V. Cortier, J. Millen, and Harald Ruess. Proving secrecy is easy enough. In 14th IEEE Computer Security Foundations Workshop (CSFW’01), pages 97–110. IEEE Comp. Soc. Press, 2001. 1.2 D. E. Cohen. Combinatorial Group Theory: a topological approach. CUP, 1989.
C. J. F. Cremers. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. In Computer Aided Verification, 20th International Conference, CAV, volume 5123 of Lecture Notes in Computer Science, pages 414–418, 2008.
B. Dutertre, V. Crettaz, and V. Stavridou. Intrusion-tolerant en- claves. In Proc. of the IEEE International Symposium on Security and Privacy, pages 216–224, 2002.
Dutertre and S. Schneider. Using a PVS Embedding of CSP to Verify Authentication Protocols. In Theorem Proving in Higher Or- der Logics, TPHOL’s 97, volume 1275 of Lecture Notes in Computer Science, pages 121–136. Springer Verlag, 1997.
D. Dolev and A. C. Yao. On the Security of Public Key Protocols. IEEE. T. on Information Theory, 29(2):198–208, 1983.
S. Escobar, D. Kapur, C. Lynch, C. Meadows, J. Meseguer, P. Narendran, and R. Sasse. Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. In Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP, pages 65–76. ACM, 2011.
N. Evans and S. Schneider. Analysing Time Dependent Security Properties in CSP Using PVS. In 6th European Symposium on Research in Computer Security ESORICS, volume 1895 of Lecture Notes in Computer Science, pages 222–237. Springer Verlag, 2000.
M. Layouni, J. Hoofman, and S. Tahar. Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol. Interna- tional Journal of Network Security, 5(3):288–298, 2007.
M. Lothaire. Algebraic Combinatorics on Words. CUP, 2002. 1.1, 2 G. Lowe. An Attack on the Needham-Schroeder Public-Key Authen- tication Protocol. Information Processing Letters, 56(3):131–133, 1995.
G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. Software - Concepts and Tools, 17(3):93–102, 1996. 1.1 W. Mao. A structured operational semantic modelling of the Dolev- Yao threat environment and its composition with cryptographic pro- tocols. Computer Standards & Interfaces, 27(5):479–488, 2005.
S. Meier, C. J. F. Cremers, and D. A. Basin. Strong Invariants for the Efficient Construction of Machine-Checked Protocol Secu- rity Proofs. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pages 231–245. IEEE Computer Society, 2010.
C. Meadows. Methods for Cryptographic Protocol Analysis: Emerg- ing Issues and Trends. IEEE J. on Selected Areas in Communica- tions, 21(1):44–54, 2003. 1.1 J. K. Millen and H. Rueß. Protocol-independent secrecy. In IEEE Symposium on Security and Privacy, pages 110–209, 2000.
R.B. Nogueira, F.L.C. de Moura, A. Nascimento, and M. Ayala- Rinc ́on. Formalization Of Security Proofs Using PVS in the Dolev- Yao Model. In Computability in Europe CiE 2010 (Booklet), 2010.
R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Comm. of the ACM, 21:993–999, 1978. 1.1 Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical report, SRI-CSL-97-2, Computer Science Labora- tory, SRI International, Menlo Park, CA, August 1997. Available at http://pvs.csl.sri.com/.
L. C. Paulson. Proving Security Protocols Correct. In 14th Annual IEEE Symposium on Logic in Computer Science LICS, pages 370– 383, 1999. 1.2 M. Rusinowitch and M. Turuani. Protocol insecurity with a finite number of sessions, composed keys is np-complete. Theoretical Com- puter Science, 299(1-3):451–475, 2003.
B. Schmidt, S. Meier, C. J. F. Cremers, and D. A. Basin. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Prop- erties. In 25th IEEE Computer Security Foundations Symposium, CSF, pages 78–94. IEEE, 2012.
F.L. Tiplea, C. Enea, and C. V. Birjoveanu. Decidability and com- plexity results for security protocols. In Edmund M. Clarke, Marius Minea, and Ferucio Laurentiu Tiplea, editors, VISSAS, volume 1 of NATO Security through Science Series D: Information and Commu- nication Security, pages 185–211. IOS Press, 2005.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2013 Mauricio Ayala-Rincón, Yuri Santos Rego
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
