Verifying a signature architecture: a comparative case study

DOI10.1007/S00165-006-0012-5MaRDI QIDQ877156zbMATH OpenOpenAlexFDO

Authors Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff, David Basin

Publication date 19 April 2007

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL http://doc.rero.ch/record/316084/files/165_2006_Article_12.pdf

zbMATH Keywords

Model checkingSecurityFormal methodsTheorem provingComparisonCase study

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• FM 2005: Formal Methods
• Verifiable composition of signature and encryption. A comprehensive study of the design paradigms
• scientific article; zbMATH DE number 815059
• Verifiably encrypted signatures: security revisited and a new construction
• Machine-checked security proofs of cryptographic signature schemes
• Conditionally Verifiable Signature
• Security of Verifiably Encrypted Signatures and a Construction without Random Oracles
• Progressive and efficient verification for digital signatures
• scientific article; zbMATH DE number 1149903
• Generic constructions for verifiable signcryption

Cites work

• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 65529 (Why is no real title available?)
• scientific article; zbMATH DE number 977452 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 1798183 (Why is no real title available?)
• A really temporal logic
• Automata-theoretic techniques for modal logics of programs
• Automated Deduction – CADE-20
• Combining WS1S and HOL
• Combining partial-order reductions with on-the-fly model-checking.
• Complete integer decision procedures as derived rules in HOL
• Completing the temporal picture
• Experimental evaluation of verification and validation tools on Martian Rover software
• FM 2005: Formal Methods
• Isabelle/HOL. A proof assistant for higher-order logic
• The B-Book

Cited in

(5)

• Proving fairness and implementation correctness of a microkernel scheduler
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
• FM 2005: Formal Methods
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier

Describes a project that uses

Uses Software

• HOL-Z
• SPIN
• PVS
• Nuprl
• NQTHM
• OFMC
• Z
• LTL2BA
• ICS

This page was built for publication: Verifying a signature architecture: a comparative case study

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