安全方面的經(jīng)典論文:A Logic of Authentication
Posted on 2009-03-18 03:10 ZelluX 閱讀(2522) 評(píng)論(0) 編輯 收藏最近有點(diǎn)忙,今天總算在某個(gè)課題deadline前把論文憋出來交上去了。跑這兒來推薦兩篇上個(gè)月看到的比較有意思的paper,都比較偏理論,也很老。
今天寫介紹下第一篇,劍橋大學(xué)的A Logic of Authentication,中了SOSP '89,整理后發(fā)在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,改天再寫點(diǎn)介紹)
這篇paper的主要工作是通過構(gòu)造一種多種類的模態(tài)邏輯(many-sorted model logic),來檢查網(wǎng)絡(luò)中驗(yàn)證協(xié)議的安全性。
基礎(chǔ)的邏輯分三部分:
原語,如驗(yàn)證雙方A和B,以及服務(wù)器S,下文用P Q R泛指
密鑰,如K_ab代表a和b之間的通訊密鑰,K_a代表a的公鑰,{K_a}^{-1}代表對(duì)應(yīng)的私鑰,下文用K泛指
公式(或者陳述),用N_a, N_b等表示,下文用X Y泛指
接下來定義以下約定(constructs)
P 信任 X: 原語P完全信任X
P 看到 X: 有人發(fā)送了一條包含X的信息給P,P可以閱讀它或者重復(fù)它(當(dāng)然通常是在做了解密操作后)
P 說了 X: 原語P發(fā)送過一條包含X的信息,同時(shí)也可以確定P是相信X的正確性的
P 控制 X: P可以判定X的正確與否。例如生成密鑰的服務(wù)器通常被默認(rèn)為擁有對(duì)密鑰質(zhì)量的審核權(quán)。
X 是新鮮的: 在此之前X沒有被發(fā)送過。這個(gè)事實(shí)可以通過綁定一個(gè)時(shí)間戳或者其他只會(huì)使用一次的標(biāo)記來證明。
P <-K-> Q: P和Q可以通過共享密鑰K進(jìn)行通訊,且這個(gè)K是好的,即不會(huì)被P Q不信任的原語知道。
K-> P: P擁有K這么一個(gè)公鑰,且它對(duì)應(yīng)的解密密鑰K^{-1}不會(huì)被其他不被P信任的原語知道。
P <=X=> Q: X是一個(gè)只被P和Q或者P和Q共同信任的原語知道的陳述,只有P和Q可以通過X來相互證明它們各自的身份,X的一個(gè)例子就是密碼。
{X}_K: X是一個(gè)被K加密了的陳述
<X>_Y: 陳述X被Y所綁定,Y可以用來證明發(fā)送X的人的身份
好了,總算把這些約定列完了,然后來看看通過這些約定能推出一些什么東東:
如果 P 相信 (P <-K-> Q), 且 P 看到 {X}_K,那么 P 相信 Q 說了 X。
這個(gè)例子很簡(jiǎn)單,既然P Q有安全的密鑰K,那么P看到通過K加密后的X肯定認(rèn)為就是Q發(fā)出的。
又比如,
如果 P 相信 Q 控制 X,P 相信 (Q 相信 X),那么 P 相信 X
也很容易理解,既然 P 相信 Q 的判斷,那么 Q 相信什么 P 自然也就相信了。
再舉一個(gè)例子
如果 P 相信 Y 是新鮮的,那么 P 相信 (X, Y) 也是新鮮的。
這里(X, Y)表示 X 和 Y 的簡(jiǎn)單拼接,也很容易理解,既然 Y 之前沒出現(xiàn)過,那么 X 和 Y 的組合自然也沒出現(xiàn)過。
一個(gè)協(xié)議要被定義為安全,最起碼要滿足
A 相信 A <-K->B,B 相信 A <-K->B
即雙方要互相信任密鑰是安全的
再健壯一點(diǎn)的協(xié)議,還要滿足
A 相信 (B 相信 (A 相信 A <-K->B)),反之一樣
即A B不僅相信密鑰,也相信對(duì)方相信自己對(duì)密鑰的信任。
有了這些簡(jiǎn)單卻強(qiáng)大的工具后,接下來這篇paper開始著手分析一些協(xié)議,包括Kerberos協(xié)議,Andrew Secure RPC 握手協(xié)議等,還指出了其中的一些問題和改進(jìn)措施,例如CCITT X.509 協(xié)議中可以通過重復(fù)發(fā)送一條老的信息來模仿成加密雙方中的一員。
具體的分析不貼上來了,一方面對(duì)于我這個(gè)不熟悉TeX的人來說碼公式實(shí)在麻煩,另一方面我實(shí)在困死了 =_=
建議有興趣的朋友好好看看這篇經(jīng)典paper
今天寫介紹下第一篇,劍橋大學(xué)的A Logic of Authentication,中了SOSP '89,整理后發(fā)在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,改天再寫點(diǎn)介紹)
這篇paper的主要工作是通過構(gòu)造一種多種類的模態(tài)邏輯(many-sorted model logic),來檢查網(wǎng)絡(luò)中驗(yàn)證協(xié)議的安全性。
基礎(chǔ)的邏輯分三部分:
原語,如驗(yàn)證雙方A和B,以及服務(wù)器S,下文用P Q R泛指
密鑰,如K_ab代表a和b之間的通訊密鑰,K_a代表a的公鑰,{K_a}^{-1}代表對(duì)應(yīng)的私鑰,下文用K泛指
公式(或者陳述),用N_a, N_b等表示,下文用X Y泛指
接下來定義以下約定(constructs)
P 信任 X: 原語P完全信任X
P 看到 X: 有人發(fā)送了一條包含X的信息給P,P可以閱讀它或者重復(fù)它(當(dāng)然通常是在做了解密操作后)
P 說了 X: 原語P發(fā)送過一條包含X的信息,同時(shí)也可以確定P是相信X的正確性的
P 控制 X: P可以判定X的正確與否。例如生成密鑰的服務(wù)器通常被默認(rèn)為擁有對(duì)密鑰質(zhì)量的審核權(quán)。
X 是新鮮的: 在此之前X沒有被發(fā)送過。這個(gè)事實(shí)可以通過綁定一個(gè)時(shí)間戳或者其他只會(huì)使用一次的標(biāo)記來證明。
P <-K-> Q: P和Q可以通過共享密鑰K進(jìn)行通訊,且這個(gè)K是好的,即不會(huì)被P Q不信任的原語知道。
K-> P: P擁有K這么一個(gè)公鑰,且它對(duì)應(yīng)的解密密鑰K^{-1}不會(huì)被其他不被P信任的原語知道。
P <=X=> Q: X是一個(gè)只被P和Q或者P和Q共同信任的原語知道的陳述,只有P和Q可以通過X來相互證明它們各自的身份,X的一個(gè)例子就是密碼。
{X}_K: X是一個(gè)被K加密了的陳述
<X>_Y: 陳述X被Y所綁定,Y可以用來證明發(fā)送X的人的身份
好了,總算把這些約定列完了,然后來看看通過這些約定能推出一些什么東東:
如果 P 相信 (P <-K-> Q), 且 P 看到 {X}_K,那么 P 相信 Q 說了 X。
這個(gè)例子很簡(jiǎn)單,既然P Q有安全的密鑰K,那么P看到通過K加密后的X肯定認(rèn)為就是Q發(fā)出的。
又比如,
如果 P 相信 Q 控制 X,P 相信 (Q 相信 X),那么 P 相信 X
也很容易理解,既然 P 相信 Q 的判斷,那么 Q 相信什么 P 自然也就相信了。
再舉一個(gè)例子
如果 P 相信 Y 是新鮮的,那么 P 相信 (X, Y) 也是新鮮的。
這里(X, Y)表示 X 和 Y 的簡(jiǎn)單拼接,也很容易理解,既然 Y 之前沒出現(xiàn)過,那么 X 和 Y 的組合自然也沒出現(xiàn)過。
一個(gè)協(xié)議要被定義為安全,最起碼要滿足
A 相信 A <-K->B,B 相信 A <-K->B
即雙方要互相信任密鑰是安全的
再健壯一點(diǎn)的協(xié)議,還要滿足
A 相信 (B 相信 (A 相信 A <-K->B)),反之一樣
即A B不僅相信密鑰,也相信對(duì)方相信自己對(duì)密鑰的信任。
有了這些簡(jiǎn)單卻強(qiáng)大的工具后,接下來這篇paper開始著手分析一些協(xié)議,包括Kerberos協(xié)議,Andrew Secure RPC 握手協(xié)議等,還指出了其中的一些問題和改進(jìn)措施,例如CCITT X.509 協(xié)議中可以通過重復(fù)發(fā)送一條老的信息來模仿成加密雙方中的一員。
具體的分析不貼上來了,一方面對(duì)于我這個(gè)不熟悉TeX的人來說碼公式實(shí)在麻煩,另一方面我實(shí)在困死了 =_=
建議有興趣的朋友好好看看這篇經(jīng)典paper