- -

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 completo del ítem

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

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/71830

Ficheros en el ítem

Thumbnail
Nombre: cade13.paper33.pdf
Tamaño: 447.3Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: lncs.pdf
Tamaño: 280.3Kb
Formato: PDF
Descripción: Versión Editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
Autor: Erbatur, Serdar Escobar Román, Santiago Kapur, Deepak Liu, Zhiqiang Lynch, Christopher A. Meadows, Catherine Meseguer, José Narendran, Paliath Santiago Pinazo, Sonia Sasse, Ralf
Entidad UPV: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica
Fecha difusión:
Resumen:
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 ...[+]
Derechos de uso: Reserva de todos los derechos
ISBN: 978-3-642-38573-5
Fuente:
Automated Deduction – CADE-24. (issn: 0302-9743 )
DOI: 10.1007/978-3-642-38574-2_16
Editorial:
Springer
Versión del editor: http://link.springer.com/chapter/10.1007/978-3-642-38574-2_16
Título del congreso: 24th International Conference on Automated Deduction (CADE - 24)
Lugar del congreso: Lake Placid, New York, USA
Fecha congreso: June 9-14, 2013
Serie: Lecture Notes in Computer Science;7898
Código del Proyecto:
info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/
...[+]
info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/
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/
info:eu-repo/grantAgreement/NSF//0905378/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/
info:eu-repo/grantAgreement/NSF//0905286/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/
info:eu-repo/grantAgreement/NSF//0905222/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/
info:eu-repo/grantAgreement/NSF//0904749/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/
[-]
Descripción: The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-38574-2_16
Agradecimientos:
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 ...[+]
Tipo: Capítulo de libro Comunicación en congreso

References

IEEE 802.11 Local and Metropolitan Area Networks: Wireless LAN Medium Access Control (MAC) and Physical (PHY) Specifications (1999)

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)

Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society (2001) [+]
IEEE 802.11 Local and Metropolitan Area Networks: Wireless LAN Medium Access Control (MAC) and Physical (PHY) Specifications (1999)

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)

Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society (2001)

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)

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)

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)

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)

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

Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7-8), 898–928 (2012)

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)

Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation - international edition, 2nd edn. Addison-Wesley (2003)

Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)

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)

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

Lowe, G., Roscoe, A.W.R.: Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering 23, 659–669 (1997)

Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

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)

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)

TeReSe, editor. Term Rewriting Systems. Cambridge University Press (2003)

Viry, P.: Equational rules for rewriting logic. Theor. Comp. Sci. 285(2), 487–517 (2002)

[-]

recommendations

 

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

Mostrar el registro completo del ítem