Analyzing security protocols with secrecy types and logic programs

DOI10.1145/1044731.1044735zbMath1204.68030OpenAlexW2073385346MaRDI QIDQ3546279

Bruno Blanchet, Martín Abadi

Publication date: 21 December 2008

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1044731.1044735

Mathematics Subject Classification ID

Cryptography (94A60) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)

Related Items

Formal analysis and offline monitoring of electronic exams ⋮ Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types ⋮ Computing strong and weak bisimulations for psi-calculi ⋮ Unnamed Item ⋮ Formal Analysis of a TTP-Free Blacklistable Anonymous Credentials System ⋮ Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography ⋮ Kripke semantics for higher-order type theory applied to constraint logic programming languages ⋮ Automated verification of selected equivalences for security protocols ⋮ On the relationships between models in protocol verification ⋮ Breaking and fixing public-key Kerberos ⋮ Contracts for security adaptation ⋮ Safe abstractions of data encodings in formal security protocol models ⋮ Formal Analysis of Dynamic, Distributed File-System Access Controls ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ Cryptographic Verification by Typing for a Sample Protocol Implementation ⋮ Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif