Are you aware of Pi-calculus and ProVerif? ProVerif sounds to address at least some of your requirements. Links: - https://en.wikipedia.org/wiki/%CE%A0-calculus - https://prosecco.gforge.inria.fr/personal/bblanche/proverif/