Automatic verification of cryptographic protocols with SETHEO

DOI10.1007/3-540-63104-6_12MaRDI QIDQ5234693zbMATH OpenOpenAlexFDO

Authors Johann Schumann

Publication date 1 October 2019

Published in Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63104-6_12

zbMATH Keywords

authentication protocolautomatic verificationcryptographic protocolfirst-order predicate logicinference rulemulti-sorted modal logic

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Cryptography (94A60)

Recommendations

• Automated verification of equivalence properties of cryptographic protocols
• Automated verification of equivalence properties of cryptographic protocols
• scientific article; zbMATH DE number 2086169
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1962854
• SeVe: automatic tool for verification of security protocols
• Automated verification of selected equivalences for security protocols
• A General Approach to the Verification of Cryptographic Protocols Using Answer Set Programming

Cites work

• A logic of authentication
• A semantics for a logic of authentication (extended abstract)
• Controlled integration of the cut rule into connection tableau calculi
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 1348483 (Why is no real title available?)
• scientific article; zbMATH DE number 1024091 (Why is no real title available?)
• ILF-SETHEO
• SETHEO: A high-performance theorem prover

Cited in

(10)

• A domain-specific language for cryptographic protocols based on streams
• Combining proverif and automated theorem provers for security protocol verification
• Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
• Using automated theorem provers in verification of protocols
• scientific article; zbMATH DE number 2086169 (Why is no real title available?)
• Automated Verification of Dynamic Root of Trust Protocols
• Type-Based Automated Verification of Authenticity in Cryptographic Protocols
• Automatic verification of temporal-epistemic properties of cryptographic protocols
• ILF-SETHEO
• Deciding cryptographic protocol adequacy with HOL: the implementation

Describes a project that uses

Uses Software

• SETHEO
• ILF-SETHEO
• HOL
• E-SETHEO

This page was built for publication: Automatic verification of cryptographic protocols with SETHEO

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