序言问题：变量和实例变量不统一，为什么？我怎么能这样做呢？

Question

好的，大家好！

我的Prolog问题的问题域是加密协议。

我有一个Prolog程序我试图在GNU Prolog中运行。它应该工作......但它当然不适用。

我试图把它这里的要点是：

% two people, c (the client) and a (the attacker) 
% we have two public keys (asymmetric cryptographic keys, e.g.PGP) 
publicKey(k_c). 
publicKey(k_a). 
% we have two private keys (asymmetric cryptographic keys, e.g.PGP) 
privateKey(k_a-1). 
privateKey(k_c-1). 
% here I define the two public/private key pairs. 
keyPair(k_c,k_c-1). 
keyPair(k_a,k_a-1). 
% just some kind of id 
id(c). 
id(a). 
% nonces (some kind of value that's always new and is not guessable) 
nonce(n_c). 
nonce(n_a). 
% two functions 
% enc(Data, Key) encrypts Data with Key 
cryptoFunction(enc(_,_)). 
% sign(Data, Key) signs Data with Key (a signature) 
cryptoFunction(sign(_,_)). 

% a default message sent from the client to a server 
init(n_c,k_c,sign([c,k_c],k_c-1)). 

% Now I want to find out all combinations that can be sent without violating the rules 
% The server always checks for some kind of guard (see below) 

% define the message template 
init(Init_1, Init_2, Init_3) :- 
% define the types 
nonce(Init_1), 
publicKey(Init_2), 
id(Init_3_1_1), 
% example: 
% Init_3_1_2 means init 
% third parameter of init (the sign function) 
% first parameter of sign function 
% second part of the concatenation 
publicKey(Init_3_1_2), 
privateKey(Init_3_2), 
% build the message 
Init_3 = sign(Init_3_1,Init_3_2), 
Init_3_1 = [Init_3_1_1,Init_3_1_2], 
keyPair(Init_2,SignKey). 
Init_3 == sign([_,Init_2],SignKey). 

身体的最后一个规则， “Init_3 ==号（[_，Init_2]，SignKey）” 是保护的服务器正在检查。现在

，当我和Prolog的跟踪，最后部分实例化

sign([c,k_c],k_c-1) == sign([_281,k_c],k_c-1) 

然后失败。为什么不_281实例化为c？其他一切都没问题。我必须使用Init_3_1_1作为变量名吗？或者有另一种方式可以使用警卫？

我希望我解释好这个问题，如果没有，请告诉我。

Answer 1

统一是内置的谓词（=）/ 2，而不是（==）/ 2。例如：

?- sign([c,k_c],k_c-1) = sign([_281,k_c],k_c-1). 
_281 = c.