Machine-checked security proofs of cryptographic signature schemes

DOI10.1007/11555827_9MaRDI QIDQ5862663zbMATH OpenOpenAlexFDO

Authors Sabrina Tarento

Publication date 9 March 2022

Published in Computer Security – ESORICS 2005 (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.97.8259

zbMATH Keywords

blind signaturecryptographic protocolhash functionproof assistantvalid signature

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Cryptography (94A60) Authentication, digital signatures and secret sharing (94A62)

Recommendations

• Types for Proofs and Programs
• Automated Reasoning
• Security proofs for signature schemes
• Automated Security Proofs with Sequences of Games
• Formal certification of code-based cryptographic proofs

Cites work

• A probabilistic polynomial-time calculus for analysis of cryptographic protocols (preliminary report)
• Automated Reasoning
• Complexity of a determinate algorithm for the discrete logarithm
• Generic groups, collision resistance, and ECDSA
• How To Prove Yourself: Practical Solutions to Identification and Signature Problems
• scientific article; zbMATH DE number 1583771 (Why is no real title available?)
• scientific article; zbMATH DE number 1739881 (Why is no real title available?)
• scientific article; zbMATH DE number 2009973 (Why is no real title available?)
• scientific article; zbMATH DE number 2080670 (Why is no real title available?)
• scientific article; zbMATH DE number 1487486 (Why is no real title available?)
• scientific article; zbMATH DE number 1759457 (Why is no real title available?)
• Logics for reasoning about cryptographic constructions
• New directions in cryptography
• Proof-assistants using dependent type systems
• Symmetric authentication within a simulatable cryptographic library
• The Exact Security of ECIES in the Generic Group Model

Cited in

(3)

• Automated Reasoning
• Types for Proofs and Programs
• Verifying a signature architecture: a comparative case study

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Machine-checked security proofs of cryptographic signature schemes

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