- -

Effective symbolic protocol analysis via equational irreducibility conditions

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Effective symbolic protocol analysis via equational irreducibility conditions

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: esorics12.pdf
Tamaño: 433.2Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: Effective Symbolic ...
Tamaño: 309.4Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Erbatur, Serdar es_ES
dc.contributor.author Escobar Román, Santiago es_ES
dc.contributor.author Kapur, Deepak es_ES
dc.contributor.author Liu, Zhiqiang es_ES
dc.contributor.author Lynch, Christopher es_ES
dc.contributor.author Meadows, Catherine es_ES
dc.contributor.author Meseguer, José es_ES
dc.contributor.author Narendran, Paliath es_ES
dc.contributor.author Santiago Pinazo, Sonia es_ES
dc.contributor.author Sasse, Ralf es_ES
dc.date.accessioned 2014-03-14T12:03:09Z
dc.date.issued 2012
dc.identifier.isbn 978-3-642-33166-4
dc.identifier.issn 0302-9743
dc.identifier.uri http://hdl.handle.net/10251/36519
dc.description.abstract We address a problem that arises in cryptographic protocol analysis when the equational properties of the cryptosystem are taken into account: in many situations it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the equational theory. We give a tool-independent methodology for state exploration, based on unification and narrowing, that generates states that obey these irreducibility constraints, called contextual symbolic reachability analysis, prove its soundness and completeness, and describe its implementation in the Maude-NPA protocol analysis tool. Contextual symbolic reachability analysis also introduces a new type of unification mechanism, which we call asymmetric unification, in which any solution must leave the right side of the solution irreducible. We also present experiments showing the effectiveness of our methodology. es_ES
dc.description.sponsorship S. Escobar and S. Santiago have been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. The following authors have been partially supported by NSF: S. Escobar, J. Meseguer and R. Sasse under grants CCF 09- 05584, CNS 09-04749, and CNS 09-05584; D. Kapur under grant CNS 09-05222; C. Lynch, Z. Liu, and C. Meadows under grant CNS 09-05378, and P. Narendran and S. Erbatur under grant CNS 09-05286.
dc.format.extent 18 es_ES
dc.language Inglés es_ES
dc.publisher Springer Verlag (Germany) es_ES
dc.relation.ispartof Computer Security - ESORICS 2012 es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;vol. 7459
dc.rights Reserva de todos los derechos es_ES
dc.subject Systems and data security es_ES
dc.subject Data encryption es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Effective symbolic protocol analysis via equational irreducibility conditions es_ES
dc.type Capítulo de libro es_ES
dc.embargo.lift 10000-01-01
dc.embargo.terms forever es_ES
dc.identifier.doi 10.1007/978-3-642-33167-1_5
dc.relation.projectID info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/NSF//0905584/US/TC: Medium: Collaborative Research: Rewriting Logic Foundations for Verification and Programming of Next-Generation Trustworthy Web-Based Systems/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/NSF//0905378/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/NSF//0905286/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/NSF//0905222/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/NSF//0904749/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Erbatur, S.; Escobar Román, S.; Kapur, D.; Liu, Z.; Lynch, C.; Meadows, C.; Meseguer, J.... (2012). Effective symbolic protocol analysis via equational irreducibility conditions. En Computer Security - ESORICS 2012. Springer Verlag (Germany). 7459:73-90. https://doi.org/10.1007/978-3-642-33167-1_5 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename 17th European Symposium on Research in Computer Security 2012 es_ES
dc.relation.conferencedate September 10-12, 2012 es_ES
dc.relation.conferenceplace Pisa, Italy es_ES
dc.relation.publisherversion http://link.springer.com/chapter/10.1007/978-3-642-33167-1_5 es_ES
dc.description.upvformatpinicio 73 es_ES
dc.description.upvformatpfin 90 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 7459 es_ES
dc.relation.senia 241041
dc.contributor.funder European Regional Development Fund
dc.contributor.funder Ministerio de Ciencia e Innovación
dc.contributor.funder Generalitat Valenciana
dc.contributor.funder National Science Foundation, EEUU
dc.description.references IEEE 802.11 Local and Metropolitan Area Networks: Wireless LAN Medium Access Control (MAC) and Physical (PHY) Specifications (1999) es_ES
dc.description.references Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2), 2–32 (2006) es_ES
dc.description.references Arapinis, M., Bursuc, S., Ryan, M.: Privacy Supporting Cloud Computing: ConfiChair, a Case Study. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 89–108. Springer, Heidelberg (2012) es_ES
dc.description.references Basin, D., Mödersheim, S., Viganò, L.: An On-the-Fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003) es_ES
dc.description.references Baudet, M., Cortier, V., Delaune, S.: YAPA: A Generic Tool for Computing Intruder Knowledge. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 148–163. Springer, Heidelberg (2009) es_ES
dc.description.references Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society (2001) es_ES
dc.description.references Blanchet, B.: Using horn clauses for analyzing security protocols. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols. IOS Press (2011) es_ES
dc.description.references Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program. 75(1), 3–51 (2008) es_ES
dc.description.references Ciobâcă, Ş., Delaune, S., Kremer, S.: Computing Knowledge in Security Protocols under Convergent Equational Theories. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 355–370. Springer, Heidelberg (2009) es_ES
dc.description.references Comon-Lundh, H., Delaune, S.: The Finite Variant Property: How to Get Rid of Some Algebraic Properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005) es_ES
dc.description.references Comon-Lundh, H., Delaune, S., Millen, J.: Constraint solving techniques and enriching the model with equational theories. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series, vol. 5, pp. 35–61. IOS Press (2011) es_ES
dc.description.references Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: LICS, pp. 271–280. IEEE Computer Society (2003) es_ES
dc.description.references Ciobâcă, Ş.: Knowledge in security protocols es_ES
dc.description.references Dolev, D., Yao, A.C.-C.: On the security of public key protocols (extended abstract). In: FOCS, pp. 350–357 (1981) es_ES
dc.description.references Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theoretical Computer Science 367(1-2), 162–202 (2006) es_ES
dc.description.references Escobar, S., Meadows, C., Meseguer, J.: State Space Reduction in the Maude-NRL Protocol Analyzer. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 548–562. Springer, Heidelberg (2008) es_ES
dc.description.references Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009) es_ES
dc.description.references Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the maude-nrl protocol analyzer. Information and Computation (in press, 2012) es_ES
dc.description.references Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program (in press, 2012) es_ES
dc.description.references Thayer Fabrega, F.J., Herzog, J., Guttman, J.: Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security 7, 191–230 (1999) es_ES
dc.description.references Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986) es_ES
dc.description.references Küsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: CSF, pp. 157–171. IEEE Computer Society (2009) es_ES
dc.description.references Küsters, R., Truderung, T.: Reducing protocol analysis with xor to the xor-free case in the horn theory based approach. Journal of Automated Reasoning 46(3-4), 325–352 (2011) es_ES
dc.description.references Liu, Z., Lynch, C.: Efficient General Unification for XOR with Homomorphism. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 407–421. Springer, Heidelberg (2011) es_ES
dc.description.references Lowe, G., Roscoe, B.: Using csp to detect errors in the tmn protocol. IEEE Transactions on Software Engineering 23, 659–669 (1997) es_ES
dc.description.references Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Functl. and Log. Progr. 1(4), 446–453 (1998) es_ES
dc.description.references Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992) es_ES
dc.description.references Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation 20(1-2), 123–160 (2007) es_ES
dc.description.references Mödersheim, S.: Models and methods for the automated analysis of security protocols. PhD thesis, ETH Zurich (2007) es_ES
dc.description.references Mödersheim, S., Viganò, L., Basin, D.A.: Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols. Journal of Computer Security 18(4), 575–618 (2010) es_ES
dc.description.references Tatebayashi, M., Matsuzaki, N., Newman Jr., D.B.: Key Distribution Protocol for Digital Mobile Communication Systems. In: Brassard, G. (ed.) CRYPTO 1989. LNCS, vol. 435, pp. 324–334. Springer, Heidelberg (1990) es_ES
dc.description.references TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003) es_ES
dc.description.references Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285(2), 487–517 (2002) es_ES
dc.description.references Zhang, H., Remy, J.-L.: Contextual Rewriting. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 46–62. Springer, Heidelberg (1985) es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem