- -

An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA

Mostrar el registro completo del ítem

Aparicio-Sánchez, D.; Escobar Román, S.; Gutiérrez Gil, R.; Sapiña-Sanchis, J. (2020). An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA. Springer Nature. 230-250. https://doi.org/10.1007/978-3-030-59013-0_12

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

Ficheros en el ítem

Thumbnail
Nombre: Aparicio-SanchezE ...
Tamaño: 492.6Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: Aparicio-Sa&#769n ...
Tamaño: 841.0Kb
Formato: Desconocido
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA
Autor: Aparicio-Sánchez, Damián Escobar Román, Santiago Gutiérrez Gil, Raúl Sapiña-Sanchis, Julia
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:
[EN] Maude-NPA is an analysis tool for cryptographic security protocols that takes into account the algebraic properties of the cryptosystem. Maude-NPA can reason about a wide range of cryptographic properties. However, ...[+]
Palabras clave: Crypto protocol analysis , Diffie-Hellman , Exponentiation , Bilinear pairing , Protocol transformation
Derechos de uso: Reserva de todos los derechos
ISBN: 978-3-030-59012-3
Fuente:
Computer Security - ESORICS 2020. 25th European Symposium on Research in Computer Security, ESORICS 2020, Guildford, UK, September 14¿18, 2020, Proceedings, Part II. (issn: 0302-9743 )
DOI: 10.1007/978-3-030-59013-0_12
Editorial:
Springer Nature
Versión del editor: https://doi.org/10.1007/978-3-030-59013-0_12
Título del congreso: 25th European Symposium on Research in Computer Security (ESORICS 2020)
Lugar del congreso: Guildford, United Kingdom
Fecha congreso: Septiembre 14-18,2020
Código del Proyecto:
info:eu-repo/grantAgreement/AFOSR//FA9550-17-1-0286//ADVANCED SYMBOLIC METHODS FOR THE CRYPTOGRAPHIC PROTOCOL ANALYZER MAUDE-NPA/
info:eu-repo/grantAgreement///PROMETEO%2F2019%2F098//DEEPTRUST/
info:eu-repo/grantAgreement/AEI//RTI2018-094403-B-C32-AR//RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/
info:eu-repo/grantAgreement///APOSTD%2F2019%2F127//CONTRATO POSDOCTORAL GVA-SAPIÑA SANCHIS. PROYECTO: METODOS SIMBOLICOS AVANZADOS PARA EL ANALISIS DE SEGURIDAD DE PROTOCOLOS/
Agradecimientos:
Partially supported by the EU (FEDER) and the Spanish MCIU under grant RTI2018-094403-B-C32, by the Spanish Generalitat Valenciana under grant PROMETEO/2019/098, and by the US Air Force Office of Scientific Research under ...[+]
Tipo: Comunicación en congreso Artículo Capítulo de libro

References

Maude-NPA manual v3.1. http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA

The Tamarin-Prover Manual, 4 June 2019. https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf

Al-Riyami, S.S., Paterson, K.G.: Tripartite authenticated key agreement protocols from pairings. In: Paterson, K.G. (ed.) Cryptography and Coding 2003. LNCS, vol. 2898, pp. 332–359. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-40974-8_27 [+]
Maude-NPA manual v3.1. http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA

The Tamarin-Prover Manual, 4 June 2019. https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf

Al-Riyami, S.S., Paterson, K.G.: Tripartite authenticated key agreement protocols from pairings. In: Paterson, K.G. (ed.) Cryptography and Coding 2003. LNCS, vol. 2898, pp. 332–359. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-40974-8_27

Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 447–533. Elsevier Science (2001)

Baelde, D., Delaune, S., Gazeau, I., Kremer, S.: Symbolic verification of privacy-type properties for security protocols with XOR. In: 30th IEEE Computer Security Foundations Symposium, CSF 2017, pp. 234–248. IEEE Computer Society (2017)

Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and ProVerif. Found. Trends Privacy Secur. 1(1–2), 1–135 (2016)

Clavel, M., et al.: Maude manual (version 3.0). Technical report, SRI International, Computer Science Laboratory (2020). http://maude.cs.uiuc.edu

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). https://doi.org/10.1007/978-3-540-32033-3_22

Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_38

Dreier, J., Duménil, C., Kremer, S., Sasse, R.: Beyond subterm-convergent equational theories in automated verification of stateful protocols. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 117–140. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54455-6_6

Escobar, S., Hendrix, J., Meadows, C., Meseguer, J.: Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proceedings of 2nd International Workshop on Security and Rewriting Techniques (SecReT 2007) (2007)

Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theor. Comput. Sci. 367(1–2), 162–202 (2006)

Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_1

Escobar, S., et al.: Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. In: Proceedings of PPDP 2011, pp. 65–76. ACM (2011)

Escobar, S., Meadows, C.A., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL protocol analyzer. Inf. Comput. 238, 157–186 (2014)

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

Fabrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: why is a security protocol correct? In: Proceedings of IEEE Symposium on Security and Privacy, pp. 160–171 (1998)

Guttman, J.D.: Security goals and protocol transformations. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 130–147. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27375-9_8

Joux, A.: A one round protocol for tripartite Diffie-Hellman. In: Bosma, W. (ed.) ANTS 2000. LNCS, vol. 1838, pp. 385–393. Springer, Heidelberg (2000). https://doi.org/10.1007/10722028_23

Kim, Y., Perrig, A., Tsudik, G.: Communication-efficient group key agreement. In: Dupuy, M., Paradinas, P. (eds.) SEC 2001. IIFIP, vol. 65, pp. 229–244. Springer, Boston, MA (2002). https://doi.org/10.1007/0-306-46998-7_16

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

Küsters, R., Truderung, T.: Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. J. Autom. Reason. 46(3–4), 325–352 (2011)

Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Program. 26(2), 113–131 (1996)

Meier, S., Cremers, C., Basin, D.: Strong invariants for the efficient construction of machine-checked protocol security proofs. In: 2010 23rd IEEE Computer Security Foundations Symposium, pp. 231–245 (2010)

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

Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3–41 (2018)

Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebr. Meth. Program. 110, 100483 (2020)

Mödersheim, S., Viganò, L.: The open-source fixed-point model checker for symbolic analysis of security protocols. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 166–194. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_6

Sasse, R., Escobar, S., Meadows, C., Meseguer, J.: Protocol analysis modulo combination of theories: a case study in Maude-NPA. In: Cuellar, J., Lopez, J., Barthe, G., Pretschner, A. (eds.) STM 2010. LNCS, vol. 6710, pp. 163–178. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22444-7_11

Schmidt, B., Sasse, R., Cremers, C., Basin, D.A.: Automated verification of group key agreement protocols. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, pp. 179–194. IEEE Computer Society (2014)

Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. J. Log. Algebraic Methods Program. 96, 81–110 (2018)

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

Yang, F., Escobar, S., Meadows, C.A., Meseguer, J., Narendran, P.: Theories of homomorphic encryption, unification, and the finite variant property. In: Proceedings of PPDP 2014, pp. 123–133. ACM (2014)

[-]

recommendations

 

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

Mostrar el registro completo del ítem