A calculus for cryptographic protocols: The spi calculus

DOI10.1006/inco.1998.2740zbMath0924.68073OpenAlexW1562901937MaRDI QIDQ1283776

Publication date: 30 March 1999

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1998.2740

zbMATH Keywords

cryptographic protocols pi calculus spi calculus

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25)

Related Items (only showing first 100 items - show all)

Trace Equivalence and Epistemic Logic to Express Security Properties ⋮ Types for Secure Pattern Matching with Local Knowledge in Universal Concurrent Constraint Programming ⋮ Unnamed Item ⋮ Adversarial logic ⋮ On-the-fly bisimilarity checking for fresh-register automata ⋮ Unnamed Item ⋮ Psi-calculi in Isabelle ⋮ Unnamed Item ⋮ A bisimulation for dynamic sealing ⋮ Typing Correspondence Assertions for Communication Protocols ⋮ A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols ⋮ Towards Secrecy for Rewriting in Weakly Adhesive Categories ⋮ Counting the Cost in the Picalculus (Extended Abstract) ⋮ A Complete Symbolic Bisimilarity for an Extended Spi Calculus ⋮ Type Inference for Correspondence Types ⋮ Security Abstractions and Intruder Models (Extended Abstract) ⋮ Encryption as an abstract data-type ⋮ Verification of Correspondence Assertions in a Calculus for Mobile Ad Hoc Networks ⋮ From rewrite rules to bisimulation congruences ⋮ Formal Analysis of Dynamic, Distributed File-System Access Controls ⋮ Bisimulation for Demonic Schedulers ⋮ Automated Verification of Equivalence Properties of Cryptographic Protocols ⋮ A Formal Analysis of Complex Type Flaw Attacks on Security Protocols ⋮ A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol ⋮ A Logical Characterisation of Static Equivalence ⋮ Bisimulation and Co-induction: Some Problems ⋮ Symmetric Authentication within a Simulatable Cryptographic Library ⋮ Secrecy types for asymmetric communication. ⋮ Declarative event based models of concurrency and refinement in psi-calculi ⋮ Private authentication ⋮ A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols ⋮ Probabilistic and nondeterministic aspects of anonymity ⋮ SPEC: An Equivalence Checker for Security Protocols ⋮ Formalising Observer Theory for Environment-Sensitive Bisimulation ⋮ Static Evidences for Attack Reconstruction ⋮ Update semantics of security protocols ⋮ Types and full abstraction for polyadic \(\pi\)-calculus ⋮ Deciding knowledge in security protocols under equational theories ⋮ On the semantics of Alice \& Bob specifications of security protocols ⋮ Injective synchronisation: An extension of the authentication hierarchy ⋮ A framework for security analysis of mobile wireless networks ⋮ Verifying the SET purchase protocols ⋮ Models for name-passing processes: Interleaving and causal ⋮ Intruder deduction for the equational theory of abelian groups with distributive encryption ⋮ Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types ⋮ A game-theoretic framework for specification and verification of cryptographic protocols ⋮ A Probabilistic Applied Pi–Calculus ⋮ Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap ⋮ Trace-based verification of imperative programs with I/O ⋮ A pure labeled transition semantics for the applied pi calculus ⋮ Typing correspondence assertions for communication protocols ⋮ Ugo Montanari and Software Verification ⋮ Implementing Spi Calculus Using Nominal Techniques ⋮ Universally composable symbolic security analysis ⋮ Compositional refinement in agent-based security protocols ⋮ \textsf{CaPiTo}: Protocol stacks for services ⋮ Computing strong and weak bisimulations for psi-calculi ⋮ Unnamed Item ⋮ Efficient representation of the attacker's knowledge in cryptographic protocols analysis ⋮ Employing Costs in Multiagent Systems with Timed Migration and Timed Communication ⋮ A constraint-based language for multiparty interactions ⋮ Channel abstractions for network security ⋮ A Testing Theory for a Higher-Order Cryptographic Language ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ On Communication Models When Verifying Equivalence Properties ⋮ A formal semantics for protocol narrations ⋮ A framework for analyzing probabilistic protocols and its application to the partial secrets exchange ⋮ Modeling ontology evolution with SetPi ⋮ The reactive simulatability (RSIM) framework for asynchronous systems ⋮ Open bisimulation, revisited ⋮ A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols ⋮ Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography ⋮ Modeling ontology evolution via pi-calculus ⋮ Automated verification of selected equivalences for security protocols ⋮ Behavioural equivalences for dynamic web data ⋮ A game semantics of names and pointers ⋮ The \(C_\pi\)-calculus: a model for confidential name passing ⋮ Unnamed Item ⋮ Cryptographic logical relations ⋮ A framework for compositional verification of security protocols ⋮ Unifying simulatability definitions in cryptographic systems under different timing assumptions ⋮ Contract signing, optimism, and advantage ⋮ Multi-attacker protocol validation ⋮ Secrecy and group creation ⋮ Logics for reasoning about cryptographic constructions ⋮ Coalgebraic minimization of HD-automata for the \(\pi\)-calculus using polymorphic types ⋮ Tree automata with one memory set constraints and cryptographic protocols ⋮ Static analysis of topology-dependent broadcast networks ⋮ Weakening the perfect encryption assumption in Dolev-Yao adversaries ⋮ Invariant-based reasoning about parameterized security protocols ⋮ Making random choices invisible to the scheduler ⋮ Multiset rewriting for the verification of depth-bounded processes with name binding ⋮ A framework for specifying and verifying the behaviour of open systems ⋮ Pattern-matching spi-calculus ⋮ Compositional reasoning for shared-variable concurrent programs ⋮ A process calculus BigrTiMo of mobile systems and its formal semantics ⋮ A decidable class of security protocols for both reachability and equivalence properties ⋮ Relating state-based and process-based concurrency through linear logic (full-version) ⋮ A domain-specific language for cryptographic protocols based on streams ⋮ On the relationships between notions of simulation-based security

Uses Software

Interrogator

Cites Work

This page was built for publication: A calculus for cryptographic protocols: The spi calculus