Рейтинг:1

Формальная проверка многопартийных вычислений и гомоморфного шифрования?

флаг cn

Недавно я нашел некоторые работы по использованию программного обеспечения для формальной проверки, такого как ProVerif для анклавов. Интересно, возможно ли иметь что-то подобное для MPC и Homomorphic Encryption и их приложений?

Я всегда думал, что существуют ограничения, связанные с использованием доказательств на основе моделирования и универсальной компонуемости в формальной проверке, но в последнее время я думаю, что должны быть более веские причины.

флаг cn
Я думаю, что есть много аспектов вашего вопроса. Я буду комментировать только MPC. Доказательства часто пишутся в рамках UC, потому что это допускает произвольную композицию. Насколько мне известно, формальные инструменты проверки этого не поддерживают.
DaWNFoRCe avatar
флаг cn
Хорошо, а теперь представьте, если мы будем работать в контексте оценки функций безопасности, упростит ли это формальную проверку?
Vadym Fedyukovych avatar
флаг in
«Как смоделировать это в Isabelle: к формальному доказательству для безопасных многосторонних вычислений», 1805.12482 на arxiv
DaWNFoRCe avatar
флаг cn
Привет... итак, есть работа таких людей, как Маурер: "Абстрактное моделирование системной связи в конструктивной криптографии с использованием CryptHOL", но если вы видите, в каких местах они появляются... Интересно, каковы основные мотивы отказа от формальной проверки?
DaWNFoRCe avatar
флаг cn
Если вы, ребята, заметили... эти работы совершенно непреклонны в том, что они могут сделать... например, улучшить симуляцию для защищенных каналов... а не то, что нельзя сделать... так что это все еще мой вопрос... что на самом деле блокирует использование формальных Проверка?
флаг cn
Я исправлен, есть инструменты, которые позволяют формально проверять доказательства на основе UC https://eprint.iacr.org/2019/582.pdf. Я полагаю, что ничто принципиально не мешает вам использовать формальную проверку для MPC, просто не хватает людей и времени для такой работы.

Ответить или комментировать

Большинство людей не понимают, что склонность к познанию нового открывает путь к обучению и улучшает межличностные связи. В исследованиях Элисон, например, хотя люди могли точно вспомнить, сколько вопросов было задано в их разговорах, они не чувствовали интуитивно связи между вопросами и симпатиями. В четырех исследованиях, в которых участники сами участвовали в разговорах или читали стенограммы чужих разговоров, люди, как правило, не осознавали, что задаваемый вопрос повлияет — или повлиял — на уровень дружбы между собеседниками.