search

DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols
GNU General Public License v3.0
17 stars 2 forks source link

Intruiging performances of equivalence by session #68

Open irakoton opened 4 years ago

irakoton commented 4 years ago

Here is a file where equivalence by session is significantly faster than the analogue verification query for determinate processes. The file models a sequence

P; P; ...; P

where the sequence is modelled by a form of token passing without private channels, but with a private function symbol (more detailed explanations in the file).

session_faster.txt

VincentCheval commented 4 years ago

I don't explain yet the difference of time but there is a bug for sure (caught when doing a make debug)

Internal Error: [data_structure.ml >> IK.transfer_incremented_knowledge_into_knowledge] Incorrect index counter
VincentCheval commented 4 years ago

I solved the bug from "make debug" but I still don't understand the difference of speed. The partition tree in determinate is somehow 10 times bigger than in session equivalence (1M nodes vs 130K nodes).

I leave the issue open but I'm changing the tag.