Tham gia Đăng nhập
Điểm:1
DaWNFoRCe avatar Crypto

Xác minh chính thức cho tính toán nhiều bên và mã hóa đồng hình?

lá cờ cn
DaWNFoRCe

Gần đây tôi đã tìm thấy một số công việc về việc sử dụng Phần mềm xác minh chính thức, chẳng hạn như ProVerif cho các vùng tách biệt. Tôi tự hỏi liệu có khả thi khi có thứ gì đó tương tự cho MPC và Mã hóa đồng hình và các ứng dụng của chúng không?

Tôi luôn nghĩ rằng có những hạn chế khi áp dụng bằng chứng dựa trên mô phỏng và Khả năng kết hợp phổ quát, nói chung, trong Xác minh chính thức, nhưng gần đây tôi nghĩ rằng phải có những lý do mạnh mẽ hơn.

57
0 + 6
lá cờ cn
lamba
Tôi nghĩ rằng có nhiều khía cạnh cho câu hỏi của bạn. Tôi sẽ chỉ nhận xét về MPC. Các bằng chứng thường được viết trong khuôn khổ UC vì nó cho phép thành phần tùy ý. Theo như tôi biết, các công cụ xác minh chính thức không hỗ trợ điều này.
0
Hồi đáp
DaWNFoRCe avatar
lá cờ cn
DaWNFoRCe
Ok, bây giờ hãy tưởng tượng nếu chúng ta làm việc trong bối cảnh Đánh giá chức năng an toàn, điều đó có giúp mọi việc dễ dàng hơn đối với Xác minh chính thức không?
0
Hồi đáp
Vadym Fedyukovych avatar
lá cờ in
Vadym Fedyukovych
"Cách mô phỏng nó ở Isabelle: Hướng tới bằng chứng chính thức để tính toán an toàn cho nhiều bên", 1805.12482 trên arxiv
0
Hồi đáp
DaWNFoRCe avatar
lá cờ cn
DaWNFoRCe
Xin chào.. vì vậy có một số công việc từ những người như Maurer: "Mô hình hóa trừu tượng của giao tiếp hệ thống trong mật mã cấu trúc sử dụng CryptHOL" nhưng nếu bạn thấy loại địa điểm mà chúng xuất hiện.. Tôi tự hỏi đâu là động lực chính để không chấp nhận xác minh chính thức
0
Hồi đáp
DaWNFoRCe avatar
lá cờ cn
DaWNFoRCe
Nếu các bạn để ý.. những công việc này khá kiên quyết về những gì họ có thể làm... như cải thiện mô phỏng cho các kênh an toàn.. không phải những gì không thể thực hiện được.. vì vậy đó vẫn là câu hỏi của tôi.. điều gì thực sự ngăn cản việc sử dụng Trang trọng Xác minh?
0
Hồi đáp
lá cờ cn
lamba
Tôi đã đính chính, có các công cụ cho phép xác minh chính thức các bằng chứng dựa trên UC https://eprint.iacr.org/2019/582.pdf. Tôi cho rằng về cơ bản không có gì ngăn cản bạn sử dụng xác minh chính thức cho MPC, chỉ là không có đủ người và không đủ thời gian để thực hiện loại công việc này.
0
Hồi đáp
lá cờ VietNam
Phan Văn Trường
Câu hỏi này là trong các ngôn ngữ khác:

Đăng câu trả lời

Hầu hết mọi người không hiểu rằng việc đặt nhiều câu hỏi sẽ mở ra cơ hội học hỏi và cải thiện mối quan hệ giữa các cá nhân. Ví dụ, trong các nghiên cứu của Alison, mặc dù mọi người có thể nhớ chính xác có bao nhiêu câu hỏi đã được đặt ra trong các cuộc trò chuyện của họ, nhưng họ không trực giác nhận ra mối liên hệ giữa câu hỏi và sự yêu thích. Qua bốn nghiên cứu, trong đó những người tham gia tự tham gia vào các cuộc trò chuyện hoặc đọc bản ghi lại các cuộc trò chuyện của người khác, mọi người có xu hướng không nhận ra rằng việc đặt câu hỏi sẽ ảnh hưởng—hoặc đã ảnh hưởng—mức độ thân thiện giữa những người đối thoại.