Combining proverif and automated theorem provers for security protocol verification

DOI10.1007/978-3-030-29436-6_21OpenAlexW2969498914MaRDI QIDQ2305427

Di Long Li, Alwen Tiu

Publication date: 10 March 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-29436-6_21

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

The 10th IJCAR automated theorem proving system competition – CASC-J10

Uses Software

• VAMPIRE
• AVISPA
• SPASS
• TPTP
• ProVerif
• Maude-NPA
• TAMARIN
• AVATAR

Cites Work

• An attack on a recursive authentication protocol. A cautionary tale
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• AVATAR: The Architecture for First-Order Theorem Provers
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Analyzing security protocols with secrecy types and logic programs
• On the security of public key protocols
• Using encryption for authentication in large networks of computers
• Mobile values, new names, and secure communication
• Automated Deduction – CADE-20
• Term Rewriting and Applications

This page was built for publication: Combining proverif and automated theorem provers for security protocol verification