序言 - 試圖從最初的知識構建，限制無限建設

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)...) 

但我想限制了上述消息建築物的特殊格式。 在初始化的例子，我想允許的

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). 

好吧，這可能有點多，但我不知道我如何能更短作出這個。如果有人有一個好主意，請告訴。

編輯：

好的，也許編程問題有點隱藏。因此，基本上，我如何限制消息從初始知識知道（數據，1）（使用enc，sign和concatenation [，]）到有限範圍（由上面的特殊格式定義）（即如果消息首先不包含此模板，則不生成enc（enc（Data，Key），Key）？

Answer 1

您可以爲每條消息定義一個「長度」函數，然後使用它來首先獲取較短的消息。

例如，考慮以下幾點：

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

此代碼識別/產生0和1的列表。 如果我們只使用列表（L），我們將得到零： []，[0]，[0,0]，[0,0,0] ....

但是，如果我們使用長度/ 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 ; 

但是，這不會擺脫你不想要的模式;它會讓它稍後出現。在這個例子中，如果我不希望列表在開始長度爲零時不夠好（仍然有助於生成「有意義」的結果）

真正的修復是創建一個模式識別器來過濾和只得到好的信息;這也可以用長度來完成，當你發現你有一個非法模式時，將長度設置爲無限長。

另一個解決方案是重組謂詞。在這個例子中，如果你先放置1個謂詞來獲得從1開始的列表，那麼在本例中爲 。 或者你也可以使用像謂詞（多）層： first_list（[1 | T]： - 列表（T）

只是一些想法:)