- -

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: cade13.paper33.pdf
Tamaño: 447.3Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: lncs.pdf
Tamaño: 280.3Kb
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 A. 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 2016-10-14T11:55:03Z
dc.date.available 2016-10-14T11:55:03Z
dc.date.issued 2013
dc.identifier.isbn 978-3-642-38573-5
dc.identifier.issn 0302-9743
dc.identifier.uri http://hdl.handle.net/10251/71830
dc.description The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-38574-2_16 es_ES
dc.description.abstract We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R,E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unification problems to a set of problems s=?ts=?t under the constraint that t remains R/E-irreducible. We call this method asymmetric unification. We first present a general-purpose generic asymmetric unification algorithm. and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification. es_ES
dc.description.sponsorship S. Escobar and S. Santiago were partially supported by EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. The following authors were partially supported by NSF: S. Escobar, J. Meseguer, and R. Sasse under CNS 09-04749 and CCF 09- 05584; D. Kapur under CNS 09-05222; C. Lynch, Z. Liu, and C. Meadows under CNS 09-05378, and P. Narendran and S. Erbatur under CNS 09-05286. Part of the S. Erbatur’s work was supported while with the Department of Computer Science, University at Albany, and part of R. Sasse’s work was supported while with the Department of Computer Science, University of Illinois at Urbana-Champaign.
dc.format.extent 18 es_ES
dc.language Inglés es_ES
dc.publisher Springer es_ES
dc.relation.ispartof Automated Deduction – CADE-24 es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;7898
dc.rights Reserva de todos los derechos es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis es_ES
dc.type Capítulo de libro es_ES
dc.type Comunicación en congreso es_ES
dc.identifier.doi 10.1007/978-3-642-38574-2_16
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.contributor.affiliation Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica es_ES
dc.description.bibliographicCitation Erbatur, S.; Escobar Román, S.; Kapur, D.; Liu, Z.; Lynch, CA.; Meadows, C.; Meseguer, J.... (2013). Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. En Automated Deduction – CADE-24. Springer. 231-248. https://doi.org/10.1007/978-3-642-38574-2_16 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename 24th International Conference on Automated Deduction (CADE - 24) es_ES
dc.relation.conferencedate June 9-14, 2013 es_ES
dc.relation.conferenceplace Lake Placid, New York, USA es_ES
dc.relation.publisherversion http://link.springer.com/chapter/10.1007/978-3-642-38574-2_16 es_ES
dc.description.upvformatpinicio 231 es_ES
dc.description.upvformatpfin 248 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.relation.senia 266076 es_ES
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.contributor.funder University at Albany
dc.contributor.funder University of Illinois at Urbana-Champaign
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 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 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 Bürckert, H.-J., Herold, A., Schmidt-Schauß, M.: On equational theories, unification, and (un)decidability. Journal of Symbolic Computation 8(1/2), 3–49 (1989) 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 Durán, F., Meseguer, J.: A Maude coherence checker tool for conditional order-sorted rewrite theories. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010) es_ES
dc.description.references Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Effective symbolic protocol analysis via equational irreducibility conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 73–90. Springer, Heidelberg (2012) es_ES
dc.description.references Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Sasse, R.: Asymmetric unification: A new unification paradigm for cryptographic protocol analysis. In: UNIF 2011 (2011), https://sites.google.com/a/cs.uni.wroc.pl/unif-2011/program es_ES
dc.description.references Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7-8), 898–928 (2012) es_ES
dc.description.references Harju, T., Karhumäki, J., Krob, D.: Remarks on generalized post correspondence problem. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 39–48. Springer, Heidelberg (1996) es_ES
dc.description.references Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation - international edition, 2nd edn. Addison-Wesley (2003) 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 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 Liu, Z.: Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis. PhD thesis, Clarkson University (2012), http://people.clarkson.edu/~clynch/papers/Dissertation_of_Zhiqiang_Liu.pdf es_ES
dc.description.references Lowe, G., Roscoe, A.W.R.: Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering 23, 659–669 (1997) 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 Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Proc. CSF 2012, pp. 78–94. IEEE (2012) 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, editor. Term Rewriting Systems. Cambridge University Press (2003) es_ES
dc.description.references Viry, P.: Equational rules for rewriting logic. Theor. Comp. Sci. 285(2), 487–517 (2002) es_ES


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

Mostrar el registro sencillo del ítem