Zobrazeno 1 - 6
of 6
pro vyhledávání: '"Adam Petcher"'
Autor:
Mike Dodds, Brett Boston, Brian Huffman, Andrei Stefanescu, Josiah Dodds, Samuel Breese, Adam Petcher
Publikováno v:
Computer Aided Verification ISBN: 9783030816841
CAV (1)
CAV (1)
We have completed machine-assisted proofs of two highly-optimized cryptographic primitives, AES-256-GCM and SHA-384. We have verified that the implementations of these primitives, written in a mix of C and x86 assembly, are memory safe and functional
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d80c573a2ad4a37d32eed49d97d55950
https://doi.org/10.1007/978-3-030-81685-8_31
https://doi.org/10.1007/978-3-030-81685-8_31
Autor:
Matthew Green, Naphat Sanguansin, Katherine Ye, Lennart Beringer, Adam Petcher, Andrew W. Appel
We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic security--that its output is pseudorandom--using a hybrid game-based proof. We have also proved that the mbedTLS implementation (C progr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::41ce98e9a8e4356bdef04a8298191fd6
http://arxiv.org/abs/1708.08542
http://arxiv.org/abs/1708.08542
Autor:
Adam Petcher, Greg Morrisett
Publikováno v:
CSF
We present a mechanized proof of security for an efficient Searchable Symmetric Encryption (SSE) scheme completed in the Foundational Cryptography Framework (FCF). FCF is a Coq library for reasoning about cryptographic schemes in the computational mo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a1e9a2daf238eda1923e74282cbf0deb
https://doi.org/10.1109/csf.2015.36
https://doi.org/10.1109/csf.2015.36
Autor:
Adam Petcher, Greg Morrisett
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783662466650
POST
POST
We present the Foundational Cryptography Framework FCF for developing and checking complete proofs of security for cryptographic schemes within a proof assistant. This is a general-purpose framework that is capable of modeling and reasoning about a w
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::61619e0e1619031c8703114d92bdd694
https://doi.org/10.1007/978-3-662-46666-7_4
https://doi.org/10.1007/978-3-662-46666-7_4
Publikováno v:
MILCOM
This paper presents a usable graphical interface for specifying and automatically enacting access control rules for applications that involve dissemination of data among mobile tactical devices. A specific motivating example is unmanned aerial vehicl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4b321ca2922ffa6121e8169a44f15a6d
https://doi.org/10.1109/milcom.2011.6127515
https://doi.org/10.1109/milcom.2011.6127515
Publikováno v:
PLPV
Operational Type Theory (OpTT) is a type theory allowing possibly diverging programs while retaining decidability of type checking and a consistent logic. This is done by distinguishing proofs and (program) terms, as well as formulas and types. The t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5e0cbfd9dd991957b7eb561a5450e679
https://doi.org/10.1145/1481848.1481856
https://doi.org/10.1145/1481848.1481856