Puncte:1

Verificare formală pentru calcularea cu mai multe părți și criptarea homomorfă?

drapel cn

Am găsit recent ceva de lucru cu privire la utilizarea software-ului de verificare formală, cum ar fi ProVerif pentru enclave. Mă întreb dacă este fezabil să existe ceva similar pentru MPC și Homomorphic Encryption și aplicațiile lor?

Întotdeauna am crezut că există limitări în adoptarea dovezilor bazate pe simulare și a compunebilității universale, în general, în verificarea formală, dar în ultimul timp mă gândesc că trebuie să existe motive mai puternice.

drapel cn
Cred că sunt multe aspecte la întrebarea ta. Voi comenta doar MPC. Dovezile sunt adesea scrise în cadrul UC, deoarece permite compunerea arbitrară. Din câte știu eu, instrumentele formale de verificare nu acceptă acest lucru.
DaWNFoRCe avatar
drapel cn
Ok, acum imaginați-vă că dacă lucrăm în contextul evaluării funcțiilor securizate, asta ar ușura lucrurile în ceea ce privește verificarea formală?
Vadym Fedyukovych avatar
drapel in
„Cum să o simulați în Isabelle: către o dovadă formală pentru calcularea sigură a mai multor părți”, 1805.12482 pe arxiv
DaWNFoRCe avatar
drapel cn
Bună.. deci există o lucrare de la oameni precum Maurer: „Modelarea abstractă a comunicării sistemului în criptografia constructivă folosind CryptHOL”, dar dacă vedeți ce fel de locații apar.. Mă întreb care sunt principalele motivații pentru a nu accepta verificarea formală
DaWNFoRCe avatar
drapel cn
Dacă observați... aceste lucrări sunt destul de neclintite asupra a ceea ce ar putea face... cum ar fi îmbunătățirea simulării pentru canalele securizate... nu ceea ce nu se poate face... deci aceasta este încă întrebarea mea... ce blochează cu adevărat utilizarea Formal Verificare?
drapel cn
Sunt corectat, există instrumente care permit verificarea formală a dovezilor bazate pe UC https://eprint.iacr.org/2019/582.pdf. Îmi imaginez că nu există nimic care să te împiedice în mod fundamental să folosești verificarea formală pentru MPC, doar că nu există destui oameni și nu este suficient timp pentru a face acest tip de muncă.

Postează un răspuns

Majoritatea oamenilor nu înțeleg că a pune multe întrebări deblochează învățarea și îmbunătățește legătura interpersonală. În studiile lui Alison, de exemplu, deși oamenii își puteau aminti cu exactitate câte întrebări au fost puse în conversațiile lor, ei nu au intuit legătura dintre întrebări și apreciere. În patru studii, în care participanții au fost implicați în conversații ei înșiși sau au citit transcrieri ale conversațiilor altora, oamenii au avut tendința să nu realizeze că întrebarea ar influența – sau ar fi influențat – nivelul de prietenie dintre conversatori.