Deciding knowledge in security protocols under equational theories

DOI10.1016/j.tcs.2006.08.032zbMath1153.94339OpenAlexW2060349224WikidataQ115036558 ScholiaQ115036558MaRDI QIDQ860894

Publication date: 9 January 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.08.032

zbMATH Keywords

cryptography decidability

Mathematics Subject Classification ID

Cryptography (94A60) Decidability of theories and sets of sentences (03B25) Authentication, digital signatures and secret sharing (94A62)

Related Items (39)

Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity ⋮ Trace Equivalence and Epistemic Logic to Express Security Properties ⋮ Algorithmic problems in the symbolic approach to the verification of automatically synthesized cryptosystems ⋮ Model Checking Security Protocols ⋮ Alice and Bob: Reconciling Formal Models and Implementation ⋮ Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties ⋮ Stateful applied pi calculus: observational equivalence and labelled bisimilarity ⋮ A game-theoretic framework for specification and verification of cryptographic protocols ⋮ Deciding equivalence-based properties using constraint solving ⋮ An Equation-Based Classical Logic ⋮ A Probabilistic Applied Pi–Calculus ⋮ Deciding Knowledge in Security Protocols for Monoidal Equational Theories ⋮ When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus ⋮ Unnamed Item ⋮ A pure labeled transition semantics for the applied pi calculus ⋮ Reducing equational theories for the decision of static equivalence ⋮ Computing knowledge in security protocols under convergent equational theories ⋮ Decidability and combination results for two notions of knowledge in security protocols ⋮ Probabilistic logic over equations and domain restrictions ⋮ Challenges in the Automated Verification of Security Protocols ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ Intruder deducibility constraints with negation. Decidability and application to secured service compositions ⋮ Intruder deduction problem for locally stable theories with normal forms and inverses ⋮ Automated verification of selected equivalences for security protocols ⋮ A Complete Symbolic Bisimilarity for an Extended Spi Calculus ⋮ Hierarchical combination of intruder theories ⋮ Automating Security Analysis: Symbolic Equivalence of Constraint Systems ⋮ Computing Knowledge in Security Protocols under Convergent Equational Theories ⋮ Compiling and securing cryptographic protocols ⋮ A spatial equational logic for the applied \(\pi \)-calculus ⋮ Deciding Security for Protocols with Recursive Tests ⋮ Symbolic Bisimulation for the Applied Pi Calculus ⋮ A Proof Theoretic Analysis of Intruder Theories ⋮ YAPA: A Generic Tool for Computing Intruder Knowledge ⋮ Deciding knowledge in security protocols under some e-voting theories ⋮ Computationally Sound Symbolic Analysis of Probabilistic Protocols with Ideal Setups ⋮ Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model ⋮ Formalizing provable anonymity in Isabelle/HOL ⋮ Terminating non-disjoint combined unification

Cites Work

This page was built for publication: Deciding knowledge in security protocols under equational theories