Finite Models in FOL-Based Crypto-Protocol Verification

DOI10.1007/978-3-642-03459-6_11MaRDI QIDQ3184717zbMATH OpenOpenAlexFDO

Authors Jan Jürjens, Tjark Weber

Publication date 22 October 2009

Published in Foundations and Applications of Security Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03459-6_11

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Model theory of finite structures (03C13) Specification and verification (program logics, model checking, etc.) (68Q60) Cryptography (94A60)

Recommendations

• Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses
• Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
• scientific article; zbMATH DE number 1759624
• Equal to the task?
• scientific article; zbMATH DE number 1962854

Cited in

(4)

• Proving semantic properties as first-order satisfiability
• Finite reasons for safety. Parameterized verification by finite model finding
• Finite State Machine Modelling of Cryptographic Systems in Loops
• scientific article; zbMATH DE number 5051652 (Why is no real title available?)

Describes a project that uses

Uses Software

• TPTP

This page was built for publication: Finite Models in FOL-Based Crypto-Protocol Verification

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