Mobile values, new names, and secure communication
From MaRDI portal
Publication:5178877
DOI10.1145/360204.360213zbMath1323.68398OpenAlexW1973054120MaRDI QIDQ5178877
Publication date: 17 March 2015
Published in: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/360204.360213
Cryptography (94A60) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (only showing first 100 items - show all)
Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity ⋮ Declarative event based models of concurrency and refinement in psi-calculi ⋮ Private authentication ⋮ Algorithmic problems in the symbolic approach to the verification of automatically synthesized cryptosystems ⋮ A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols ⋮ Model Checking Security Protocols ⋮ A closer look at constraints as processes ⋮ A Behavioural Theory for a π-calculus with Preorders ⋮ Moving the bar on computationally sound exclusive-or ⋮ Formalising Observer Theory for Environment-Sensitive Bisimulation ⋮ Alice and Bob: Reconciling Formal Models and Implementation ⋮ Deciding knowledge in security protocols under equational theories ⋮ A framework for security analysis of mobile wireless networks ⋮ Decision procedures for the security of protocols with probabilistic encryption against offline dictionary attacks ⋮ Stateful applied pi calculus: observational equivalence and labelled bisimilarity ⋮ Modular verification of protocol equivalence in the presence of randomness ⋮ POR for security protocol equivalences. Beyond action-determinism ⋮ Efficiently deciding equivalence for standard primitives and phases ⋮ Formal analysis and offline monitoring of electronic exams ⋮ Models for name-passing processes: Interleaving and causal ⋮ Types for Secure Pattern Matching with Local Knowledge in Universal Concurrent Constraint Programming ⋮ A game-theoretic framework for specification and verification of cryptographic protocols ⋮ Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later ⋮ Deciding equivalence-based properties using constraint solving ⋮ A Probabilistic Applied Pi–Calculus ⋮ Deciding Knowledge in Security Protocols for Monoidal Equational Theories ⋮ A behavioural theory for a \(\pi\)-calculus with preorders ⋮ Unnamed Item ⋮ A pure labeled transition semantics for the applied pi calculus ⋮ On the existence and decidability of unique decompositions of processes in the applied \(\pi\)-calculus ⋮ To know or not to know: Epistemic approaches to security protocol verification ⋮ Tree automata with equality constraints modulo equational theories ⋮ Reducing equational theories for the decision of static equivalence ⋮ Decidability of equivalence of symbolic derivations ⋮ Computing knowledge in security protocols under convergent equational theories ⋮ Decidability and combination results for two notions of knowledge in security protocols ⋮ Formally sound implementations of security protocols with JavaSPI ⋮ Computing strong and weak bisimulations for psi-calculi ⋮ Modeling and verifying ad hoc routing protocols ⋮ Deducibility constraints and blind signatures ⋮ A Secure Group-Based AKA Protocol for Machine-Type Communications ⋮ A Spatial Equational Logic for the Applied π-Calculus ⋮ Challenges in the Automated Verification of Security Protocols ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ Parametric synchronizations in mobile nominal calculi ⋮ A Testing Theory for a Higher-Order Cryptographic Language ⋮ Improvement of a chaotic maps-based three-party password-authenticated key exchange protocol without using server's public key and smart card ⋮ Automated Verification of Dynamic Root of Trust Protocols ⋮ On Communication Models When Verifying Equivalence Properties ⋮ A formal semantics for protocol narrations ⋮ Formal methods for web security ⋮ A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols ⋮ Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography ⋮ Intruder deduction problem for locally stable theories with normal forms and inverses ⋮ Automated verification of selected equivalences for security protocols ⋮ Free-algebra models for the \(\pi \)-calculus ⋮ Composition of password-based protocols ⋮ The \(C_\pi\)-calculus: a model for confidential name passing ⋮ A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols ⋮ A complete symbolic bisimulation for full applied pi calculus ⋮ A Complete Symbolic Bisimilarity for an Extended Spi Calculus ⋮ Fair multi-party contract signing using private contract signatures ⋮ Security Abstractions and Intruder Models (Extended Abstract) ⋮ A Calculus for Mobile Ad-hoc Networks with Static Location Binding ⋮ Encoding cryptographic primitives in a calculus with polyadic synchronisation ⋮ Rigid tree automata and applications ⋮ Verification of Correspondence Assertions in a Calculus for Mobile Ad Hoc Networks ⋮ A procedure for deciding symbolic equivalence between sets of constraint systems ⋮ A method for symbolic analysis of security protocols ⋮ A hierarchy of equivalences for asynchronous calculi ⋮ Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures ⋮ Safe abstractions of data encodings in formal security protocol models ⋮ Pattern-matching spi-calculus ⋮ Computing Knowledge in Security Protocols under Convergent Equational Theories ⋮ A spatial equational logic for the applied \(\pi \)-calculus ⋮ A decidable class of security protocols for both reachability and equivalence properties ⋮ PRISMA: A Mobile Calculus with Parametric Synchronization ⋮ Formal Analysis of Dynamic, Distributed File-System Access Controls ⋮ Bisimulation for Demonic Schedulers ⋮ Rigid Tree Automata ⋮ Open Bisimulation for the Concurrent Constraint Pi-Calculus ⋮ Symbolic Bisimulation for the Applied Pi Calculus ⋮ Formal analysis of security protocols for wireless sensor networks ⋮ Automated Verification of Equivalence Properties of Cryptographic Protocols ⋮ Computationally sound implementations of equational theories against passive adversaries ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ YAPA: A Generic Tool for Computing Intruder Knowledge ⋮ On the relationships between notions of simulation-based security ⋮ An Epistemic Predicate CTL* for Finite Control π-Processes ⋮ A Symbolic Framework to Analyse Physical Proximity in Security Protocols ⋮ Deciding knowledge in security protocols under some e-voting theories ⋮ Broadcast Psi-calculi with an Application to Wireless Protocols ⋮ A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract) ⋮ Dynamic management of capabilities in a network aware coordination language ⋮ A Formal Analysis of Complex Type Flaw Attacks on Security Protocols ⋮ Computationally Sound Symbolic Analysis of Probabilistic Protocols with Ideal Setups ⋮ Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif ⋮ Protocol Composition Logic (PCL) ⋮ A Logical Characterisation of Static Equivalence ⋮ A Coq Library for Verification of Concurrent Programs
This page was built for publication: Mobile values, new names, and secure communication
