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

Reasoning about security properties involves reasoning about where theinformation of a system is located, and how it evolves over time. While mostsecurity analysis techniques need to cope with some notions of informationlocality and knowledge propagation, usually they do not provide a generallanguage for expressing arbitrary properties involving local knowledge andknowledge transfer. Building on this observation, we introduce a framework forsecurity protocol analysis based on dynamic spatial logic specifications. Ourcomputational model is a variant of existing pi-calculi, while specificationsare expressed in a dynamic spatial logic extended with an epistemic operator.We present the syntax and semantics of the model and logic, and discuss theexpressiveness of the approach, showing it complete for passive attackers. Wealso prove that generic Dolev-Yao attackers may be mechanically determined forany deterministic finite protocol, and discuss how this result may be used toreason about security properties of open systems. We also present amodel-checking algorithm for our logic, which has been implemented as anextension to the SLMC system.

A Spatial-Epistemic Logic for Reasoning about Security Protocols