About: ProVerif     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : yago:Software106566077, within Data Space : dbpedia.org associated with source document(s)
QRcode icon
http://dbpedia.org/describe/?url=http%3A%2F%2Fdbpedia.org%2Fresource%2FProVerif&graph=http%3A%2F%2Fdbpedia.org&graph=http%3A%2F%2Fdbpedia.org

ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet. Support is provided for cryptographic primitives including: symmetric & asymmetric cryptography; digital signatures; hash functions; bit-commitment; and signature proofs of knowledge. The tool is capable of evaluating reachability properties, correspondence assertions and observational equivalence. These reasoning capabilities are particularly useful to the computer security domain since they permit the analysis of secrecy and authentication properties. Emerging properties such as privacy, traceability and verifiability can also be considered. Protocol analysis is considered with respect to an unbounded number of sessions and an

AttributesValues
rdf:type
rdfs:label
  • ProVerif (ja)
  • ProVerif (en)
rdfs:comment
  • ProVerifは、暗号化プロトコルの安全性要件に関する自動推論を行うソフトウェアツールであり、ブルーノ ブランシェットによって開発された。 対称と非対称暗号、デジタル署名、ハッシュ関数、ビットコミットメント、知識の証明などの暗号化プリミティブがサポートされている。このツールは、到達可能性(reachability)、対応表明(correspondence assertions)、および観測等価性(observational equivalence)を評価することができる。これらの推論機能は、機密性や認証機能の分析を可能にするため、コンピュータセキュリティにおいて特に役立つ。プライバシー、追跡可能性、検証可能性などの新たな性質も解析することができる。プロトコル分析では、無限個のセッションと無限大のメッセージ空間が考慮される。このツールは攻撃の再構築が可能である。つまり、ある特性を持つことが証明できない場合には、その特性を破る実行を得ることができる。 (ja)
  • ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet. Support is provided for cryptographic primitives including: symmetric & asymmetric cryptography; digital signatures; hash functions; bit-commitment; and signature proofs of knowledge. The tool is capable of evaluating reachability properties, correspondence assertions and observational equivalence. These reasoning capabilities are particularly useful to the computer security domain since they permit the analysis of secrecy and authentication properties. Emerging properties such as privacy, traceability and verifiability can also be considered. Protocol analysis is considered with respect to an unbounded number of sessions and an (en)
foaf:name
  • ProVerif (en)
name
  • ProVerif (en)
dcterms:subject
Wikipage page ID
Wikipage revision ID
Link from a Wikipage to another Wikipage
Link from a Wikipage to an external page
sameAs
dbp:wikiPageUsesTemplate
developer
  • Bruno Blanchet (en)
language
  • English (en)
latest release date
latest release version
license
  • Mainly, GNU GPL; Windows binaries, BSD licenses (en)
programming language
released
title
  • ProVerif (en)
has abstract
  • ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet. Support is provided for cryptographic primitives including: symmetric & asymmetric cryptography; digital signatures; hash functions; bit-commitment; and signature proofs of knowledge. The tool is capable of evaluating reachability properties, correspondence assertions and observational equivalence. These reasoning capabilities are particularly useful to the computer security domain since they permit the analysis of secrecy and authentication properties. Emerging properties such as privacy, traceability and verifiability can also be considered. Protocol analysis is considered with respect to an unbounded number of sessions and an unbounded message space. The tool is capable of attack reconstruction: when a property cannot be proved, an execution trace which falsifies the desired property is constructed. (en)
  • ProVerifは、暗号化プロトコルの安全性要件に関する自動推論を行うソフトウェアツールであり、ブルーノ ブランシェットによって開発された。 対称と非対称暗号、デジタル署名、ハッシュ関数、ビットコミットメント、知識の証明などの暗号化プリミティブがサポートされている。このツールは、到達可能性(reachability)、対応表明(correspondence assertions)、および観測等価性(observational equivalence)を評価することができる。これらの推論機能は、機密性や認証機能の分析を可能にするため、コンピュータセキュリティにおいて特に役立つ。プライバシー、追跡可能性、検証可能性などの新たな性質も解析することができる。プロトコル分析では、無限個のセッションと無限大のメッセージ空間が考慮される。このツールは攻撃の再構築が可能である。つまり、ある特性を持つことが証明できない場合には、その特性を破る実行を得ることができる。 (ja)
gold:hypernym
prov:wasDerivedFrom
page length (characters) of wiki page
latest release date
latest release version
  • 2.04
release date
license
programming language
foaf:isPrimaryTopicOf
is Link from a Wikipage to another Wikipage of
is foaf:primaryTopic of
Faceted Search & Find service v1.17_git139 as of Feb 29 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 08.03.3330 as of Mar 19 2024, on Linux (x86_64-generic-linux-glibc212), Single-Server Edition (61 GB total memory, 41 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software