Protocol-Design
我應該如何解釋 Dolev Yao 閉包的這個定義？
請看下圖，它代表了 Dolev Yao 閉包的代數定義。通過閱讀，這似乎是 BAN 邏輯，並且這些行的意思是*“如果你相信上面的陳述是真實的，那麼你必須相信下面的陳述也是真實的。”*
這是準確的嗎？為什麼這些陳述按照它們的順序出現？
語句的順序並不重要。它可能有助於精神上的翻譯 $ \mathcal{DY}(M) $ 作為“您應該相信對手可以從一組初始已知數據開始輕鬆計算的資訊 $ M $ ”。然後，這些規則應該在直覺上是真實的。
公理（第一）規則可以被認為是“對手可以簡單地計算初始數據集”。
代數（第二）規則可以被認為是“對手可以簡單地計算一個由他們知道的值組成的代數表達式”。
組合（第三）規則可以被認為是“對手可以計算他們知道的一組值的邏輯模型內的任何函式”。
投影（第四）規則可以被認為是“如果對手知道一對數據值，那麼他們就可以計算各個數據值”。
對稱解密（第五）規則可以被認為是“如果對手知道一個對稱加密的密文和用於加密它的密鑰，那麼他們就可以計算出相應的明文”。
非對稱解密（第六條）規則可以被認為是“如果對手知道一個公鑰加密的密文和對應的私鑰，那麼他們就可以計算出對應的明文”。
開放簽名（第七條）規則可以被認為是“如果對手知道一條消息摘要的簽名，那麼他們就可以計算消息摘要”。
初始數據集的 Dolaev-Yao 閉包 $ M $ 然後應該將其視為對手可以根據這些規則輕鬆計算的數據集。