Search | arXiv e-print repository

<!DOCTYPE html> <html lang="en"> <head> <meta charset="utf-8"/> <meta name="viewport" content="width=device-width, initial-scale=1"/>  <link rel="apple-touch-icon" sizes="180x180" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/apple-touch-icon.png"> <link rel="icon" type="image/png" sizes="32x32" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon-32x32.png"> <link rel="icon" type="image/png" sizes="16x16" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon-16x16.png"> <link rel="manifest" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/site.webmanifest"> <link rel="mask-icon" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/safari-pinned-tab.svg" color="#b31b1b"> <link rel="shortcut icon" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon.ico"> <meta name="msapplication-TileColor" content="#b31b1b"> <meta name="msapplication-config" content="images/icons/browserconfig.xml"> <meta name="theme-color" content="#b31b1b">  <title>Search | arXiv e-print repository</title> <script defer src="https://static.arxiv.org/static/base/1.0.0a5/fontawesome-free-5.11.2-web/js/all.js"></script> <link rel="stylesheet" href="https://static.arxiv.org/static/base/1.0.0a5/css/arxivstyle.css" /> <script type="text/x-mathjax-config"> MathJax.Hub.Config({ messageStyle: "none", extensions: ["tex2jax.js"], jax: ["input/TeX", "output/HTML-CSS"], tex2jax: { inlineMath: [ ['$','$'], ["\$","\$"] ], displayMath: [ ['$$','$$'], ["\\[","\\]"] ], processEscapes: true, ignoreClass: '.*', processClass: 'mathjax.*' }, TeX: { extensions: ["AMSmath.js", "AMSsymbols.js", "noErrors.js"], noErrors: { inlineDelimiters: ["$","$"], multiLine: false, style: { "font-size": "normal", "border": "" } } }, "HTML-CSS": { availableFonts: ["TeX"] } }); </script> <script src='//static.arxiv.org/MathJax-2.7.3/MathJax.js'></script> <script src="https://static.arxiv.org/static/base/1.0.0a5/js/notification.js"></script> <link rel="stylesheet" href="https://static.arxiv.org/static/search/0.5.6/css/bulma-tooltip.min.css" /> <link rel="stylesheet" href="https://static.arxiv.org/static/search/0.5.6/css/search.css" /> <script src="https://code.jquery.com/jquery-3.2.1.slim.min.js" integrity="sha256-k2WSCIexGzOj3Euiig+TlR8gA0EmPjuc79OEeY5L45g=" crossorigin="anonymous"></script> <script src="https://static.arxiv.org/static/search/0.5.6/js/fieldset.js"></script> <style> radio#cf-customfield_11400 { display: none; } </style> </head> <body> <header><a href="#main-container" class="is-sr-only">Skip to main content</a>  <div class="attribution level is-marginless" role="banner"> <div class="level-left"> <a class="level-item" href="https://cornell.edu/"><img src="https://static.arxiv.org/static/base/1.0.0a5/images/cornell-reduced-white-SMALL.svg" alt="Cornell University" width="200" aria-label="logo" /></a> </div> <div class="level-right is-marginless"><p class="sponsors level-item is-marginless"><span id="support-ack-url">We gratefully acknowledge support from<br /> the Simons Foundation, <a href="https://info.arxiv.org/about/ourmembers.html">member institutions</a>, and all contributors. <a href="https://info.arxiv.org/about/donate.html">Donate</a></span></p></div> </div>  <div class="identity level is-marginless"> <div class="level-left"> <div class="level-item"> <a class="arxiv" href="https://arxiv.org/" aria-label="arxiv-logo"> <img src="https://static.arxiv.org/static/base/1.0.0a5/images/arxiv-logo-one-color-white.svg" aria-label="logo" alt="arxiv logo" width="85" style="width:85px;"/> </a> </div> </div> <div class="search-block level-right"> <form class="level-item mini-search" method="GET" action="https://arxiv.org/search"> <div class="field has-addons"> <div class="control"> <input class="input is-small" type="text" name="query" placeholder="Search..." aria-label="Search term or terms" /> <p class="help"><a href="https://info.arxiv.org/help">Help</a> | <a href="https://arxiv.org/search/advanced">Advanced Search</a></p> </div> <div class="control"> <div class="select is-small"> <select name="searchtype" aria-label="Field to search"> <option value="all" selected="selected">All fields</option> <option value="title">Title</option> <option value="author">Author</option> <option value="abstract">Abstract</option> <option value="comments">Comments</option> <option value="journal_ref">Journal reference</option> <option value="acm_class">ACM classification</option> <option value="msc_class">MSC classification</option> <option value="report_num">Report number</option> <option value="paper_id">arXiv identifier</option> <option value="doi">DOI</option> <option value="orcid">ORCID</option> <option value="author_id">arXiv author ID</option> <option value="help">Help pages</option> <option value="full_text">Full text</option> </select> </div> </div> <input type="hidden" name="source" value="header"> <button class="button is-small is-cul-darker">Search</button> </div> </form> </div> </div>  <div class="container"> <div class="user-tools is-size-7 has-text-right has-text-weight-bold" role="navigation" aria-label="User menu"> <a href="https://arxiv.org/login">Login</a> </div> </div> </header> <main class="container" id="main-container"> <div class="level is-marginless"> <div class="level-left"> <h1 class="title is-clearfix"> Showing 1–20 of 20 results for author: <span class="mathjax">Escobar, S</span> </h1> </div> <div class="level-right is-hidden-mobile">  <span class="help" style="display: inline-block;"><a href="https://github.com/arXiv/arxiv-search/releases">Search v0.5.6 released 2020-02-24</a>  </span> </div> </div> <div class="content"> <form method="GET" action="/search/cs" aria-role="search"> Searching in archive <strong>cs</strong>. <a href="/search/?searchtype=author&query=Escobar%2C+S">Search in all archives.</a> <div class="field has-addons-tablet"> <div class="control is-expanded"> <label for="query" class="hidden-label">Search term or terms</label> <input class="input is-medium" id="query" name="query" placeholder="Search term..." type="text" value="Escobar, S"> </div> <div class="select control is-medium"> <label class="is-hidden" for="searchtype">Field</label> <select class="is-medium" id="searchtype" name="searchtype"><option value="all">All fields</option><option value="title">Title</option><option selected value="author">Author(s)</option><option value="abstract">Abstract</option><option value="comments">Comments</option><option value="journal_ref">Journal reference</option><option value="acm_class">ACM classification</option><option value="msc_class">MSC classification</option><option value="report_num">Report number</option><option value="paper_id">arXiv identifier</option><option value="doi">DOI</option><option value="orcid">ORCID</option><option value="license">License (URI)</option><option value="author_id">arXiv author ID</option><option value="help">Help pages</option><option value="full_text">Full text</option></select> </div> <div class="control"> <button class="button is-link is-medium">Search</button> </div> </div> <div class="field"> <div class="control is-size-7"> <label class="radio"> <input checked id="abstracts-0" name="abstracts" type="radio" value="show"> Show abstracts </label> <label class="radio"> <input id="abstracts-1" name="abstracts" type="radio" value="hide"> Hide abstracts </label> </div> </div> <div class="is-clearfix" style="height: 2.5em"> <div class="is-pulled-right"> <a href="/search/advanced?terms-0-term=Escobar%2C+S&terms-0-field=author&size=50&order=-announced_date_first">Advanced Search</a> </div> </div> <input type="hidden" name="order" value="-announced_date_first"> <input type="hidden" name="size" value="50"> </form> <div class="level breathe-horizontal"> <div class="level-left"> <form method="GET" action="/search/"> <div style="display: none;"> <select id="searchtype" name="searchtype"><option value="all">All fields</option><option value="title">Title</option><option selected value="author">Author(s)</option><option value="abstract">Abstract</option><option value="comments">Comments</option><option value="journal_ref">Journal reference</option><option value="acm_class">ACM classification</option><option value="msc_class">MSC classification</option><option value="report_num">Report number</option><option value="paper_id">arXiv identifier</option><option value="doi">DOI</option><option value="orcid">ORCID</option><option value="license">License (URI)</option><option value="author_id">arXiv author ID</option><option value="help">Help pages</option><option value="full_text">Full text</option></select> <input id="query" name="query" type="text" value="Escobar, S"> <ul id="abstracts"><li><input checked id="abstracts-0" name="abstracts" type="radio" value="show"> <label for="abstracts-0">Show abstracts</label></li><li><input id="abstracts-1" name="abstracts" type="radio" value="hide"> <label for="abstracts-1">Hide abstracts</label></li></ul> </div> <div class="box field is-grouped is-grouped-multiline level-item"> <div class="control"> <span class="select is-small"> <select id="size" name="size"><option value="25">25</option><option selected value="50">50</option><option value="100">100</option><option value="200">200</option></select> </span> <label for="size">results per page</label>. </div> <div class="control"> <label for="order">Sort results by</label> <span class="select is-small"> <select id="order" name="order"><option selected value="-announced_date_first">Announcement date (newest first)</option><option value="announced_date_first">Announcement date (oldest first)</option><option value="-submitted_date">Submission date (newest first)</option><option value="submitted_date">Submission date (oldest first)</option><option value="">Relevance</option></select> </span> </div> <div class="control"> <button class="button is-small is-link">Go</button> </div> </div> </form> </div> </div> <ol class="breathe-horizontal" start="1"> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2307.06348">arXiv:2307.06348</a> <span> [<a href="https://arxiv.org/pdf/2307.06348">pdf</a>, <a href="https://arxiv.org/format/2307.06348">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Symbolic Computation">cs.SC</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=L%C3%B3pez-Rueda%2C+R">Ra煤l L贸pez-Rueda</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Sapi%C3%B1a%2C+J">Julia Sapi帽a</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2307.06348v1-abstract-short" style="display: inline;"> 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… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2307.06348v1-abstract-full').style.display = 'inline'; document.getElementById('2307.06348v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2307.06348v1-abstract-full" style="display: none;"> 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. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2307.06348v1-abstract-full').style.display = 'none'; document.getElementById('2307.06348v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 12 July, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2023. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">41 pages, 7 tables, 1 algorithm, 9 examples</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2112.10201">arXiv:2112.10201</a> <span> [<a href="https://arxiv.org/pdf/2112.10201">pdf</a>, <a href="https://arxiv.org/format/2112.10201">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Symbolic Specialization of Rewriting Logic Theories with Presto </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Alpuente%2C+M">Mar铆a Alpuente</a>, <a href="/search/cs?searchtype=author&query=Ballis%2C+D">Demis Ballis</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Sapi%C3%B1a%2C+J">Julia Sapi帽a</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2112.10201v1-abstract-short" style="display: inline;"> This paper introduces Presto, a symbolic partial evaluator for Maude's rewriting logic theories that can improve system analysis and verification. In Presto, the automated optimization of a conditional rewrite theory R (whose rules define the concurrent transitions of a system) is achieved by partially evaluating, with respect to the rules of R, an underlying, companion equational logic theory E t… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2112.10201v1-abstract-full').style.display = 'inline'; document.getElementById('2112.10201v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2112.10201v1-abstract-full" style="display: none;"> This paper introduces Presto, a symbolic partial evaluator for Maude's rewriting logic theories that can improve system analysis and verification. In Presto, the automated optimization of a conditional rewrite theory R (whose rules define the concurrent transitions of a system) is achieved by partially evaluating, with respect to the rules of R, an underlying, companion equational logic theory E that specifies the algebraic structure of the system states of R. This can be particularly useful for specializing an overly general equational theory E whose operators may obey complex combinations of associativity, commutativity, and/or identity axioms, when being plugged into a host rewrite theory R as happens, for instance, in protocol analysis, where sophisticated equational theories for cryptography are used. Presto implements different unfolding operators that are based on folding variant narrowing (the symbolic engine of Maude's equational theories). When combined with an appropriate abstraction algorithm, they allow the specialization to be adapted to the theory termination behavior and bring significant improvement while ensuring strong correctness and termination of the specialization. We demonstrate the effectiveness of Presto in several examples of protocol analysis where it achieves a significant speed-up. Actually, the transformation provided by Presto may cut down an infinite folding variant narrowing space to a finite one, and moreover, some of the costly algebraic axioms and rule conditions may be eliminated as well. As far as we know, this is the first partial evaluator for Maude that respects the semantics of functional, logic, concurrent, and object-oriented computations. Under consideration in Theory and Practice of Logic Programming (TPLP). <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2112.10201v1-abstract-full').style.display = 'none'; document.getElementById('2112.10201v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 19 December, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> December 2021. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Under consideration in Theory and Practice of Logic Programming (TPLP)</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2101.05670">arXiv:2101.05670</a> <span> [<a href="https://arxiv.org/pdf/2101.05670">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computers and Society">cs.CY</span> </div> </div> <p class="title is-5 mathjax"> Exploring the Smart City Adoption Process: Evidence from the Belgian urban context </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Margherita%2C+E+G">Emanuele Gabriel Margherita</a>, <a href="/search/cs?searchtype=author&query=Esposito%2C+G">Giovanni Esposito</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S+D">Stefania Denise Escobar</a>, <a href="/search/cs?searchtype=author&query=Crutzen%2C+N">Nathalie Crutzen</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2101.05670v1-abstract-short" style="display: inline;"> In this position paper, we explore the adoption of a Smart City with a socio-technical perspective. A Smart city is a transformational technological process leading to profound modifications of existing urban regimes and infrastructure components. In this study, we consider a Smart City as a socio-technical system where the interplay between technologies and users ensures the sustainable developme… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2101.05670v1-abstract-full').style.display = 'inline'; document.getElementById('2101.05670v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2101.05670v1-abstract-full" style="display: none;"> In this position paper, we explore the adoption of a Smart City with a socio-technical perspective. A Smart city is a transformational technological process leading to profound modifications of existing urban regimes and infrastructure components. In this study, we consider a Smart City as a socio-technical system where the interplay between technologies and users ensures the sustainable development of smart city initiatives that improve the quality of life and solve important socio-economic problems. The adoption of a Smart City required a participative approach where users are involved during the adoption process to joint optimise both systems. Thus, we contribute to socio-technical research showing how a participative approach based on press relationships to facilitate information exchange between municipal actors and citizens worked as a success factor for the smart city adoption. We also discuss the limitations of this approach. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2101.05670v1-abstract-full').style.display = 'none'; document.getElementById('2101.05670v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 14 January, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2021. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Proceedings of the 6th International Workshop on Socio-Technical Perspective in IS Development (STPIS 2020), June 8-9, 2020 http://ceur-ws.org/Vol-2789/paper1.pdf</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> CEUR Workshop Proceedings, Vol-2789, pages 1-7, 2020 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2010.13707">arXiv:2010.13707</a> <span> [<a href="https://arxiv.org/pdf/2010.13707">pdf</a>, <a href="https://arxiv.org/format/2010.13707">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Protocol Analysis with Time </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Aparicio-S%C3%A1nchez%2C+D">Dami谩n Aparicio-S谩nchez</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Meadows%2C+C">Catherine Meadows</a>, <a href="/search/cs?searchtype=author&query=Meseguer%2C+J">Jose Meseguer</a>, <a href="/search/cs?searchtype=author&query=Sapi%C3%B1a%2C+J">Julia Sapi帽a</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2010.13707v1-abstract-short" style="display: inline;"> We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition semantics that takes account of fundamental properties of time. Additional properties can be added by the user if desirable. This timed protocol framework can be implemented either… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2010.13707v1-abstract-full').style.display = 'inline'; document.getElementById('2010.13707v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2010.13707v1-abstract-full" style="display: none;"> We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition semantics that takes account of fundamental properties of time. Additional properties can be added by the user if desirable. This timed protocol framework can be implemented either as a simulation tool or as a symbolic analysis tool in which time references are represented by logical variables, and in which the properties of time are implemented as constraints on those time logical variables. These constraints are carried along the symbolic execution of the protocol. The satisfiability of these constraints can be evaluated as the analysis proceeds, so attacks that violate the laws of physics can be rejected as impossible. We demonstrate the feasibility of our approach by using the Maude-NPA protocol analyzer together with an SMT solver that is used to evaluate the satisfiability of timing constraints. We provide a sound and complete protocol transformation from our timed process algebra to the Maude-NPA syntax and semantics, and we prove its soundness and completeness. We then use the tool to analyze Mafia fraud and distance hijacking attacks on a suite of distance-bounding protocols. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2010.13707v1-abstract-full').style.display = 'none'; document.getElementById('2010.13707v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 26 October, 2020; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2020. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2009.11070">arXiv:2009.11070</a> <span> [<a href="https://arxiv.org/pdf/2009.11070">pdf</a>, <a href="https://arxiv.org/format/2009.11070">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.4204/EPTCS.325.10">10.4204/EPTCS.325.10 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Variant-based Equational Unification under Constructor Symbols </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Aparicio-S%C3%A1nchez%2C+D">Dami谩n Aparicio-S谩nchez</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Sapi%C3%B1a%2C+J">Julia Sapi帽a</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2009.11070v1-abstract-short" style="display: inline;"> Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. A narrowing-based equational unification algorithm relying on the concept of the variants of a term is available in the most recent version of Maude, version 3.0, which provides quite sophisticated unification features. A variant of a term t i… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2009.11070v1-abstract-full').style.display = 'inline'; document.getElementById('2009.11070v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2009.11070v1-abstract-full" style="display: none;"> Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. A narrowing-based equational unification algorithm relying on the concept of the variants of a term is available in the most recent version of Maude, version 3.0, which provides quite sophisticated unification features. A variant of a term t is a pair consisting of a substitution sigma and the canonical form of tsigma. Variant-based unification is decidable when the equational theory satisfies the finite variant property. However, this unification procedure does not take into account constructor symbols and, thus, may compute many more unifiers than the necessary or may not be able to stop immediately. In this paper, we integrate the notion of constructor symbol into the variant-based unification algorithm. Our experiments on positive and negative unification problems show an impressive speedup. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2009.11070v1-abstract-full').style.display = 'none'; document.getElementById('2009.11070v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 21 September, 2020; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2020. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">In Proceedings ICLP 2020, arXiv:2009.09158. arXiv admin note: substantial text overlap with arXiv:1909.08241</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> EPTCS 325, 2020, pp. 38-51 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1910.08416">arXiv:1910.08416</a> <span> [<a href="https://arxiv.org/pdf/1910.08416">pdf</a>, <a href="https://arxiv.org/format/1910.08416">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Symbolic Computation">cs.SC</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1016/j.jlamp.2019.100497">10.1016/j.jlamp.2019.100497 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Programming and Symbolic Computation in Maude </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Dur%C3%A1n%2C+F">Francisco Dur谩n</a>, <a href="/search/cs?searchtype=author&query=Eker%2C+S">Steven Eker</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Mart%C3%AD-Oliet%2C+N">Narciso Mart铆-Oliet</a>, <a href="/search/cs?searchtype=author&query=Meseguer%2C+J">Jos茅 Meseguer</a>, <a href="/search/cs?searchtype=author&query=Rubio%2C+R">Rub茅n Rubio</a>, <a href="/search/cs?searchtype=author&query=Talcott%2C+C">Carolyn Talcott</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1910.08416v1-abstract-short" style="display: inline;"> Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurr… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1910.08416v1-abstract-full').style.display = 'inline'; document.getElementById('1910.08416v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1910.08416v1-abstract-full" style="display: none;"> Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurrent systems and for increasing the power of formal tools. We present several new symbolic features of Maude that enhance formal reasoning about Maude programs and the effectiveness of formal tools. They include: (i) very general unification modulo user-definable equational theories, and (ii) symbolic reachability analysis of concurrent systems using narrowing. The paper does not focus just on symbolic features: it also describes several other new Maude features, including: (iii) Maude's strategy language for controlling rewriting, and (iv) external objects that allow flexible interaction of Maude object-based concurrent systems with the external world. In particular, meta-interpreters are external objects encapsulating Maude interpreters that can interact with many other objects. To make the paper self-contained and give a reasonably complete language overview, we also review the basic Maude features for equational rewriting and rewriting with rules, Maude programming of concurrent object systems, and reflection. Furthermore, we include many examples illustrating all the Maude notions and features described in the paper. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1910.08416v1-abstract-full').style.display = 'none'; document.getElementById('1910.08416v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 18 October, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2019. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Journal of Logical and Algebraic Methods in Programming, 2019</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1909.08241">arXiv:1909.08241</a> <span> [<a href="https://arxiv.org/pdf/1909.08241">pdf</a>, <a href="https://arxiv.org/format/1909.08241">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.4204/EPTCS.306.21">10.4204/EPTCS.306.21 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Most General Variant Unifiers </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Sapi%C3%B1a%2C+J">Julia Sapi帽a</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1909.08241v1-abstract-short" style="display: inline;"> Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. Equational unification is of special relevance to automated deduction, theorem proving, protocol analysis, partial evaluation, model checking, etc. Several algorithms have been developed in the literature for specific equational theories, such… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1909.08241v1-abstract-full').style.display = 'inline'; document.getElementById('1909.08241v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1909.08241v1-abstract-full" style="display: none;"> Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. Equational unification is of special relevance to automated deduction, theorem proving, protocol analysis, partial evaluation, model checking, etc. Several algorithms have been developed in the literature for specific equational theories, such as associative-commutative symbols, exclusive-or, Diffie-Hellman, or Abelian Groups. Narrowing was proved to be complete for unification and several cases have been studied where narrowing provides a decidable unification algorithm. A new narrowing-based equational unification algorithm relying on the concept of the variants of a term has been developed and it is available in the most recent version of Maude, version 2.7.1, which provides quite sophisticated unification features. A variant of a term t is a pair consisting of a substitution sigma and the canonical form of tsigma. Variant-based unification is decidable when the equational theory satisfies the finite variant property. However, it may compute many more unifiers than the necessary and, in this paper, we explore how to strengthen the variant-based unification algorithm implemented in Maude to produce a minimal set of most general variant unifiers. Our experiments suggest that this new adaptation of the variant-based unification is more efficient both in execution time and in the number of computed variant unifiers than the original algorithm available in Maude. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1909.08241v1-abstract-full').style.display = 'none'; document.getElementById('1909.08241v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 18 September, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2019. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">In Proceedings ICLP 2019, arXiv:1909.07646</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> EPTCS 306, 2019, pp. 154-167 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1907.10919">arXiv:1907.10919</a> <span> [<a href="https://arxiv.org/pdf/1907.10919">pdf</a>, <a href="https://arxiv.org/format/1907.10919">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> Symbolic Analysis of Maude Theories with Narval </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Alpuente%2C+M">Mar铆a Alpuente</a>, <a href="/search/cs?searchtype=author&query=Ballis%2C+D">Demis Ballis</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Sapi%C3%B1a%2C+J">Julia Sapi帽a</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1907.10919v1-abstract-short" style="display: inline;"> Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude's symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1907.10919v1-abstract-full').style.display = 'inline'; document.getElementById('1907.10919v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1907.10919v1-abstract-full" style="display: none;"> Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude's symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations. This paper is under consideration for acceptance in TPLP. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1907.10919v1-abstract-full').style.display = 'none'; document.getElementById('1907.10919v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 25 July, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2019. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Paper presented at the 35th International Conference on Logic Programming (ICLP 2019), Las Cruces, New Mexico, USA, 20-25 September 2019, 16 pages</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1904.09946">arXiv:1904.09946</a> <span> [<a href="https://arxiv.org/pdf/1904.09946">pdf</a>, <a href="https://arxiv.org/ps/1904.09946">ps</a>, <a href="https://arxiv.org/format/1904.09946">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> Strand Spaces with Choice via a Process Algebra Semantics </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Yang%2C+F">Fan Yang</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Meadows%2C+C">Catherine Meadows</a>, <a href="/search/cs?searchtype=author&query=Meseguer%2C+J">Jos茅 Meseguer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1904.09946v1-abstract-short" style="display: inline;"> Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic protocols, particularly as it is used in the Maude-NPA cryptographic protocol analysis tool. To achieve this goal, we develop and give form… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1904.09946v1-abstract-full').style.display = 'inline'; document.getElementById('1904.09946v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1904.09946v1-abstract-full" style="display: none;"> Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic protocols, particularly as it is used in the Maude-NPA cryptographic protocol analysis tool. To achieve this goal, we develop and give formal semantics to a process algebra for cryptographic protocols that supports a rich taxonomy of choice primitives for composing strand spaces. In our taxonomy, deterministic and non-deterministic choices are broken down further. Non-deterministic choice can be either explicit, i.e., one of two paths is chosen, or implicit, i.e., the value of a variable is chosen non-deterministically. Likewise, deterministic choice can be either an explicit if-then-else choice, i.e., one path is chosen if a predicate is satisfied, while the other is chosen if it is not, or implicit deterministic choice, i.e., execution continues only if a certain pattern is matched. We have identified a class of choices which includes finite branching and some cases of infinite branching, which we address in this paper. We provide a bisimulation result between the expected forwards execution semantics of the new process algebra and the original symbolic backwards semantics of Maude-NPA that preserves attack reachability. We have fully integrated the process algebra syntax and its transformation into strands in Maude-NPA. We illustrate its expressive power and naturalness with various examples, and show how it can be effectively used in formal analysis. This allows users to write protocols from now on using the process syntax, which is more convenient for expressing choice than the strand space syntax, in which choice can only be specified implicitly, via two or more strands that are identical until the choice point. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1904.09946v1-abstract-full').style.display = 'none'; document.getElementById('1904.09946v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 22 April, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2019. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1808.05097">arXiv:1808.05097</a> <span> [<a href="https://arxiv.org/pdf/1808.05097">pdf</a>, <a href="https://arxiv.org/ps/1808.05097">ps</a>, <a href="https://arxiv.org/format/1808.05097">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> Homeomorphic Embedding modulo Combinations of Associativity and Commutativity Axioms </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Alpuente%2C+M">Mar铆a Alpuente</a>, <a href="/search/cs?searchtype=author&query=Cuenca-Ortega%2C+A">Angel Cuenca-Ortega</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Meseguer%2C+J">Jos茅 Meseguer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1808.05097v2-abstract-short" style="display: inline;"> The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding r… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1808.05097v2-abstract-full').style.display = 'inline'; document.getElementById('1808.05097v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1808.05097v2-abstract-full" style="display: none;"> The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order-sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of increasingly efficient formulations of the homeomorphic embedding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1808.05097v2-abstract-full').style.display = 'none'; document.getElementById('1808.05097v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 November, 2018; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 15 August, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> August 2018. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Report number:</span> LOPSTR/2018/8 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1806.07209">arXiv:1806.07209</a> <span> [<a href="https://arxiv.org/pdf/1806.07209">pdf</a>, <a href="https://arxiv.org/format/1806.07209">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> </div> </div> <p class="title is-5 mathjax"> Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Gonz%C3%A1lez-Burgue%C3%B1o%2C+A">Antonio Gonz谩lez-Burgue帽o</a>, <a href="/search/cs?searchtype=author&query=Aparicio%2C+D">Dami谩n Aparicio</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Meadows%2C+C">Catherine Meadows</a>, <a href="/search/cs?searchtype=author&query=Meseguer%2C+J">Jos茅 Meseguer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1806.07209v1-abstract-short" style="display: inline;"> In this paper, we perform an automated analysis of two devices developed by Yubico: YubiKey, designed to authenticate a user to network-based services, and YubiHSM, Yubicos hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol analyzer. Although previous work has been done applying automated tools to these devices, to the best of our knowledge there has been no com… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1806.07209v1-abstract-full').style.display = 'inline'; document.getElementById('1806.07209v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1806.07209v1-abstract-full" style="display: none;"> In this paper, we perform an automated analysis of two devices developed by Yubico: YubiKey, designed to authenticate a user to network-based services, and YubiHSM, Yubicos hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol analyzer. Although previous work has been done applying automated tools to these devices, to the best of our knowledge there has been no completely automated analysis to date. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. In this work, we have been able to both prove properties of YubiKey and find the known attacks on the YubiHSM, in a completely automated way beyond the capabilities of previous work in the literature. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1806.07209v1-abstract-full').style.display = 'none'; document.getElementById('1806.07209v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 19 June, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2018. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1707.05599">arXiv:1707.05599</a> <span> [<a href="https://arxiv.org/pdf/1707.05599">pdf</a>, <a href="https://arxiv.org/format/1707.05599">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> Inspecting Maude Variants with GLINTS </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Alpuente%2C+M">Mar铆a Alpuente</a>, <a href="/search/cs?searchtype=author&query=Cuenca-Ortega%2C+A">Angel Cuenca-Ortega</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Sapi%C3%B1a%2C+J">Julia Sapi帽a</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1707.05599v1-abstract-short" style="display: inline;"> This paper introduces GLINTS, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including order-sorted equational unification for convergent theories modulo axioms such as associativity, commutativity, and identity (ACU). This novel equational unification relies on built-in gen… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1707.05599v1-abstract-full').style.display = 'inline'; document.getElementById('1707.05599v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1707.05599v1-abstract-full" style="display: none;"> This paper introduces GLINTS, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including order-sorted equational unification for convergent theories modulo axioms such as associativity, commutativity, and identity (ACU). This novel equational unification relies on built-in generation of the set of 'variants' of a term $t$, i.e., the canonical form of $t 蟽$ for a computed substitution $蟽$. Variant generation relies on a novel narrowing strategy called 'folding variant narrowing' that opens up new applications in formal reasoning, theorem proving, testing, protocol analysis, and model checking, especially when the theory satisfies the 'finite variant property', i.e., there is a finite number of most general variants for every term in the theory. However, variant narrowing computations can be extremely involved and are simply presented in text format by Maude, often being too heavy to be debugged or even understood. The GLINTS system provides support for (i) determining whether a given theory satisfies the finite variant property, (ii) thoroughly exploring variant narrowing computations, (iii) automatic checking of node 'embedding' and 'closedness' modulo axioms, and (iv) querying and inspecting selected parts of the variant trees. This paper is under consideration for acceptance in TPLP. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1707.05599v1-abstract-full').style.display = 'none'; document.getElementById('1707.05599v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 18 July, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2017. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Paper presented at the 33nd International Conference on Logic Programming (ICLP 2017), Melbourne, Australia, August 28 to September 1, 2017 15 pages, LaTeX, 7 PDF figures, 2 PNG figures</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1701.00233">arXiv:1701.00233</a> <span>  </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.4204/EPTCS.235">10.4204/EPTCS.235 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cirstea%2C+H">Horatiu Cirstea</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1701.00233v1-abstract-short" style="display: inline;"> This volume contains the formal proceedings of the Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), held on 23rd June 2016 in Porto, Portugal, as a satellite event of the First International Conference on Formal Structures for Computation and Deduction (FSCD 2016). The workshop brought together researchers working on program transformatio… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1701.00233v1-abstract-full').style.display = 'inline'; document.getElementById('1701.00233v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1701.00233v1-abstract-full" style="display: none;"> This volume contains the formal proceedings of the Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), held on 23rd June 2016 in Porto, Portugal, as a satellite event of the First International Conference on Formal Structures for Computation and Deduction (FSCD 2016). The workshop brought together researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1701.00233v1-abstract-full').style.display = 'none'; document.getElementById('1701.00233v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 1 January, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2017. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Dedicated to the memory of Kristoffer H. Rose</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> EPTCS 235, 2017 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1608.03424">arXiv:1608.03424</a> <span> [<a href="https://arxiv.org/pdf/1608.03424">pdf</a>, <a href="https://arxiv.org/ps/1608.03424">ps</a>, <a href="https://arxiv.org/format/1608.03424">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> Partial Evaluation of Order-sorted Equational Programs modulo Axioms </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Alpuente%2C+M">Maria Alpuente</a>, <a href="/search/cs?searchtype=author&query=Cuenca%2C+A">Angel Cuenca</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Meseguer%2C+J">Jose Meseguer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1608.03424v1-abstract-short" style="display: inline;"> Partial evaluation (PE) is a powerful and general program optimization technique with many successful applications. However, it has never been investigated in the context of expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: 1) rich type structures with sorts, subsorts and overloading; 2) equational rewriting modulo axioms such as commutativity, associativi… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1608.03424v1-abstract-full').style.display = 'inline'; document.getElementById('1608.03424v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1608.03424v1-abstract-full" style="display: none;"> Partial evaluation (PE) is a powerful and general program optimization technique with many successful applications. However, it has never been investigated in the context of expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: 1) rich type structures with sorts, subsorts and overloading; 2) equational rewriting modulo axioms such as commutativity, associativity-commutativity, and associativity-commutativity-identity. In this extended abstract, we illustrate the key concepts by showing how they apply to partial evaluation of expressive rule-based programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on equational least general generalization for ensuring global termination. We demonstrate the use of the resulting partial evaluator for program optimization on several examples where it shows significant speed-ups. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1608.03424v1-abstract-full').style.display = 'none'; document.getElementById('1608.03424v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 11 August, 2016; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> August 2016. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Report number:</span> LOPSTR/2016/38 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1603.00087">arXiv:1603.00087</a> <span> [<a href="https://arxiv.org/pdf/1603.00087">pdf</a>, <a href="https://arxiv.org/ps/1603.00087">ps</a>, <a href="https://arxiv.org/format/1603.00087">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> Effective Sequential Protocol Composition in Maude-NPA </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Santiago%2C+S">Sonia Santiago</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Meadows%2C+C">Catherine Meadows</a>, <a href="/search/cs?searchtype=author&query=Meseguer%2C+J">Jos茅 Meseguer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1603.00087v1-abstract-short" style="display: inline;"> Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and its operational semantics to support dynamic sequential composition of protocols, so that protocols can be s… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1603.00087v1-abstract-full').style.display = 'inline'; document.getElementById('1603.00087v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1603.00087v1-abstract-full" style="display: none;"> Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and its operational semantics to support dynamic sequential composition of protocols, so that protocols can be specified separately and composed when desired. This allows one to reason about many different compositions with minimal changes to the specification, as well as improving, in terms of both performance and ease of specification, on an earlier composition extension we presented in [18]. We show how compositions can be defined and executed symbolically in Maude-NPA using the compositional syntax and semantics. We also provide an experimental analysis of the performance of Maude-NPA using the compositional syntax and semantics, and compare it to the performance of a syntax and semantics for composition developed in earlier research. Finally, in the conclusion we give some lessons learned about the best ways of extending narrowing-based state reachability tools, as well as comparison with related work and future plans. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1603.00087v1-abstract-full').style.display = 'none'; document.getElementById('1603.00087v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 29 February, 2016; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2016. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1501.01693">arXiv:1501.01693</a> <span>  </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.4204/EPTCS.173">10.4204/EPTCS.173 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Proceedings XIV Jornadas sobre Programaci贸n y Lenguajes </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1501.01693v1-abstract-short" style="display: inline;"> This volume contains a selection of the papers presented at the XIV Jornadas sobre Programaci贸n y Lenguajes (PROLE 2014), held at C谩diz, Spain, during September 17th-19th, 2014. Previous editions of the workshop were held in Madrid (2013), Almer铆a (2012), A Coru帽a (2011), Val茅ncia (2010), San Sebasti谩n (2009), Gij贸n (2008), Zaragoza (2007), Sitges (2006), Granada (2005), M谩laga (2004), Alicante (2… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1501.01693v1-abstract-full').style.display = 'inline'; document.getElementById('1501.01693v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1501.01693v1-abstract-full" style="display: none;"> This volume contains a selection of the papers presented at the XIV Jornadas sobre Programaci贸n y Lenguajes (PROLE 2014), held at C谩diz, Spain, during September 17th-19th, 2014. Previous editions of the workshop were held in Madrid (2013), Almer铆a (2012), A Coru帽a (2011), Val茅ncia (2010), San Sebasti谩n (2009), Gij贸n (2008), Zaragoza (2007), Sitges (2006), Granada (2005), M谩laga (2004), Alicante (2003), El Escorial (2002), and Almagro (2001). Programming languages provide a conceptual framework which is necessary for the development, analysis, optimization and understanding of programs and programming tasks. The aim of the PROLE series of conferences (PROLE stems from the spanish PROgramaci贸n y LEnguajes) is to serve as a meeting point for spanish research groups which develop their work in the area of programming and programming languages. The organization of this series of events aims at fostering the exchange of ideas, experiences and results among these groups. Promoting further collaboration is also one of the main goals of PROLE. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1501.01693v1-abstract-full').style.display = 'none'; document.getElementById('1501.01693v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 7 January, 2015; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2015. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> EPTCS 173, 2015 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1204.5318">arXiv:1204.5318</a> <span>  </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.4204/EPTCS.82">10.4204/EPTCS.82 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Proceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1204.5318v1-abstract-short" style="display: inline;"> This volume contains a selection of the papers presented at the 10th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'2011), held on 29 May 2011 in Novi Sad, Serbia. Previous editions of the workshop were held in Utrecht (2001), Copenhagen (2002), Valencia (2003), Aachen (2004), Nara (2005), Seattle (2006), Paris (2007), Hagenberg (2008), Brasilia (2009), and Edinbu… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1204.5318v1-abstract-full').style.display = 'inline'; document.getElementById('1204.5318v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1204.5318v1-abstract-full" style="display: none;"> This volume contains a selection of the papers presented at the 10th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'2011), held on 29 May 2011 in Novi Sad, Serbia. Previous editions of the workshop were held in Utrecht (2001), Copenhagen (2002), Valencia (2003), Aachen (2004), Nara (2005), Seattle (2006), Paris (2007), Hagenberg (2008), Brasilia (2009), and Edinburgh (2010); the last one as a joint workshop with the STRATEGIES workshop. The WRS 2011 workshop was part of the Federated Conference on Rewriting, Deduction, and Programming (RDP'1), which grouped together different events including the 22th International Conference on Rewriting Techniques and Applications (RTA'11) and the 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11). <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1204.5318v1-abstract-full').style.display = 'none'; document.getElementById('1204.5318v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 24 April, 2012; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2012. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> EPTCS 82, 2012 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1105.5282">arXiv:1105.5282</a> <span> [<a href="https://arxiv.org/pdf/1105.5282">pdf</a>, <a href="https://arxiv.org/format/1105.5282">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> State Space Reduction in the Maude-NRL Protocol Analyzer </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Meadows%2C+C">Catherine Meadows</a>, <a href="/search/cs?searchtype=author&query=Meseguer%2C+J">Jose Meseguer</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1105.5282v1-abstract-short" style="display: inline;"> The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic pr… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1105.5282v1-abstract-full').style.display = 'inline'; document.getElementById('1105.5282v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1105.5282v1-abstract-full" style="display: none;"> The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic properties that includes many crypto-systems of interest such as, for example, one-time pads and Diffie-Hellman. Maude-NPA, like the original NPA, looks for attacks by searching backwards from an insecure attack state, and assumes an unbounded number of sessions. Because of the unbounded number of sessions and the support for different equational theories, it is necessary to develop ways of reducing the search space and avoiding infinite search paths. In order for the techniques to prove useful, they need not only to speed up the search, but should not violate completeness, so that failure to find attacks still guarantees security. In this paper we describe some state space reduction techniques that we have implemented in Maude-NPA. We also provide completeness proofs, and experimental evaluations of their effect on the performance of Maude-NPA. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1105.5282v1-abstract-full').style.display = 'none'; document.getElementById('1105.5282v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 26 May, 2011; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2011. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1006.4304">arXiv:1006.4304</a> <span> [<a href="https://arxiv.org/pdf/1006.4304">pdf</a>, <a href="https://arxiv.org/ps/1006.4304">ps</a>, <a href="https://arxiv.org/format/1006.4304">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> Abstract Certification of Global Non-Interference in Rewriting Logic </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Alba-Castro%2C+M">Mauricio Alba-Castro</a>, <a href="/search/cs?searchtype=author&query=Alpuente%2C+M">Mar铆a Alpuente</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1006.4304v1-abstract-short" style="display: inline;"> Non-interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this paper, we present a novel security model for global non-interference which approximates non-interference as a safety property. We also propose a certification technique for global non-interference of comp… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1006.4304v1-abstract-full').style.display = 'inline'; document.getElementById('1006.4304v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1006.4304v1-abstract-full" style="display: none;"> Non-interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this paper, we present a novel security model for global non-interference which approximates non-interference as a safety property. We also propose a certification technique for global non-interference of complete Java classes based on rewriting logic, a very general logical and semantic framework that is efficiently implemented in the high-level programming language Maude. Starting from an existing Java semantics specification written in Maude, we develop an extended, information-flow Java semantics that allows us to correctly observe global non-interference policies. In order to achieve a finite state transition system, we develop an abstract Java semantics that we use for secure and effective non-interference Java analysis. The analysis produces certificates that are independently checkable and are small enough to be used in practice. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1006.4304v1-abstract-full').style.display = 'none'; document.getElementById('1006.4304v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 22 June, 2010; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2010. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">26 pages. ACM class (full): D.2.4 [Software Engineering]: Software/Program Verification---Formal Methods; F.3.2 [Logics and Meaning of Programs]: Semantics of Programming Languages---Program Analysis</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> D.2.4; F.3.2 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/cs/0601039">arXiv:cs/0601039</a> <span> [<a href="https://arxiv.org/pdf/cs/0601039">pdf</a>, <a href="https://arxiv.org/ps/cs/0601039">ps</a>, <a href="https://arxiv.org/format/cs/0601039">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Programming Languages">cs.PL</span> </div> </div> <p class="title is-5 mathjax"> Removing Redundant Arguments Automatically </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Alpuente%2C+M">Maria Alpuente</a>, <a href="/search/cs?searchtype=author&query=Escobar%2C+S">Santiago Escobar</a>, <a href="/search/cs?searchtype=author&query=Lucas%2C+S">Salvador Lucas</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="cs/0601039v1-abstract-short" style="display: inline;"> The application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers usually (or presumably) do not write. An example is the introduction of redundant arguments in the functions defined in the program. Redundancy of a parameter means that replacing it by any expression does not change th… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('cs/0601039v1-abstract-full').style.display = 'inline'; document.getElementById('cs/0601039v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="cs/0601039v1-abstract-full" style="display: none;"> The application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers usually (or presumably) do not write. An example is the introduction of redundant arguments in the functions defined in the program. Redundancy of a parameter means that replacing it by any expression does not change the result. In this work, we provide methods for the analysis and elimination of redundant arguments in term rewriting systems as a model for the programs that can be written in more sophisticated languages. On the basis of the uselessness of redundant arguments, we also propose an erasure procedure which may avoid wasteful computations while still preserving the semantics (under ascertained conditions). A prototype implementation of these methods has been undertaken, which demonstrates the practicality of our approach. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('cs/0601039v1-abstract-full').style.display = 'none'; document.getElementById('cs/0601039v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 10 January, 2006; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2006. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Accepted for publication in Theory and Practice of Logic Programming</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> D.2.4; F.3.1; F.3.3; I.2.2; I.2.5 </p> </li> </ol> <div class="is-hidden-tablet">  <span class="help" style="display: inline-block;"><a href="https://github.com/arXiv/arxiv-search/releases">Search v0.5.6 released 2020-02-24</a>  </span> </div> </div> </main> <footer> <div class="columns is-desktop" role="navigation" aria-label="Secondary">  <div class="column"> <div class="columns"> <div class="column"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/about">About</a></li> <li><a href="https://info.arxiv.org/help">Help</a></li> </ul> </div> <div class="column"> <ul class="nav-spaced"> <li> <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><title>contact arXiv</title><desc>Click here to contact arXiv</desc><path d="M502.3 190.8c3.9-3.1 9.7-.2 9.7 4.7V400c0 26.5-21.5 48-48 48H48c-26.5 0-48-21.5-48-48V195.6c0-5 5.7-7.8 9.7-4.7 22.4 17.4 52.1 39.5 154.1 113.6 21.1 15.4 56.7 47.8 92.2 47.6 35.7.3 72-32.8 92.3-47.6 102-74.1 131.6-96.3 154-113.7zM256 320c23.2.4 56.6-29.2 73.4-41.4 132.7-96.3 142.8-104.7 173.4-128.7 5.8-4.5 9.2-11.5 9.2-18.9v-19c0-26.5-21.5-48-48-48H48C21.5 64 0 85.5 0 112v19c0 7.4 3.4 14.3 9.2 18.9 30.6 23.9 40.7 32.4 173.4 128.7 16.8 12.2 50.2 41.8 73.4 41.4z"/></svg> <a href="https://info.arxiv.org/help/contact.html"> Contact</a> </li> <li> <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><title>subscribe to arXiv mailings</title><desc>Click here to subscribe</desc><path d="M476 3.2L12.5 270.6c-18.1 10.4-15.8 35.6 2.2 43.2L121 358.4l287.3-253.2c5.5-4.9 13.3 2.6 8.6 8.3L176 407v80.5c0 23.6 28.5 32.9 42.5 15.8L282 426l124.6 52.2c14.2 6 30.4-2.9 33-18.2l72-432C515 7.8 493.3-6.8 476 3.2z"/></svg> <a href="https://info.arxiv.org/help/subscribe"> Subscribe</a> </li> </ul> </div> </div> </div>   <div class="column"> <div class="columns"> <div class="column"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/help/license/index.html">Copyright</a></li> <li><a href="https://info.arxiv.org/help/policies/privacy_policy.html">Privacy Policy</a></li> </ul> </div> <div class="column sorry-app-links"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/help/web_accessibility.html">Web Accessibility Assistance</a></li> <li> <p class="help"> <a class="a11y-main-link" href="https://status.arxiv.org" target="_blank">arXiv Operational Status <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 256 512" class="icon filter-dark_grey" role="presentation"><path d="M224.3 273l-136 136c-9.4 9.4-24.6 9.4-33.9 0l-22.6-22.6c-9.4-9.4-9.4-24.6 0-33.9l96.4-96.4-96.4-96.4c-9.4-9.4-9.4-24.6 0-33.9L54.3 103c9.4-9.4 24.6-9.4 33.9 0l136 136c9.5 9.4 9.5 24.6.1 34z"/></svg></a><br> Get status notifications via <a class="is-link" href="https://subscribe.sorryapp.com/24846f03/email/new" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><path d="M502.3 190.8c3.9-3.1 9.7-.2 9.7 4.7V400c0 26.5-21.5 48-48 48H48c-26.5 0-48-21.5-48-48V195.6c0-5 5.7-7.8 9.7-4.7 22.4 17.4 52.1 39.5 154.1 113.6 21.1 15.4 56.7 47.8 92.2 47.6 35.7.3 72-32.8 92.3-47.6 102-74.1 131.6-96.3 154-113.7zM256 320c23.2.4 56.6-29.2 73.4-41.4 132.7-96.3 142.8-104.7 173.4-128.7 5.8-4.5 9.2-11.5 9.2-18.9v-19c0-26.5-21.5-48-48-48H48C21.5 64 0 85.5 0 112v19c0 7.4 3.4 14.3 9.2 18.9 30.6 23.9 40.7 32.4 173.4 128.7 16.8 12.2 50.2 41.8 73.4 41.4z"/></svg>email</a> or <a class="is-link" href="https://subscribe.sorryapp.com/24846f03/slack/new" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 448 512" class="icon filter-black" role="presentation"><path d="M94.12 315.1c0 25.9-21.16 47.06-47.06 47.06S0 341 0 315.1c0-25.9 21.16-47.06 47.06-47.06h47.06v47.06zm23.72 0c0-25.9 21.16-47.06 47.06-47.06s47.06 21.16 47.06 47.06v117.84c0 25.9-21.16 47.06-47.06 47.06s-47.06-21.16-47.06-47.06V315.1zm47.06-188.98c-25.9 0-47.06-21.16-47.06-47.06S139 32 164.9 32s47.06 21.16 47.06 47.06v47.06H164.9zm0 23.72c25.9 0 47.06 21.16 47.06 47.06s-21.16 47.06-47.06 47.06H47.06C21.16 243.96 0 222.8 0 196.9s21.16-47.06 47.06-47.06H164.9zm188.98 47.06c0-25.9 21.16-47.06 47.06-47.06 25.9 0 47.06 21.16 47.06 47.06s-21.16 47.06-47.06 47.06h-47.06V196.9zm-23.72 0c0 25.9-21.16 47.06-47.06 47.06-25.9 0-47.06-21.16-47.06-47.06V79.06c0-25.9 21.16-47.06 47.06-47.06 25.9 0 47.06 21.16 47.06 47.06V196.9zM283.1 385.88c25.9 0 47.06 21.16 47.06 47.06 0 25.9-21.16 47.06-47.06 47.06-25.9 0-47.06-21.16-47.06-47.06v-47.06h47.06zm0-23.72c-25.9 0-47.06-21.16-47.06-47.06 0-25.9 21.16-47.06 47.06-47.06h117.84c25.9 0 47.06 21.16 47.06 47.06 0 25.9-21.16 47.06-47.06 47.06H283.1z"/></svg>slack</a> </p> </li> </ul> </div> </div> </div>  </div> </footer> <script src="https://static.arxiv.org/static/base/1.0.0a5/js/member_acknowledgement.js"></script> </body> </html>

CINXE.COM

Search | arXiv e-print repository