我們可以對協議驗證者給予多少信任？
我閱讀了許多關於認證密鑰交換協議的論文，大多數安全證明都是由作者完成的。在這種方法中，您可以想像效率低下。而且，即使你已經證明了 AKE 協議在某種模型下的安全性（比如eCK），你仍然無法保證在所有其他模型下的安全性，包括現實生活。
這讓我問：可以使用一些自動化工具來驗證協議，例如Tamarin嗎？畢竟這將非常有效。我最初的擔心是這是否會被人們接受並像傳統方式一樣令人信服？
我們知道，傳統的數學證明可能包含錯誤，而且這些錯誤可能多年未被發現。有時，即使證明不正確，該方案也是安全的，例如RSA-OAEP。有時，該方案存在輕微缺陷，由於證明中的錯誤而未被發現的缺陷，例如HMQV。有時一個計劃根本不安全。
我們知道形式系統可能無法描述現實世界並因此證明不正確的結果，例如BAN 邏輯，但現在形式系統似乎更加完整。
形式系統通常使用理想化的密碼學。有時可以證明某種理想化是合理的，但總的來說這很困難。這意味著原則上，可以設計在正式系統中安全的方案，但無論使用什麼密碼術來實例化正式對像都是不安全的。隨機預言機模型和通用組模型存在類似的結果，但隨機預言機模型仍然被認為是現實世界中安全性的良好啟發式（通用組模型較少）。
許多系統將注意力限制在各種形式的加密和數字簽名上。這在某種意義上是好的，因為理想化很可能是合理的。另一方面，您通常甚至無法在正式系統中表達 Diffie-Hellman，這意味著它的用處不大。在可以表達 Diffie-Hellman 的地方，群模型通常非常有限，這意味著形式系統可能無法表達涉及群微妙屬性的各種攻擊，因此理想化的合理性就不太清楚了。
最終結果是具有工具支持的正式系統，這些系統是完善的並且能夠對您感興趣的方案進行建模，並且通常非常容易使用。傳統的數學證明很有用，但很難使用。
答案肯定會有點基於意見，因為沒有人能真正說出手動檢查是否比自動檢查更有說服力。畢竟，如果成功地與第三方溝通/銷售，兩者都可以令人信服。
從我個人的角度來看，最好的方法是手動驗證自動驗證的結果。因此，首先進行自動驗證，然後手動檢查/驗證自動驗證工具產生的正面和負面結果。這樣更徹底，您將兩全其美。
除此之外，請記住沒有像“100% 安全”這樣的東西。
我們可以接近，但我們很可能永遠無法達到完美的安全性。