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

DOI10.1016/J.JLAMP.2015.06.002zbMATH Open1337.68193OpenAlexW1157586374WikidataQ114159207 ScholiaQ114159207MaRDI QIDQ492914FDOQ492914

Authors: 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

Recommendations

• scientific article; zbMATH DE number 1832233
• scientific article; zbMATH DE number 1104389
• Type-Based Automated Verification of Authenticity in Cryptographic Protocols
• Programming Languages and Systems
• Foundations of Security Analysis and Design III

zbMATH Keywords

type reconstructionstatic analysisauthentication protocolscompromised principalsinjective agreement

Mathematics Subject Classification ID

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

Cites Work

• Computer Aided Verification
• Secure distributed programming with value-dependent types
• Isabelle. A generic theorem prover
• A calculus for cryptographic protocols: The spi calculus
• On the security of SPLICE/AS -- The authentication system in WIDE Internet
• Using encryption for authentication in large networks of computers
• Types and programing languages
• A logic of authentication
• Proving more observational equivalences with ProVerif
• On the security of public key protocols
• An attack on the Needham-Schroeder public-key authentication protocol
• A bisimulation for dynamic sealing
• 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
• Type Inference for Correspondence Types
• Modular verification of security protocol code by typing
• Logical foundations of secure resource management in protocol implementations
• Probabilistic relational verification for cryptographic implementations
• CONCUR 2005 – Concurrency Theory
• CONCUR 2005 – Concurrency Theory
• Formal correctness of security protocols.

Cited In (4)

• Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types
• Title not available (Why is that?)
• Injective synchronisation: An extension of the authentication hierarchy
• A syntactic criterion for injectivity of authentication protocols

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q492914)