Security protocols: from linear to classical logic by abstract interpretation

DOI10.1016/J.IPL.2005.05.011MaRDI QIDQ1041815zbMATH OpenOpenAlexFDO

Authors Bruno Blanchet

Publication date 4 December 2009

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2005.05.011

zbMATH Keywords

abstract interpretationformal methodslinear logicclassical logiccryptographic protocols

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Grammars and rewriting systems (68Q42)

Recommendations

• Encryption as an abstract data-type (extended abstract)
• scientific article; zbMATH DE number 1962760
• Analyzing security protocols with secrecy types and logic programs
• Analyzing security protocols with secrecy types and logic programs
• Abstract interpretation for proving secrecy properties in security protocols

Cites work

• scientific article; zbMATH DE number 1341618 (Why is no real title available?)
• scientific article; zbMATH DE number 1962758 (Why is no real title available?)
• scientific article; zbMATH DE number 786485 (Why is no real title available?)
• Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs

Cited in

(9)

• Automated verification of selected equivalences for security protocols
• An equation-based classical logic
• Linearity, persistence and testing semantics in the asynchronous pi-calculus
• Abstract State Machines 2004. Advances in Theory and Practice
• Automatic verification of security protocols in the symbolic model: the verifier ProVerif
• Encryption as an abstract data-type (extended abstract)
• scientific article; zbMATH DE number 7806140 (Why is no real title available?)
• scientific article; zbMATH DE number 1962760 (Why is no real title available?)
• On the relationships between models in protocol verification

This page was built for publication: Security protocols: from linear to classical logic by abstract interpretation

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