Open sgiampietro opened 1 year ago
The diffie-hellman equational theory now includes a "DH_neutral" symbol, this does not appear in the manual though: ( at least not here https://tamarin-prover.github.io/manual/develop/book/004_cryptographic-messages.html ).
It often appears in trivial attacks and I think for users it would be useful if it was mentioned in the theory definition. This is also true for the release version!
The diffie-hellman equational theory now includes a "DH_neutral" symbol, this does not appear in the manual though: ( at least not here https://tamarin-prover.github.io/manual/develop/book/004_cryptographic-messages.html ).
It often appears in trivial attacks and I think for users it would be useful if it was mentioned in the theory definition. This is also true for the release version!