Prolog - 尝试从初始知识构建，限制无限构建

Question

我正在尝试构建一个知识库，指示攻击者能够发送以访问某些秘密数据的消息（我的示例使用 TLS 协议的简化版本，即 Client-Server-Certificate-CertificationAuthority-SessionKey）。

无论如何，如果需要进一步解释，请询问。

我的问题：

使用协议发送消息，如下所示：

init(Init_1, Init_2, Init_3)

此消息有 3 个参数。 每个参数都需要具有特殊格式。 例如：

nonce(Init_1)
publicKey(Init_2)
Init_3 = sign(SignedData, PrivateKey)
SignedData = [Id,PublicKey]
id(Id)
publicKey(PublicKey)

此外，要接受消息并发送以下消息，必须检查守卫：

ext(Init_3,Init_2) % meaning the signature can be extracted with the second parameter
extractedData(Init_3,Data) % Data is the extracted data from the signature
nth(2,Data,Init_2) % the second atom of the extracted data is the same as the second parameter

最重要的是，攻击者只能发送带有他知道的参数的消息。

knows(Init_1),
knows(Init_2),
knows(Init_3)

好吧，攻击者有能力获取知识。基本上他能读懂所有的消息，所以他知道一开始的参数，这就是他的初始知识。 默认消息示例：

init(n_c , k_c , sign([c,k_c],k_c-1) )

导致

knows(n_c,1) % the 1 is an artifact which may or may not be needed; tells the depth of the knowledge
knows(k_c,1)
knows(sign([c,k_c],k_c-1),1)

编辑：我删除了有关从加密和/或签名数据中提取数据的长部分。基本上在收集默认消息并断言其中的初始知识之后，每个可解密和可提取的数据都被添加到初始知识中。

我现在的问题： 我想通过对初始知识中的内容进行加密和签名来构建新消息。 这本身很容易，但目前会带来无限的知识增益，因为您可以构建诸如

enc(enc(enc(enc(enc(...(Data, Key)...)

但我想将消息构建限制为上面的特殊格式。 在 init 的示例中，我希望允许构建

sign([Id,PublicKey],PrivateKey)

, 但不允许构建类似

sign(sign([Id,PublicKey],PrivateKey),PrivateKey)

或更糟的东西。

最后但并非最不重要的一点是，这是我的消息构建或参数生成规则：

knows([FirstData,SecondData],Depth) :-
Depth @> 1,
depth(SecondData,B), A is Depth - B,
knows(SecondData,B), knows(FirstData,A).

knows(enc(Data,Key),Depth) :-
Depth @> 1,
DepthMin1 is Depth - 1,
for(KeyDepth,1,DepthMin1),
isKey(Key),
Data \== enc(_, Key),
    knows(Key, KeyDepth),
knows(Data, DepthMin1).

knows(sign(Data,Signature),Depth) :-
Depth @> 1,
DepthMin1 is Depth - 1,
for(KeyDepth,1,DepthMin1),
isKey(Signature),
Data \== sign(_, Signature),
knows(Signature,KeyDepth),
knows(Data,DepthMin1).

好吧，这可能有点多，但我不知道我可以把它缩短多少。如果有人有一个绝妙的主意，请告诉我们。

编辑：

好的，也许编程问题有点隐藏。因此，基本上，如何将消息的生成从初始知识 knows(Data,1) （使用 enc,sign 和串联 [,]）限制到有限范围（由 定义）特殊格式 上面）（即，如果消息一开始不包含此模板，则不生成 enc(enc(Data,Key),Key) ）？

Answer 1

您可以为每条消息定义一个“长度”函数，然后使用它首先获取较短的消息。

例如，请考虑以下情况：

list([]).
list([0|T]):-list(T).
list([1|T]):-list(T).

此代码识别/生成 0 和 1 的列表。
如果我们只使用 list(L) 我们只会得到零：
[],[0],[0,0],[0,0,0]....

但是，如果我们对列表使用 length/2，我们将得到我们想要的：

?- length(L,X), list(L).
L = [],
X = 0 ;
L = [0],
X = 1 ;
L = [1],
X = 1 ;
L = [0, 0],
X = 2 ;
L = [0, 1],
X = 2 ;
L = [1, 0],
X = 2 ;
L = [1, 1],
X = 2 ;

但是，这不会摆脱模式你不想要；它只会让它稍后出现。在这个例子中，如果我不希望列表在开始处有零， length/2 还不够好（仍然，它有助于生成“有意义的”结果），

真正的解决方法是创建一个模式识别器来过滤并只获得好的结果消息；这也可以用长度来完成，当你发现你有一个非法模式时，只需将长度设置为无限即可。

另一种解决方案是重新组织谓词。
在示例中，如果您将 1 谓词放在前面，则会先获取以 1 开头的列表。
或者您可以使用（更多）谓词层，例如：
first_list([1|T]:-list(T)。

只是一些想法:)