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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Automated verification has become an essential part in the securityevaluation of cryptographic protocols. In this context privacy-type propertiesare often modelled by indistinguishability statements, expressed as behaviouralequivalences in a process calculus. In this paper we contribute both to thetheory and practice of this verification problem. We establish new complexityresults for static equivalence, trace equivalence and labelled bisimilarity andprovide a decision procedure for these equivalences in the case of a boundednumber of protocol sessions. Our procedure is the first to decide traceequivalence and labelled bisimilarity exactly for a large variety ofcryptographic primitives -- those that can be represented by a subtermconvergent destructor rewrite system. We also implemented the procedure in anew tool, DeepSec. We showed through extensive experiments that it issignificantly more efficient than other similar tools, while at the same timeraises the scope of the protocols that can be analysed.

DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice