Snowdream

最近有點忙，今天總算在某個課題deadline前把論文憋出來交上去了。跑這兒來推薦兩篇上個月看到的比較有意思的paper，都比較偏理論，也很老。

今天寫介紹下第一篇，劍橋大學的A Logic of Authentication，中了SOSP '89，整理后發在1990年的ACM Transactions on Computer Systems上。
http://www.csie.fju.edu.tw/~yeh/research/papers/os-reading-list/burrows-tocs90-logic.pdf

（另一篇是Safe Kernel Extensions Without Run-Time Checking，改天再寫點介紹）

這篇paper的主要工作是通過構造一種多種類的模態邏輯(many-sorted model logic)，來檢查網絡中驗證協議的安全性。

基礎的邏輯分三部分：
原語，如驗證雙方A和B，以及服務器S，下文用P Q R泛指
密鑰，如K_ab代表a和b之間的通訊密鑰，K_a代表a的公鑰，{K_a}^{-1}代表對應的私鑰，下文用K泛指
公式（或者陳述），用N_a, N_b等表示，下文用X Y泛指

接下來定義以下約定（constructs）
P 信任 X: 原語P完全信任X
P 看到 X: 有人發送了一條包含X的信息給P，P可以閱讀它或者重復它（當然通常是在做了解密操作后）
P 說了 X: 原語P發送過一條包含X的信息，同時也可以確定P是相信X的正確性的
P 控制 X: P可以判定X的正確與否。例如生成密鑰的服務器通常被默認為擁有對密鑰質量的審核權。
X 是新鮮的: 在此之前X沒有被發送過。這個事實可以通過綁定一個時間戳或者其他只會使用一次的標記來證明。
P <-K-> Q: P和Q可以通過共享密鑰K進行通訊，且這個K是好的，即不會被P Q不信任的原語知道。
K-> P: P擁有K這么一個公鑰，且它對應的解密密鑰K^{-1}不會被其他不被P信任的原語知道。
P <=X=> Q: X是一個只被P和Q或者P和Q共同信任的原語知道的陳述，只有P和Q可以通過X來相互證明它們各自的身份，X的一個例子就是密碼。
{X}_K: X是一個被K加密了的陳述
<X>_Y: 陳述X被Y所綁定，Y可以用來證明發送X的人的身份

好了，總算把這些約定列完了，然后來看看通過這些約定能推出一些什么東東：
如果 P 相信 (P <-K-> Q), 且 P 看到 {X}_K，那么 P 相信 Q 說了 X。
這個例子很簡單，既然P Q有安全的密鑰K，那么P看到通過K加密后的X肯定認為就是Q發出的。

又比如，
如果 P 相信 Q 控制 X，P 相信 (Q 相信 X)，那么 P 相信 X
也很容易理解，既然 P 相信 Q 的判斷，那么 Q 相信什么 P 自然也就相信了。

再舉一個例子
如果 P 相信 Y 是新鮮的，那么 P 相信 (X, Y) 也是新鮮的。
這里(X, Y)表示 X 和 Y 的簡單拼接，也很容易理解，既然 Y 之前沒出現過，那么 X 和 Y 的組合自然也沒出現過。

一個協議要被定義為安全，最起碼要滿足
A 相信 A <-K->B，B 相信 A <-K->B
即雙方要互相信任密鑰是安全的

再健壯一點的協議，還要滿足
A 相信 (B 相信 (A 相信 A <-K->B))，反之一樣
即A B不僅相信密鑰，也相信對方相信自己對密鑰的信任。

有了這些簡單卻強大的工具后，接下來這篇paper開始著手分析一些協議，包括Kerberos協議，Andrew Secure RPC 握手協議等，還指出了其中的一些問題和改進措施，例如CCITT X.509 協議中可以通過重復發送一條老的信息來模仿成加密雙方中的一員。

具體的分析不貼上來了，一方面對于我這個不熟悉TeX的人來說碼公式實在麻煩，另一方面我實在困死了 =_=

建議有興趣的朋友好好看看這篇經典paper