From security protocols to pushdown automata

DOI10.1145/2811262MaRDI QIDQ5277904zbMATH OpenOpenAlexFDO

Authors Rémy Chrétien, Véronique Cortier, Stéphanie Delaune

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2811262

zbMATH Keywords

formal proofssecurity protocolstrace equivalenceverification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Cryptography (94A60)

Recommendations

• From security protocols to pushdown automata
• Deciding equivalence-based properties using constraint solving
• POR for security protocol equivalences. Beyond action-determinism
• A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
• SPEC: an equivalence checker for security protocols

Cites work

• Automated verification of selected equivalences for security protocols
• Decidability of equivalence of symbolic derivations
• scientific article; zbMATH DE number 2043527 (Why is no real title available?)
• scientific article; zbMATH DE number 2086674 (Why is no real title available?)
• LALBLC A Program Testing the Equivalence of dpda’s
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Proving more observational equivalences with ProVerif
• The equivalence problem for deterministic pushdown automata is decidable
• The inclusion problem for simple languages

Cited in

(8)

• A decidable class of security protocols for both reachability and equivalence properties
• POR for security protocol equivalences. Beyond action-determinism
• SPEC: an equivalence checker for security protocols
• Analysing privacy-type properties in cryptographic protocols (invited talk)
• scientific article; zbMATH DE number 7559487 (Why is no real title available?)
• A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
• From security protocols to pushdown automata
• DeepSec: deciding equivalence properties for security protocols -- improved theory and practice

Describes a project that uses

Uses Software

• LALBLC

This page was built for publication: From security protocols to pushdown automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277904)