1.challenge

面临的挑战是 通过组合各部分的独立证明 来建立 复合协议的安全性证明。但组合是一个困难的问题，因为一个组件 泄露的信息并不会影响其自身的安全性，但会降低其他组件的安全性！

因为即使 各个部分的独立证明可能已经确保了它们的安全性，然而，将这些部分组合在一起时，某个组件可能会泄露与其自身无关的信息，但却降低了其他组件的安全性。

如果能找到一种方法，将两者考虑进来，既 组合独立组件的安全性证明，又考虑它们之间的安全降级问题。

2.a framework consisting of two formal systems 由两个正式系统组成的框架

Protocol Derivation System 协议推导系统 (PDS) and Protocol Composition Logic 协议组合逻辑 (PCL).

PDS

PDS从基本组件开始，使用一连串的 组合、细化、转化操作来组合或者扩展。

安全协议推导框架由 一组基本的构件（组件）和一组操作（用于从旧的协议中构建新的协议） 组成。

操作可以分为:

1.composition

组合composition（组合了两个协议，有并行合成和顺序合成两种操作。对于顺序合成：将第一个组件的输出给第二个组件的输入）、

2.transformation

转换transformation（作用于单个协议，它会修改协议的若干步骤，通过 将数据从一个消息移动到另一个，或组合步骤，或插入一个或多个附加步骤。例如，在同一个party中，将数据从某个协议信息移动到一个更早的消息中）

Message component move, T1： 消息组件移动，将消息m中的顶层字段t移动到之前的消息m’中，其中，它们具有相同的发送方和接收方，并且t在 消息m和消息m‘之间没有生成或接收到新数据，否则会出现后续过程数据不一致的情况。使用该转换的原因是 为了减少协议中总消息数量。

Binding, T2：绑定。

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-40Xc2QGg-1691330903723)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691310058970.png)]绑定转换通常以某种有意义的方法将协议的一部分信息添加到另一部分，以绑定这两部分。上述我们将 n 添加到后续消息的签名部分中，我们首先使用T1转换，将n移动到第二条信息，然后在应用T2，从而获得右边的协议，这样可以确保m和n属于同一个会话。

Cookie, T3：

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-BXUKC8Sx-1691330903726)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691329937787.png)]

Cookie转换的目的是使协议对blind denial-of-service攻击具有抵抗力。在传统的协议中，响应方在收到发起方的消息之后会立即进行昂贵的计算和状态的创建，攻击者可以利用这一点进行大量的请求来消耗响应方的 **计算资源和内存资源，从而导致拒绝服务攻击。**使用cookie转换时，我们假设消息由两部分组成：1.可以在不执行任何昂贵操作的情况下计算出来mc2；2.需要昂贵操作的me2。响应方在接收到第一条消息后，不会创建本地状态，也不会执行昂贵的计算。它会将一个不可伪造的token（cookie）发送回给发起方I，只有I返回了此cookie后，才恢复协议的运行。cookie是消息 **m1和mc2的带密钥的哈希值，**注意，HKR只有R知道。昂贵的计算和状态的创建都被推迟到发起者可以通过 它声称是自己的IP地址 接收信息之后，因此产生的协议可以抵御 盲目dos攻击。

3.refinement

细化refinement（作用于单个协议的消息组件，比如使用加密nonce替换明文nonce，它不会改变消息的数量或协议的基本结构）。

R1：[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-KVgggVWw-1691330903728)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691223193064.png)]

K是 对等方共享的密钥，这里的目的是提供身份保护，为了抵抗passive attackers。因为签名内容是public的，所以，如果签名不加密，攻击者可以验证对主体身份的猜测。

R2：[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-N351oQjo-1691330903734)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691223896422.png)]

签名itself可以证明该term m是由实体X生成的，附加的keyed hash（基于密钥的哈希）可以证明实体X拥有密钥K。

R3：

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-bgN3Ow8u-1691330903735)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691231910708.png)]

它与R2的作用相同。

R4：

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-4WjfA9AF-1691330903736)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691232090488.png)]

Y是peer（对等体）， 假设X拥有Y的必要识别信息 。

R5：

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-ciyJ1XXB-1691330903737)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691233530602.png)]

nx是一个新鲜值， Diffie-Hellman指数的计算成本很高，故使用了nonce随机数，使用nonce使得可以在多个会话中重复使用指数，但这会使完全前向保密性丢失。

R6

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-UDAClgbN-1691330903738)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691234338693.png)]

IDX表示X的公钥证书，对于对方可能没有对应的公钥证书的情况，无法对 签名的有效性进行验证，通过将 证书和签名一起发送，以便接收方可以验证签名的有效性，从而解决这个问题。这样，**通过包含证书，**协议可以消除 **进行会话之前必须持有对方公钥证书的假设。**满足在对方可能没有公钥证书的情况下，仍然能够验证签名的有效性。

R7：

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-fmLl2lbo-1691330903739)(C:\Users\Administrator\AppData\Roaming\Typora\typora-user-images\1691304772109.png)]

K’和K是peer之间的 共享key，role用来标识产生m的协议角色（如：发起者或响应者）。

组件 是构件更大协议的基本协议步骤或步骤集合。如 Diffie-Hellman key exchange 和 challenge-response 就是基本组件。一个协议组件包括了一组角色（发起者、响应者、服务器），每个角色都有一系列的输入、输出和协议动作。直观地说，执行协议角色的principal从一个已知输入的状态开始，执行规定的动作，然后产生输出。

PCL

PCL是Floyd-Hoare风格的逻辑[52，64]，支持协议属性的公理化证明。 关于 公理化证明，它是一种通过使用公理和推理规则来推导出逻辑论断的方法。这意味着，使用 一组公理和推理规则来，利用已知的 公理和协议规范，推导出关于协议安全性或其他属性的结论。从而，可以 形式化地证明协议的正确性或安全性。

上述方法的最终目标是为PDS中的每个 派生操作 开发PCL的证明方法，从而实现 协议及其安全性证明 的并行开发。