search

DeepSec-prover / deepsec

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

internal error for reduction rules with non-atomic right-hand sides #63

Closed irakoton closed 4 years ago

irakoton commented 4 years ago

The constraint solver returns an internal error when handling a reduction rule for extracting the public-key used to produce a ciphertext:

reduc h(f(x,g(y))) -> g(y).

where f models encryption and g public key generation. Attached a minimal example where the error is observable (triggers Internal Error: [data_structure.ml >> IK.get] Invalid index.)

internal_error.txt

VincentCheval commented 4 years ago

Should be fixed in beta6. Regression testing on fast examples worked. Would probably need to do the heavy examples too. I'm closing the issue for now. We could reopen it if one of the heavy test fails in the future.