Proof techniques for cryptographic processes

DOI10.1137/S0097539700377864MaRDI QIDQ2784489zbMATH OpenOpenAlexWikidataFDO

Authors Rocco De Nicola, Michele Boreale, Rosario Pugliese

Publication date 23 April 2002

Published in SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1137/s0097539700377864

zbMATH Keywords

semanticsformal methodsprocess calculireasoning about security

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 1405638
• scientific article; zbMATH DE number 1982609
• Computer-aided cryptographic proofs
• Logic for verifying public-key cryptographic protocols
• Mathematical Foundations of Computer Science 2003
• The practice of cryptographic protocol verification
• Computer-Aided Security Proofs for the Working Cryptographer
• Proof-based design of security protocols

Cited in

(23)

• Deciding equivalence-based properties using constraint solving
• Decidability of equivalence of symbolic derivations
• A Testing Theory for a Higher-Order Cryptographic Language
• Encoding cryptographic primitives in a calculus with polyadic synchronisation
• Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity
• A logical characterisation of static equivalence
• An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0
• When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
• On the symbolic reduction of processes with cryptographic functions.
• Implementing Spi Calculus Using Nominal Techniques
• Modal logics for nominal transition systems
• Context-sensitive equivalences for non-interference based protocol analysis.
• Modal logics for cryptographic processes
• Cryptographic logical relations
• Bisimulations in the join-calculus
• Automated verification of selected equivalences for security protocols
• A bisimulation for dynamic sealing
• Reasoning about cryptographic protocols in the spi calculus
• EXPLOITING SYMMETRIES FOR TESTING EQUIVALENCE VERIFICATION IN THE SPI CALCULUS
• Formalising Observer Theory for Environment-Sensitive Bisimulation
• Efficient representation of the attacker's knowledge in cryptographic protocols analysis
• Analysis of security protocols as open systems
• A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols

This page was built for publication: Proof techniques for cryptographic processes

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