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)

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 ⋮ Cryptographic Verification by Typing for a Sample Protocol Implementation ⋮ Quantifying information leakage in process calculi ⋮ The λ-calculus in the π-calculus ⋮ A calculus for cryptographic protocols: The spi calculus ⋮ Abstract Interpretation for Proving Secrecy Properties in Security Protocols ⋮ Information based reasoning about security protocols ⋮ Cryptographic Analysis in Cubic Time ⋮ Techniques for Security Checking ⋮ Mobile ambients ⋮ Types for access control ⋮ On the Expressive Power of Polyadic Synchronisation in π-calculus ⋮ Modal Logics for Cryptographic Processes ⋮ Processes against tests: on defining contextual equivalences ⋮ Structured coalgebras and minimal HD-automata for the \(\pi\)-calculus ⋮ Analysis of security protocols as open systems ⋮ A new logic for electronic commerce protocols ⋮ A comparison of three authentication properties. ⋮ Static analysis for the \(\pi\)-calculus with applications to security ⋮ Trace and testing equivalence on asynchronous processes ⋮ Type-based information flow analysis for the \(\pi\)-calculus ⋮ Protocol Composition Logic (PCL) ⋮ A Process Algebra for Reasoning About Quantum Security ⋮ A Uniform Framework for Security and Trust Modeling and Analysis with Crypto-CCS ⋮ Models and emerging trends of concurrent constraint programming ⋮ Primitives for authentication in process algebras. ⋮ Dynamic connectors for concurrency ⋮ Process algebras as support for sustainable systems of services

Uses Software

Interrogator

Cites Work

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