Verifying a signature architecture: a comparative case study

DOI10.1007/S00165-006-0012-5zbMATH Open1111.68075OpenAlexW1989012792MaRDI QIDQ877156FDOQ877156

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

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

zbMATH Keywords

Model checkingSecurityFormal methodsTheorem provingComparisonCase study

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

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

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)