Хорошо, всем привет!
Проблемная область для моей проблемы 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 == sign([_,Init_2],SignKey)» — это защита, которую проверяет сервер.
Теперь, когда я трассирую с помощью Пролога, последняя часть создается для
sign([c,k_c],k_c-1) == sign([_281,k_c],k_c-1)
А потом терпит неудачу. Почему _281 не создает экземпляр c? Все остальное в порядке. Должен ли я использовать Init_3
% 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).
Надеюсь, я хорошо объяснил проблему, если нет, пожалуйста, скажите.
