English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Rewriting theory is becoming of increasing interest to security researchers. Rewriting logic is a form of logic which has the advantage of being straightforward to automate, thus making it useful not only for specifying security properties of systems, but verifying that these properties hold. One particular application in which rewriting is making important contributions is the verification of security protocols that are used to protect communication in networks. Security protocols are used now in more and more applications as the extent of our networked environment grows. Since the early 1980s, a growing effort has been put into the automated verification of such protocols. Following Dolev and Yao (1983), the most popular model of protocols relies on a representation of messages as terms: each cryptographic primitive is a function symbol. Variables usually represent parts of the messages that cannot be analysed, hence that could be replaced by an attacker who intercepts and forges new messages. That is why, since this area of research started, term unification plays an important role in the automated verification of security protocols. Until ten years ago, only a few security primitives were considered. More recently, several other primitives were introduced, for instance exclusive or. For most examples, the free term algebra is too rough for a faithful abstraction of the cryptographic primitives. Thus it is necessary to require that the function symbols used in specifying the cryptosystems satisfy some algebraic properties: the messages are now member of a quotient term algebra. This quotient structure is specified by a set of equations. Many of these equations can be specified as rewrite rules, which allows us to bring rewriting theory to bear on the problem.

Special Issue on Security and Rewriting Foreword