Unused subprocess (draft 20 implementation)

[muhammad-usama-sardar]

In ProVerif modeling of draft 20, no piece of code in any process ever uses the subprocess fixedLongTermKeys. Hence, the following code snippet serves no purpose other than adding more confusion to the auditors.

let fixedLongTermKeys() = 
     new skA: privkey;
     new skB: privkey;
     new skM: privkey;
     let pkA = pk(skA) in
     let pkB = pk(skB) in
     let pkM = pk(skM) in
     new pskAB: bitstring;
     new pskAM: bitstring;
     new pskMB: bitstring;
     insert longTermKeys(A,skA,pkA);
     insert longTermKeys(B,skB,pkB);
     insert longTermKeys(M,skM,pkM);
     insert preSharedKeys(A,B,PSK(pskAB));     
     insert preSharedKeys(A,M,PSK(pskAM));     
     insert preSharedKeys(M,B,PSK(pskMB));     
     event WeakOrCompromisedKey(NoPubKey);
     event WeakOrCompromisedKey(pkM);
     event CompromisedPreSharedKey(PSK(pskAM));
     event CompromisedPreSharedKey(PSK(pskMB));
     out(io,(skM,pskAM,pskMB)).

This was checked by defining a simple event test2 and placing this event at the very beginning of the subprocess. Then writing a simple reachability query query event (test2). confirms that it is not reachable.

[bruno-blanchet]

It is true that fixedLongTermKeys is currently not used. It is a possible replacement for the process longTermKeysProc that the people can use by modifying the main process in tls13-draft20-only.pv. (longTermKeysProc provides dynamic long-term keys, while fixedLongTermKeys provides fixed long-term keys as the name says.)