Observational equivalence + induction?

59 views
Skip to first unread message

felipecboeira

unread,
Aug 19, 2022, 9:41:26 AM8/19/22
to tamarin...@googlegroups.com
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

RA-symmetric-counter-loop.spthy
Reply all
Reply to author
Forward
0 new messages