-
jdreier authored
Inntroducing a new feature in Tamarin: automatic generation of sources lemmas. To enable source lemma generation, Tamarin needs to be launched using the command line parameter --auto-sources. The theory behind this PR is explained in the upcoming ESORICS'20 paper Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols. * Started implementing auto-generated source lemmas * first running version of auto-generated source lemmas * auto-generated source lemmas in diff mode * fixed spurious wellformedness errors * fixed encrypted subterms, consider other input facts * do not consider variable as deepest encrypted subterm * use all conclusion facts * add conclusion index to out annotation * unfolding variants if necessary * fixed protected subterm computation * handle rule names correctly, pretty print variant rules as rules modulo AC * examples * README for examples * Added auto-sources regression test