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

formal methodsprocess calculireasoning about securitysemantics

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)

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

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)