- -

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

Ficheros en el ítem

Thumbnail
Nombre: Aparicio-SanchezE ...
Tamaño: 492.6Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: Aparicio-Sa&#769n ...
Tamaño: 841.0Kb
Formato: Desconocido
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Aparicio-Sánchez, Damián es_ES
dc.contributor.author Escobar Román, Santiago es_ES
dc.contributor.author Gutiérrez Gil, Raúl es_ES
dc.contributor.author Sapiña-Sanchis, Julia es_ES
dc.date.accessioned 2021-12-27T08:37:25Z
dc.date.available 2021-12-27T08:37:25Z
dc.date.issued 2020-09-18 es_ES
dc.identifier.isbn 978-3-030-59012-3 es_ES
dc.identifier.issn 0302-9743 es_ES
dc.identifier.uri http://hdl.handle.net/10251/178909
dc.description.abstract [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, some algebraic properties, and protocols using them, have been beyond Maude-NPA capabilities, either because the cryptographic properties cannot be expressed using its equational unification features or because the state space is unmanageable. In this paper, we provide a protocol transformation that can safely get rid of cryptographic properties under some conditions. The time and space difference between verifying the protocol with all the crypto properties and verifying the protocol with a minimal set of the crypto properties is remarkable. We also provide, for the first time, an encoding of the theory of bilinear pairing into Maude-NPA that goes beyond the encoding of bilinear pairing available in the Tamarin tool es_ES
dc.description.sponsorship 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 award number FA9550-17-1-0286. Julia Sapiña has been supported by the Generalitat Valenciana APOSTD/2019/127 grant es_ES
dc.language Inglés es_ES
dc.publisher Springer Nature es_ES
dc.relation.ispartof Computer Security - ESORICS 2020. 25th European Symposium on Research in Computer Security, ESORICS 2020, Guildford, UK, September 14¿18, 2020, Proceedings, Part II es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Crypto protocol analysis es_ES
dc.subject Diffie-Hellman es_ES
dc.subject Exponentiation es_ES
dc.subject Bilinear pairing es_ES
dc.subject Protocol transformation es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA es_ES
dc.type Comunicación en congreso es_ES
dc.type Artículo es_ES
dc.type Capítulo de libro es_ES
dc.identifier.doi 10.1007/978-3-030-59013-0_12 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/AFOSR//FA9550-17-1-0286//ADVANCED SYMBOLIC METHODS FOR THE CRYPTOGRAPHIC PROTOCOL ANALYZER MAUDE-NPA/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement///PROMETEO%2F2019%2F098//DEEPTRUST/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/AEI//RTI2018-094403-B-C32-AR//RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement///APOSTD%2F2019%2F127//CONTRATO POSDOCTORAL GVA-SAPIÑA SANCHIS. PROYECTO: METODOS SIMBOLICOS AVANZADOS PARA EL ANALISIS DE SEGURIDAD DE PROTOCOLOS/ 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 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 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename 25th European Symposium on Research in Computer Security (ESORICS 2020) es_ES
dc.relation.conferencedate Septiembre 14-18,2020 es_ES
dc.relation.conferenceplace Guildford, United Kingdom es_ES
dc.relation.publisherversion https://doi.org/10.1007/978-3-030-59013-0_12 es_ES
dc.description.upvformatpinicio 230 es_ES
dc.description.upvformatpfin 250 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.relation.pasarela S\418751 es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.contributor.funder Air Force Office of Scientific Research es_ES
dc.description.references Maude-NPA manual v3.1. http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA es_ES
dc.description.references The Tamarin-Prover Manual, 4 June 2019. https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and ProVerif. Found. Trends Privacy Secur. 1(1–2), 1–135 (2016) es_ES
dc.description.references Clavel, M., et al.: Maude manual (version 3.0). Technical report, SRI International, Computer Science Laboratory (2020). http://maude.cs.uiuc.edu 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). https://doi.org/10.1007/978-3-540-32033-3_22 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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) 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. Theor. Comput. Sci. 367(1–2), 162–202 (2006) 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-2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_1 es_ES
dc.description.references Escobar, S., et al.: Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. In: Proceedings of PPDP 2011, pp. 65–76. ACM (2011) es_ES
dc.description.references Escobar, S., Meadows, C.A., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL protocol analyzer. Inf. Comput. 238, 157–186 (2014) 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 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references Küsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: IEEE Computer Security Foundations, pp. 157–171 (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. J. Autom. Reason. 46(3–4), 325–352 (2011) es_ES
dc.description.references Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Program. 26(2), 113–131 (1996) es_ES
dc.description.references 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) es_ES
dc.description.references Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theoret. Comput. Sci. 96(1), 73–155 (1992) es_ES
dc.description.references Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3–41 (2018) es_ES
dc.description.references Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebr. Meth. Program. 110, 100483 (2020) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. J. Log. Algebraic Methods Program. 96, 81–110 (2018) es_ES
dc.description.references TeReSe: Term Rewriting Systems. Cambridge University Press, Cambridge (2003) es_ES
dc.description.references 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) es_ES


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

Mostrar el registro sencillo del ítem