安全协议的新逻辑

安全协议的新逻辑

1新逻辑与串空间模型1.1新逻辑及其应用假设p、q和r是协议的对象，并且是所有参与协议的元素的集合。c是一条信道，k是密钥，x是消息。w（c）是c视道c的集合，r（c）是读取信道c的主体的集合，c（x）是信道c中的消息x，f表示公式。P|≡X:表示协议从开始到结束的整个运行过程中P一直相信X.P|～X:表示P在某时发送了一个包含X的消息,但不能确定它是何时发送的.P||～X:表示P在本轮协议中发送了X.P|⇒X:表示P对X有仲裁权.P<X:表示P可见X.P<C(X):表示有主体通过信道C发送了消息X,P可以看到.如果P不能读信道C,那么P不能识别和理解此消息.P<X|C:表示P通过信道C接收了消息X,只有当有某个主体(不是P)通过信道C发送了消息X,并且P可读信道C.#(X):表示X是新鲜的.X在当前协议轮之前未被说过.ΡΚ↔QP↔KQ:表示密钥K只为P和Q所知.ΚαΡαKP:表示K是P的公钥,K-1是P的私钥,K-1只能是P拥有或者P相信的实体拥有.{X}K:表示用K加密X.〈X〉Y:表示X和秘密Y的组合,Y的出现证明了谁发送了〈X〉Y.P∩x∩Q:表示秘密X只为P和Q所知.(X,Y):表示消息X和消息Y的组合消息.如果φ是一个公式,那么下列表示也是一个公式,P|≡φ:P相信φ为真,并不意味着φ为真.如果φ1和φ2是公式,那么φ1∨φ2、φ1∨φ2和φ1→φ2都是公式.在新逻辑中给出了25条推理规则用于安全协议的分析,31条合成规则用于安全协议的设计,使安全协议的设计和分析可以在同一中逻辑框架中进行.消除了用一种方法来设计安全协议而用另一种方法来分析协议的不一致性.通过这种新逻辑的运用,可以将安全协议的初始条件直接运用到安全协议的分析和设计中,减少了初始条件的形式化过程,提高了工作效率.有关新逻辑的推理规则和合成规则见文献.1.2randmap安全串(strand)是协议中的主体可以执行的事件序列.对于诚实的主体,该事件序列是由协议定义好的,由发送消息的事件和接收消息的事件所组成;对于攻击者,该事件序列由攻击者的行为来确定.串空间(strandspace)是诚实的主体串和攻击者串所组成的集合.束(bundle)是串空间的一个子集,用来表示一个完整的协议.束是一个有限无环图,每个结点由两部分组成,即<串名,位置>,其中串名指出该结点所属的串的名称,位置指出该结点在串中的位置编号.束中有两种边,这两种边表示了结点间的因果依赖关系.第一种边:〈s,i〉→〈s1,i1〉,表示串s中的第i个结点发送消息给串s1中第i1个结点;第二种边:〈s,i〉⇒〈s,i+1〉,表示结点〈s,i〉是结点〈s,i+1〉的直接前驱.在串空间模型中,协议的正确性问题可以表示为不同串之间的因果连接关系.有关串空间模型的详细资料,见文献.2基于principal的s/s转换设〈B,s,i〉表示束B中的点,也就是束B中串s上的第i个结点,则公式j在〈B,s,i〉为真表示为〈B,s,i〉|=φ.公式φ蕴涵公式Ψ表示为φ→Ψ,φ→Ψ在〈B,s,i〉为真表示为〈B,s,i〉|=(φ→Ψ).用principal(s)表示执行串s的主体.用r(C)表示可读信道C的主体集合,用w(C)表示可写信道C的主体集合.2.1基本句子的含义2.1.1p.dx〈B,s,i〉|=P|≡X当且仅当在束B的结点〈s,i〉满足:(a)principal(s)=P;(b)〈B,s,i〉|=X.2.1.2principalt,l〈B,s,i〉|=P|～X为真当且仅当束B中或者束B′(B′表示当前协议轮B的前面的某个轮)中存在一个结点〈t,j〉,满足:(a)principal(t)≠P,principal(s)=P;(b)〈s,i〉≤〈t,j〉;(c)term(〈t,j〉)=+X,term(〈s,i〉)=-X.2.1.3principal/s计算p〈B,s,i〉|=P||～X为真当且仅当束B中存在一个结点〈t,j〉,满足:(a)principal(t)≠P,principal(s)=P;(b)〈s,i〉≤〈t,j〉;(c)term(〈t,j〉)=+X,term(〈s,i〉)=-X.2.1.4束b中多个结论〈B,s,i〉|=P|⇒X为真当且仅当束B中存在一个结点〈s,j〉,满足:(a)principal(s)=P;(b)〈B,s,j〉|=X.2.1.5principalt驱动〈B,s,i〉|=P□X为真当且仅当束B中存在一个结点〈t,j〉,满足:(a)principal(t)≠P,principal(s)=P;(b)〈t,j〉≤〈s,i〉;(c)term(〈t,j〉)=+M,X⊂term(〈s,i〉)=-M(也就是X是M的子术语).2.1.6principal/t〈B,s,i〉|=P□C(X)为真当且仅当束B中存在一个结点〈t,j〉,满足:(a)principal(t)≠P,principal(s)=P;(b)〈t,j〉≤〈s,i〉;(c)term(〈t,j〉)=+X.2.1.7principalt驱动〈B,s,i〉|=P□X|C为真当且仅当束B中存在一个结点〈t,j〉,满足:(a)principal(t)≠P,principal(s)=P;(b)〈t,j〉≤〈s,i〉;(c)term(〈t,j〉)=+X,P□r(C),term(〈s,i〉)=-X.2.1.8elyoringingintitat3.3.4和4.33.3.35.35.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.555.55.55.55.55.55.55.55.55.555.55.55.55.55.55.55.55.55.55.55.55.55.55.555555555555555.555.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.55.〈B,s,i〉|=#(X)为真当且仅当束B中存在一个结点〈t,j〉,满足:(a)〈t,j〉≤〈s,i〉;(b)X唯一源发(uniquelyoriginating)于结点〈t,j〉.2.1.9ΡΚ↔Q〈B,s,i〉|=ΡΚ↔Q⟨t,j⟩.2.1.9P↔KQ⟨B,s,i⟩|=P↔KQ为真当且仅当束B中存在两个结点〈t1,j1〉、〈t2,j2〉,满足:(a)principal(t1)=P,principal(t2)=Q;(b)〈t1,j1〉≤〈s,i〉,〈t2,j2〉≤〈s,i〉;(c)r(CPQ)=w(CPQ)={P,Q}.2.2个表示公式以下这些公理可以从谓词逻辑和串空间模型中直接得到,证明从略.公理1设〈B,s,i〉为束B中的一个点,φ公式,〈B,s,i〉|=φ,对于束B中的任意一个结点〈t,j〉,如果〈s,i〉≤〈t,j〉,那么〈B,t,j〉|=φ.公理2设〈B,s,i〉为束B中的一个点,φ、Ψ为公式,如果〈B,s,i〉|=φ并且〈B,s,i〉|=(φ→Ψ),那么〈B,s,i〉|=Ψ.公理3设〈B,s,i〉为束B中的一个点,φ、Ψ为公式,〈B,s,i〉|=(φ∧Ψ)充要条件是〈B,s,i〉|=φ并且〈B,s,i〉|=Ψ.公理4设〈B,s,i〉为束B中的一个点,φ、Ψ为公式,〈B,s,i〉|=(φ∨Ψ)充要条件是〈B,s,i〉|=φ或者〈B,s,i〉|=Ψ.公理5设〈B,s,i〉为束B中的一个点,φ为公式,〈B,s,i〉|=φ和〈B,s,i〉|=(⇁φ)只有一个成立(⇁表示公式的否定).2.3在新逻辑中有25条推理规则,由于篇幅的限制,我们只证明一部分规则,其它推理规则可进行类似的证明.另外,用于安全协议设计的合成规则是由推理规则构造出来的,所以只要证明了推理规则即可,相应的合成规则不需要进行额外的证明.定理1(接收规则1)Ρ＜C(X)‚Ρ∈r(C)Ρ|≡(Ρ＜X|C),Ρ＜XP＜C(X)‚P∈r(C)P|≡(P＜X|C),P＜X证明:由P□C(X)知束B中存在一个结点〈s,i〉,使得〈B,s,i〉|=P□C(X),也就是在束B中存在一个节点〈t,j〉,满足:principal(t)≠P,principal(s)=P(1.1)〈t,j〉≤〈s,i〉(1.2)term(〈t,j〉)=+X(1.3)又因为P∈r(C)(1.4)所以term(〈s,i〉)=-X(1.5)由(1.1)(1.2)(1.3)(1.4)(1.5)得到:〈B,s,i〉|=P|≡P□X|C(1.6)由X⊂X(也就是X是X的子术语)和(1.6)得到:〈B,s,i〉|=P□X(1.7)由公理3和(1.6)(1.7)可得:〈B,s,i〉|=(P|≡P□X|C)∧(P□X)所以Ρ＜C(X)‚Ρ∈r(C)Ρ|≡(Ρ＜X|C),Ρ＜XP＜C(X)‚P∈r(C)P|≡(P＜X|C),P＜X成立.定理2(接收规则2)Ρ＜(X,Y)Ρ＜X,Ρ＜Y证明:由P□(X,Y)知束B中存在一个节点〈s,i〉,使得〈B,s,i〉|=P□(X,Y)也就是在束B中存在一个节点〈t,j〉,满足:principal(t)≠P,principal(s)=P(2.1)〈t,j〉≤〈s,i〉(2.2)term(〈t,j〉)=+M,term(〈s,i〉)=-M,(X,Y)⊂M(2.3)因为X⊂(X,Y)⊂M,所以term(〈s,i〉)=-X(2.4)因为X⊂X和(2.1)(2.2)(2.3)(2.4),所以〈B,s,i〉|=P□X(2.5)因为Y⊂(X,Y)⊂M,所以term(〈s,i〉)=-Y(2.6)因为Y⊂Y和(2.1)(2.2)(2.3)(2.6),所以〈B,s,i〉|=P□Y(2.7)由(2.5)(2.7)和公理3得到:〈B,s,i〉|=(P□X)∧(P□Y)所以Ρ＜(X,Y)Ρ＜X,Ρ＜Y成立.定理3(发送规则1)Ρ|≡(w(C)=W)Ρ|≡((Ρ＜X|C)→∨∀Qi(Qi∈W\{Ρ})(Qi|∶x))证明:可以把该规则进行等价变换为:(P|≡(w(C)=W)∧(P□X|C))→P|≡(∨(“Qi(Qi∈W\P)(Qi|～X))),只要证明该公式成立即可.由P□X|C可知,在束B中存在一个节点〈s,i〉使得,〈B,s,i〉|=P□X|C,也就是在束B中存在一个节点〈t,j〉,满足:principal(t)≠P,principal(s)=P(3.1)〈t,j〉≤〈s,i〉(3.2)term(〈t,j〉)=+X,P∈r(C),term(〈s,i〉)=-X(3.3)由w(C)=W和(3.1)(3.2)(3.3)得到:principal(t)=W\P(3.4)由(3.4)可知Qk∈W\P,k=1,2,…,使得principal(t)=Qk(3.5)由(3.3)(3.5)可得:〈B,s,i〉|=∨(“Qk(Qk∈W\P)(Qk|～X))(3.6)由(3.6)和(3.1)可得:〈B,s,i〉|=(P|≡∨(“Qk(Qk∈W\P)(Qk|～X)))(3.7)所以(P|≡(w(C)=W)∧(P□X|C))→P|≡(∨(∀Qi(Qi∈W\P)(Qi|～X)))成立,也就是Ρ|≡(w(C)=W)Ρ|≡((Ρ＜X|C)→∨∀Qi(Qi∈W\{Ρ})(Qi|∶X))成立.定理4(发送规则2)Ρ|≡(Q|∶(X,Y))Ρ|≡(Q|∶X),Ρ|≡(Q|∶Y))证明:由P|≡Q|～(X,Y)可知在束B中存在一个节点〈s,i〉,满足principal(s)=P(4.1)〈B,s,i〉|=(Q|～(X,Y))(4.2)因为X⊂(X,Y),所以〈B,s,i〉|=(Q|～X)(4.3)又因为Y⊂(X,Y),所以〈B,s,i〉|=(Q|～Y)(4.4)由(4.3)(4.4)和公理3可得:〈B,s,i〉|=(Q|～X)∧(Q|～Y)(4.5)由(4.1)(4.5)可得:〈B,s,i〉|=(P|≡(Q|～X))∧(P|≡(Q|～Y))所以Ρ|≡(Q|∶(X,Y))Ρ|≡(Q|∶X,Ρ|≡(Q|∶Y))成立.定理5(新鲜性规则1)Ρ|≡(Q|∶X),Ρ|≡#(X)Ρ|≡(Q||∶X)证明:由P|≡(Q|～X)可知在束B中存在一个节点〈s,i〉,满足〈B,s,i〉|=(Q|～X),或者在束B′中存在一个结点〈t,j〉,满足〈B,t,j〉|=(Q|～X),这里〈t,j〉≤〈s,i〉.因为P|≡#(X),所以只可能是〈B,s,i〉|=(Q|～X)成立,由#(X)马上可得〈B,s,i〉|=(Q||～X),因为principal(s)=P,所以〈B,s,i〉|=P|≡(Q||～X)成立.因此Ρ|≡(Q|∶X),Ρ|≡#(X)Ρ|≡(Q||∶X)成立.定理6(新鲜性规则2)Ρ|≡#(X)Ρ|≡#(X,Y)证明:由P|≡#(X)可知在束B中存在一个节点〈s,i〉,满足〈B,s,i〉|=#(X),也就是束B中存在一个结点〈t,j〉,满足:〈t,j〉≤〈s,i〉(6.1)X唯一源发(uniquelyoriginating)于结点〈t,j〉(6.2)由X⊂(X,Y)和(6.2)得到〈B,s,i〉|=#(X,Y)