Observational equivalence + induction?

[felipecboeira]

Hello all!

has induction been explored in the context of observational equivalence using Tamarin? I noticed it is mentioned as future work in the CCS15 paper [1]. I have attached a toy example I have been experimenting with. In this model, the 'prover agent' has a monotonically increasing counter to construct messages. Perhaps it would be sufficient to simply allow two counters ('1' and '1'+'1'), instead? Thanks in advance for any pointers :-)

Regards,

Felipe

[1] David Basin, Jannik Dreier, and Ralf Sasse. 2015. Automated Symbolic Proofs of Observational Equivalence. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security (CCS '15). Association for Computing Machinery, New York, NY, USA, 1144–1155. https://doi.org/10.1145/2810103.2813662