Initial commit
add STR protocol model
rename STR model since it's a simplified version
add more realistic STR model
- Removed initiator nonce where inappropriate
- added test result timings
add ocaml protocol implementation and
manual translation to spthy file
Fixed indexing error in ResponderLoop rule, blindedRandoms need to be based off the changing index k, not the fixed index j

Added missing dis-equality constraints for R3 in key_reachable_4
add intermediate key actions and secrecy lemma
Typo fixes in STR_ml

Added a version with 2 arguments for AuthOut

Added a version on top of that where the intruder can send authenticated messages using a Corrupt rule
Added IKey action to the ResponderDone rule, otherwise IKey secrecy does not imply Key secrecy, which is what we want.
Added variant with JOIN
- stored proof of key agreement for 2member group with 1 joiner

Changed rule names to take advantage of Cas's new "cleandot"

Variant without authenticated channels allows (obvious!) attacks, tool find them
Added "private function"-based version without authentic channels

The authentic channels are replaced by each message being signed with the private-function-based private key of each sender, while each recipient checks for correct signatures. This models a PKI infrastructure-based signing scheme.

Also, included a minor bug fix in the other protocol definitions.
Added PKI based version of STR

Noted certain timings in comments in PKI and private function version.
Joux-based group protocol - tree generation complete

No cryptographic messages are included yet, but the overall tree generation in the form of subgroup computation is complete, and shown by existential lemmas up to 5 participants
Added protocol rules

Not executable with all rules available, initial loading takes too long.
Restricted to powers of 3

Changed the rules so that only one single Receive rule takes care of all cases, by modifying the three different Send rules. They are all needed. In this version the 2_double and 2_single rules are commented out, so effectively the protocol is restricted to participants that are powers of 3. (Technically speaking, the sum of 3 powers of 3, when ignoring tree generation, is possible as well.)
Added explaining comments, cleaned out unused code
Fixed potential looping for "StepOver1"

- added hash function application to the secret that StepOver1 keeps
Added comments in the group generation

Particularly for the matching cases and why the 2, 1, or 0 remaining case only has to deal with 3-element cases in the "already generated" set.
Added version using intermediate fact AuthIn