title: Prolog problem: Variable and instanced variable do not unify, why? And how could I do it instead?
body: <p>Okay, hello everyone!</p>
  
  <p>The problem domain for my Prolog problem is cryptographic protocols.</p>
  
  <p>I've a Prolog program I'm trying to run in GNU Prolog. It should work...but of course it doesn't.</p>
  
  <p>I'm trying to put the gist of it here:</p>
  
  <pre><code>% 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).
  </code></pre>
  
  <p>The last rule of the body, "Init_3 == sign([_,Init_2],SignKey)" is the guard that the server is checking.</p>
  
  <p>Now when I trace with Prolog, the last part is instantiated to</p>
  
  <pre><code>sign([c,k_c],k_c-1) == sign([_281,k_c],k_c-1)
  </code></pre>
  
  <p>And then fails. Why doesn't _281 instantiate to c? Everything else is okay. Do I have to use Init_3_1_1 as the variable name? Or is there another way to be able to use the guard?</p>
  
  <p>I hope I explained the problem well, if not, please do tell.</p>