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 Tools annual

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference systemfor reasoning about the security of cryptographic protocols in which thecryptosystems satisfy different equational properties. It both extends andprovides a formal framework for the original NRL Protocol Analyzer, whichsupported equational reasoning in a more limited way. Maude-NPA supports a widevariety of algebraic properties that includes many crypto-systems of interestsuch as, for example, one-time pads and Diffie-Hellman. Maude-NPA, like theoriginal NPA, looks for attacks by searching backwards from an insecure attackstate, and assumes an unbounded number of sessions. Because of the unboundednumber of sessions and the support for different equational theories, it isnecessary to develop ways of reducing the search space and avoiding infinitesearch paths. In order for the techniques to prove useful, they need not onlyto speed up the search, but should not violate completeness, so that failure tofind attacks still guarantees security. In this paper we describe some statespace reduction techniques that we have implemented in Maude-NPA. We alsoprovide completeness proofs, and experimental evaluations of their effect onthe performance of Maude-NPA.

State Space Reduction in the Maude-NRL Protocol Analyzer