Zobrazeno 1 - 10
of 33
pro vyhledávání: '"Andreas Lochbihler"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 18, Issue 1 (2022)
The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatypes can be built modularly from bounded natural functors (BNFs), a clas
Externí odkaz:
https://doaj.org/article/73f942a82f9b4b85abfb1c2f89cd28ef
Autor:
Andreas Lochbihler
Publikováno v:
Journal of Automated Reasoning. 66:585-610
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::33dfbdb7d18110500375c6149ea80b99
https://doi.org/10.1007/s10817-022-09616-4
https://doi.org/10.1007/s10817-022-09616-4
Publikováno v:
Journal of Automated Reasoning. 65:521-567
Machine-checked proofs of security are important to increase the rigour of provable security. In this work we present a formalised theory of two fundamental two party cryptographic primitives: $$\varSigma $$ Σ -protocols and Commitment Schemes. $$\v
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ea05e7b07277f66ebfc4be6327ff258c
https://doi.org/10.1007/s10817-020-09581-w
https://doi.org/10.1007/s10817-020-09581-w
Publikováno v:
Journal of Cryptology, 33 (2)
Game-based proofs are a well-established paradigm for structuring security arguments and simplifying their understanding. We present a novel framework, CryptHOL, for rigorous game-based proofs that is supported by mechanical theorem proving. CryptHOL
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::88f69174e438c98d69f4d71c5a4ce505
https://doi.org/10.1007/s00145-019-09341-z
https://doi.org/10.1007/s00145-019-09341-z
Publikováno v:
CSF
Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streaml
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b76b68352affeb97dbf5dc08995b26a0
https://doi.org/10.1109/csf51468.2021.00047
https://doi.org/10.1109/csf51468.2021.00047
Autor:
Peter Lammich, Andreas Lochbihler
Publikováno v:
Journal of Automated Reasoning, 63 (1)
We consider the problem of formally verifying an algorithm in a proof assistant and generating efficient code. Reasoning about correctness is best done at an abstract level, but efficiency of the generated code often requires complicated data structu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6e9b2286cfd129e79f7219de95316f4e
https://doi.org/10.1007/s10817-018-9461-9
https://doi.org/10.1007/s10817-018-9461-9
Autor:
Andreas Lochbihler
Publikováno v:
Journal of Automated Reasoning. 61:243-332
This article presents JinjaThreads, a unified, type-safe model of multithreaded Java source code and bytecode formalised in the proof assistant Isabelle/HOL. The semantics strictly separates sequential aspects from multithreading features like locks,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8a7894bafc17d16f34849005c48db6a7
https://doi.org/10.1007/s10817-018-9452-x
https://doi.org/10.1007/s10817-018-9452-x
Publikováno v:
CSF
Computer-aided cryptography increases the rigour of cryptographic proofs by mechanizing their verification. Existing tools focus mainly on game-based proofs, and efforts to formalize composable frameworks such as Universal Composability have met with
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::70a7d0fc3fc98a3098e3a3ceff6c668e
https://doi.org/10.1109/csf.2019.00018
https://doi.org/10.1109/csf.2019.00018
Autor:
Andreas Lochbihler
Publikováno v:
Journal of Automated Reasoning, 63 (2)
The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. I show that if a monad is restricted to values of a fixed type, this notion can be formalised in HOL. Based on this idea, I develop a library o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3387f4b86ed184e31a1bc94d90196a74
https://hdl.handle.net/20.500.11850/293987
https://hdl.handle.net/20.500.11850/293987
Publikováno v:
Proceedings on Privacy Enhancing Technologies, Vol 2019, Iss 2, Pp 26-46 (2019)
Proceedings on Privacy Enhancing Technologies, 2019 (2)
Proceedings on Privacy Enhancing Technologies, 2019 (2)
Cardinality estimators like HyperLogLog are sketching algorithms that estimate the number of distinct elements in a large multiset. Their use in privacy-sensitive contexts raises the question of whether they leak private information. In particular, c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c2821442a52872f3ca536aec9f4e58b1