- -

An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: Lopez-RuedaEscoba ...
Tamaño: 720.5Kb
Formato: PDF
Descripción: Versión editorial
Abrir
dc.contributor.author López-Rueda, Raúl es_ES
dc.contributor.author Escobar Román, Santiago es_ES
dc.contributor.author Sapiña-Sanchis, Julia es_ES
dc.date.accessioned 2024-06-13T18:17:12Z
dc.date.available 2024-06-13T18:17:12Z
dc.date.issued 2023-10 es_ES
dc.identifier.issn 2352-2208 es_ES
dc.identifier.uri http://hdl.handle.net/10251/205130
dc.description.abstract [EN] Narrowing and unification are very useful tools for symbolic analysis of rewrite theories, and thus for any model that can be specified in that way. A very clear example of their application is the field of formal cryptographic protocol analysis, which is why narrowing and unification are used in tools such as Maude-NPA, Tamarin and Akiss. In this work we present the implementation of a canonical narrowing algorithm, which improves the standard narrowing algorithm, extended to be able to process rewrite theories with conditional rules. The conditions of the rules will contain SMT constraints, which will be carried throughout the execution of the algorithm to determine if the solutions have associated satisfiable or unsatisfiable constraints, and in the latter case, discard them. es_ES
dc.description.sponsorship This work has been partially supported by the EC H2020-EU grant agreement No. 952215 (TAILOR) , by the grant PID2021-122830OB-C42 funded by MCIN/AEI/10.13039/501100011033 and ERDF A way of making Europe, by the grant CIPROM/2022/6 funded by Generalitat Valenciana, and by the grant PCI2020-120708-2 funded by MICIN/AEI/10.13039/501100011033 and by the European Union NextGenerationEU/PRTR. Raul Lopez has been supported by the grant FPI-2022- S2-49802 funded by Universitat Politecnica de Valencia. es_ES
dc.language Inglés es_ES
dc.publisher Elsevier es_ES
dc.relation.ispartof Journal of Logical and Algebraic Methods in Programming es_ES
dc.rights Reconocimiento (by) es_ES
dc.subject Narrowing es_ES
dc.subject SMTsolver es_ES
dc.subject Maude es_ES
dc.subject Security protocols es_ES
dc.subject Symbolic analysis es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1016/j.jlamp.2023.100895 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2021-2023/PID2021-122830OB-C42/ES/METODOS FORMALES ESCALABLES PARA APLICACIONES REALES/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/EC/H2020/952215/EU/Integrating Reasoning, Learning and Optimization/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GENERALITAT VALENCIANA//CIPROM%2F2022%2F6//TECNOLOGIAS DE APRENDIZAJE Y RAZONAMIENTO RAPIDO Y LENTO/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/AEI//PCI2020-120708-2//FORMAL ANALYSIS AND VERIFICATION OF POST-QUANTUM CRYPTOGRAPHIC PROTOCOLS/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/UPV//FPI-2022-S2-49802/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica es_ES
dc.description.bibliographicCitation López-Rueda, R.; Escobar Román, S.; Sapiña-Sanchis, J. (2023). An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis. Journal of Logical and Algebraic Methods in Programming. 135. https://doi.org/10.1016/j.jlamp.2023.100895 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion https://doi.org/10.1016/j.jlamp.2023.100895 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 135 es_ES
dc.relation.pasarela S\498005 es_ES
dc.contributor.funder European Commission es_ES
dc.contributor.funder GENERALITAT VALENCIANA es_ES
dc.contributor.funder AGENCIA ESTATAL DE INVESTIGACION es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.contributor.funder COMISION DE LAS COMUNIDADES EUROPEA es_ES
dc.contributor.funder Universitat Politècnica de València es_ES


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

Mostrar el registro sencillo del ítem