Automated type-based analysis of injective agreement in the presence of compromised principals

DOI10.1016/j.jlamp.2015.06.002zbMath1337.68193OpenAlexW1157586374WikidataQ114159207 ScholiaQ114159207MaRDI QIDQ492914

Behnam Sattarzadeh, Mehran S. Fallah

Publication date: 21 August 2015

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.06.002

zbMATH Keywords

static analysistype reconstructionauthentication protocolscompromised principalsinjective agreement

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Network protocols (68M12) Authentication, digital signatures and secret sharing (94A62)

Uses Software

• Isabelle
• AVISPA
• CASPA_
• ProVerif
• OFMC
• Cryptyc
• TAMARIN
• F*

Cites Work

• Unnamed Item
• An attack on the Needham-Schroeder public-key authentication protocol
• On the security of SPLICE/AS -- The authentication system in WIDE Internet
• Formal correctness of security protocols.
• A calculus for cryptographic protocols: The spi calculus
• Isabelle. A generic theorem prover
• Verification of cryptographic protocols: tagging enforces termination
• Pattern-matching spi-calculus
• Security Protocol Verification: Symbolic and Computational Models
• Secrecy by typing in security protocols
• Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols
• Type-Based Automated Verification of Authenticity in Cryptographic Protocols
• On the security of public key protocols
• Using encryption for authentication in large networks of computers
• A logic of authentication
• Type Inference for Correspondence Types
• Secure distributed programming with value-dependent types
• Modular verification of security protocol code by typing
• Logical Foundations of Secure Resource Management in Protocol Implementations
• Proving More Observational Equivalences with ProVerif
• Probabilistic relational verification for cryptographic implementations
• Computer Aided Verification
• CONCUR 2005 – Concurrency Theory
• CONCUR 2005 – Concurrency Theory
• A bisimulation for dynamic sealing

This page was built for publication: Automated type-based analysis of injective agreement in the presence of compromised principals