On the security of public key protocols
From MaRDI portal
Publication:3968876
DOI10.1109/TIT.1983.1056650zbMath0502.94005OpenAlexW2029693536MaRDI QIDQ3968876
Andrew Chi-Chih Yao, Danny Dolev
Publication date: 1983
Published in: IEEE Transactions on Information Theory (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1109/tit.1983.1056650
Cryptography (94A60) Data encryption (aspects in computer science) (68P25) Network protocols (68M12)
Related Items (only showing first 100 items - show all)
Protocol insecurity with a finite number of sessions and composed keys is NP-complete. ⋮ Three systems for cryptographic protocol analysis ⋮ On the verifiability of two-party algebraic protocols ⋮ Provable security analysis of FIDO2 ⋮ A novel ECC-based provably secure and privacy-preserving multi-factor authentication protocol for cloud computing ⋮ Analysis of security protocols based on challenge-response ⋮ Cryptanalysis and design of a three-party authenticated key exchange protocol using smart card ⋮ Moving the bar on computationally sound exclusive-or ⋮ On the design of cryptographic primitives ⋮ Attestation waves: platform trust via remote power analysis ⋮ On the security of p-party protocols ⋮ Update semantics of security protocols ⋮ A tutorial-style introduction to \(\mathsf{DY}^{\star}\) ⋮ Security protocols as choreographies ⋮ Secure key management policies in strand spaces ⋮ On the complexity of verification of time-sensitive distributed systems ⋮ Probabilistic annotations for protocol models. Dedicated to Joshua Guttman ⋮ An undecidability result for AGh ⋮ Complete symbolic reachability analysis using back-and-forth narrowing ⋮ Deciding knowledge in security protocols under equational theories ⋮ Formal analysis of Kerberos 5 ⋮ On the semantics of Alice \& Bob specifications of security protocols ⋮ A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties ⋮ A (restricted) quantifier elimination for security protocols ⋮ Decidability issues for extended ping-pong protocols ⋮ Attacking group protocols by refuting incorrect inductive conjectures ⋮ Decision procedures for the security of protocols with probabilistic encryption against offline dictionary attacks ⋮ A formal language for cryptographic protocol requirements ⋮ Modular verification of protocol equivalence in the presence of randomness ⋮ Automated identification of desynchronisation attacks on shared secrets ⋮ Formal analysis and offline monitoring of electronic exams ⋮ Intruder deduction for the equational theory of abelian groups with distributive encryption ⋮ A collusion problem and its solution ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ A game-theoretic framework for specification and verification of cryptographic protocols ⋮ Privacy and verifiability in voting systems: methods, developments and trends ⋮ How to simulate it in Isabelle: towards formal proof for secure multi-party computation ⋮ To know or not to know: Epistemic approaches to security protocol verification ⋮ Authenticated confidential channel establishment and the security of TLS-DHE ⋮ Universally composable symbolic security analysis ⋮ Timed models of security protocols including delays in the network ⋮ Using probabilistic automata for security protocols verification ⋮ Reducing equational theories for the decision of static equivalence ⋮ Formally sound implementations of security protocols with JavaSPI ⋮ State space reduction in the Maude-NRL protocol analyzer ⋮ Bounded memory Dolev-Yao adversaries in collaborative systems ⋮ Lattice-based completely non-malleable public-key encryption in the standard model ⋮ An inductive approach to strand spaces ⋮ Protocol insecurity with a finite number of sessions and a cost-sensitive guessing intruder is NP-complete ⋮ Efficient representation of the attacker's knowledge in cryptographic protocols analysis ⋮ Improvement of a chaotic maps-based three-party password-authenticated key exchange protocol without using server's public key and smart card ⋮ A Markov adversary model to detect vulnerable iOS devices and vulnerabilities in iOS apps ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ A formal semantics for protocol narrations ⋮ The reactive simulatability (RSIM) framework for asynchronous systems ⋮ Transducer-based analysis of cryptographic protocols ⋮ A novel quantum dragonfly multi-key exchange protocol beyond conventional attacks ⋮ Intruder deducibility constraints with negation. Decidability and application to secured service compositions ⋮ Design and analysis of a three party password-based authenticated key exchange protocol using extended chaotic maps ⋮ Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography ⋮ Intruder deduction problem for locally stable theories with normal forms and inverses ⋮ A Maude environment for CafeOBJ ⋮ Collaborative planning with confidentiality ⋮ Secrecy and group creation ⋮ Dealing with logical omniscience: expressiveness and pragmatics ⋮ Distributed temporal logic for the analysis of security protocol models ⋮ Cancellation rules and extended word problems ⋮ Reachability results for timed automata with unbounded data structures ⋮ The RSA group is pseudo-free ⋮ An NP decision procedure for protocol insecurity with XOR ⋮ Simulation relations for alternating Büchi automata ⋮ A method for symbolic analysis of security protocols ⋮ A computational interpretation of Dolev-Yao adversaries ⋮ Abstract interpretation of mobile systems ⋮ Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures ⋮ Invariant-based reasoning about parameterized security protocols ⋮ Safe abstractions of data encodings in formal security protocol models ⋮ Abstractions of non-interference security: probabilistic versus possibilistic ⋮ On the complexity of some extended word problems defined by cancellation rules ⋮ On a new formal proof model for RFID location privacy ⋮ PRUB: A privacy protection friend recommendation system based on user behavior ⋮ Ping-pong protocols as prefix grammars: modelling and verification via program transformation ⋮ Computationally sound implementations of equational theories against passive adversaries ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ Analyzing security protocols using time-bounded task-PIOAs ⋮ Reachability is decidable for weakly extended process rewrite systems ⋮ Easy intruder deduction problems with homomorphisms ⋮ Ephemeral-secret-leakage secure ID-based three-party authenticated key agreement protocol for mobile distributed computing environments ⋮ Bounded memory protocols ⋮ A formal framework for security testing of automotive over-the-air update systems ⋮ Analysis of security protocols as open systems ⋮ On the symbolic reduction of processes with cryptographic functions. ⋮ A new logic for electronic commerce protocols ⋮ Models and emerging trends of concurrent constraint programming ⋮ Authentication tests and the structure of bundles. ⋮ Validating firewalls using flow logics ⋮ Finite-state analysis of two contract signing protocols ⋮ Comment on the ``Quantum public-key cryptosystem ⋮ On the security of name-stamp protocols ⋮ Formalizing provable anonymity in Isabelle/HOL
This page was built for publication: On the security of public key protocols
