Prolog - essayer de construire à partir des connaissances initiales, limiter le bâtiment infini

Question

J'essaie de construire une base de connaissances qui indique les messages qu'un attaquant est capable d'envoyer pour avoir accès à des données secrètes (mon exemple utilise une version simplifiée du Protocole TLS, ce qui signifie Client-Server-Certificate-CertificationAuthority-SessionKey).

Quoi qu'il en soit, si vous avez besoin d'explications supplémentaires, s'il vous plaît demander.

Mon problème:

En utilisant le protocole, les messages sont envoyés, comme ceci:

init(Init_1, Init_2, Init_3) 

Ce message a 3 paramètres. Chacun des paramètres doit avoir un format spécial . Par exemple:

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

En outre, d'accepter le message et envoyer le suivant un garde doit être vérifié:

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 

le plus important, l'attaquant ne peut envoyer des messages avec des paramètres qu'il connaît .

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

Bon, l'attaquant a la capacité d'acquérir des connaissances. Fondamentalement, il peut lire tous les messages, donc il connaît les paramètres au début, qui est son connaissance initiale. Exemple pour un message par défaut :

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

conduit à

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) 

EDIT: Je retiré la partie longue sur l'extraction des données cryptées à partir et/ou des données signées. Fondamentalement, après la collecte des messages par défaut et l'affirmation des connaissances initiales, chaque donnée déchiffrable et extractible est ajoutée à la connaissance initiale.

Mon problème maintenant: Je veux construire de nouveaux messages en cryptant et en signant les choses dans la connaissance initiale. Cela en soi est facile, mais pour le moment conduit à un gain infini de connaissances, parce que vous pouvez construire des choses telles que

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

Mais je veux limiter la construction de message au format spécial au-dessus. Dans l'exemple de init, je veux permettre la construction de

sign([Id,PublicKey],PrivateKey) 

, mais pas quelque chose comme

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

choses ou pire.

Last but not least, voici mon immeuble de message ou génération de paramètres règles:

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

D'accord, cela peut être un peu beaucoup, mais je ne sais pas combien plus courte je aurais pu faire ce. Si quelqu'un a une idée brillante, s'il vous plaît dites-le.

EDIT:

D'accord, peut-être le problème de programmation était un peu caché. Donc, fondamentalement, comment limiter la génération de messages de la connaissance initiale sait (Data, 1) (en utilisant enc, signe et concaténation [,]) à une gamme finie (définie par le format spécial ci-dessus) (c'est-à-dire ne pas générer enc (enc (Data, Key), Key) si le message ne contient pas ce template en premier lieu)?

Answer 1

Vous pouvez définir une fonction "longueur" pour chaque message, puis l'utiliser pour obtenir les messages les plus courts en premier.

par exemple, tenez compte des éléments suivants:

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

ce code reconnaît/produit des listes de 0 et de 1. devrions-nous simplement utiliser la liste (L) nous obtiendrons juste des zéros: [], [0], [0,0], [0,0,0] ....

cependant, si nous utilisons la longueur/2 pour les listes, nous obtiendrons ce que nous voulons:

?- 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 ; 

Cependant, ceci ne supprimera pas les motifs que vous ne voulez pas; ça va juste le faire apparaître plus tard. dans l'exemple, si je ne voulais pas que les listes aient des zéros au début longueur/2 n'est pas assez bon (encore, ça aide à générer des résultats "significatifs")

la vraie solution est de créer un outil de reconnaissance de formes à filtrer et obtenir seulement les bons messages; Cela peut être fait avec la longueur aussi, il suffit de définir la longueur à l'infini lorsque vous découvrez que vous avez un modèle illégal.

Une autre solution consiste à réorganiser vos prédicats. dans l'exemple, si vous mettez le prédicat 1 en premier pour obtenir les listes commençant par 1 en premier. ou vous auriez pu utiliser (plus) couches de prédicats comme: first_list ([1 | T]. - Liste (T)

juste quelques idées :)