- -

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

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

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

Ficheros en el ítem

Thumbnail
Nombre: esorics12.pdf
Tamaño: 433.2Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: Effective Symbolic ...
Tamaño: 309.4Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Effective symbolic protocol analysis via equational irreducibility conditions
Autor: Erbatur, Serdar Escobar Román, Santiago Kapur, Deepak Liu, Zhiqiang Lynch, Christopher 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ó
Fecha difusión:
Resumen:
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 ...[+]
Palabras clave: Systems and data security , Data encryption
Derechos de uso: Reserva de todos los derechos
ISBN: 978-3-642-33166-4
Fuente:
Computer Security - ESORICS 2012. (issn: 0302-9743 )
DOI: 10.1007/978-3-642-33167-1_5
Editorial:
Springer Verlag (Germany)
Versión del editor: http://link.springer.com/chapter/10.1007/978-3-642-33167-1_5
Título del congreso: 17th European Symposium on Research in Computer Security 2012
Lugar del congreso: Pisa, Italy
Fecha congreso: September 10-12, 2012
Serie: Lecture Notes in Computer Science;vol. 7459
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/
[-]
Agradecimientos:
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 ...[+]
Tipo: Capítulo de libro

References

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

Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2), 2–32 (2006)

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) [+]
IEEE 802.11 Local and Metropolitan Area Networks: Wireless LAN Medium Access Control (MAC) and Physical (PHY) Specifications (1999)

Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2), 2–32 (2006)

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)

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)

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)

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

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)

Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program. 75(1), 3–51 (2008)

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)

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)

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)

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)

Ciobâcă, Ş.: Knowledge in security protocols

Dolev, D., Yao, A.C.-C.: On the security of public key protocols (extended abstract). In: FOCS, pp. 350–357 (1981)

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)

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)

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)

Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the maude-nrl protocol analyzer. Information and Computation (in press, 2012)

Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program (in press, 2012)

Thayer Fabrega, F.J., Herzog, J., Guttman, J.: Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security 7, 191–230 (1999)

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

Küsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: CSF, pp. 157–171. IEEE Computer Society (2009)

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)

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)

Lowe, G., Roscoe, B.: Using csp to detect errors in the tmn protocol. IEEE Transactions on Software Engineering 23, 659–669 (1997)

Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Functl. and Log. Progr. 1(4), 446–453 (1998)

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

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)

Mödersheim, S.: Models and methods for the automated analysis of security protocols. PhD thesis, ETH Zurich (2007)

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)

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 (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)

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

Zhang, H., Remy, J.-L.: Contextual Rewriting. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 46–62. Springer, Heidelberg (1985)

[-]

recommendations

 

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

Mostrar el registro completo del ítem