Revert "decrease version numbers"; back at 0.5.0.0

This reverts commit 0e39c2b70114913d9930e964b321e94aab81a93d.
fix #53: migrate to yesod-1.0 and upgrade other dependencies
reimplemented constraint solver

new features
  - We can now verify properties over the extended traces, which log all
    KU-actions of the intruder. This allows to formulate typing invariants as
    standard security properties. See the examples/iso-tomas/M2_typing.spthy
    protocol for an example. Note that attack extraction also works for such
    typing properties. We might be able to use this to detect typeflaw
    attacks...well provided we have a typing assumption.

changes to solver
  - All construction steps are maded explicit using the KU-actions logged in
    construction rules. These actions are must always be equal to the
    conclusion of the construction rules.
  - Attack extraction also works in the presence of Last-atoms.
  - Stronger simplification of guarded formulas.

regressions tests
  - all protocols in 'examples/stable' and 'examples/csf12' yield the same
    verification/falsification result. Some protocols have shorter proofs
    because of the better formula simplifier. It also seems that the heuristic
    for selecting KU-goals has changed slightly. Probably because KU-actions
    are ordered differently from the previous KU-goals.

  - the new solver is about 1.5x slower than the old implementation.
    Especially for the STS_MAC_fixN protocols it is 2x slower, which is a
    hefty price to pay. However, I expect that we can improve the speed. I
    have not done any profiling yet.

changes to the implementation
  - I have performed a massive cleanup. The code is now in good correspondence
    with the paper (my thesis in case of the new constraint reduction rules).
    It is commented and ready to be built upon.

  - The module hierarchy is as follows.

      Theory.Model               -- modeling security protocols and properties
      Theory.Constraint.System   -- constraint systems
      Theory.Constraint.Solver   -- constraint solving steps
      Theory.Proof               -- proof constructed using the constraint
                                 -- solver
  - added convenience functions:

    * added termVar, termVar', ltermVar, ltermVar', ltermNodeId,
    * ltermNodeId' destructors
updated changelog for 0.5.0.0
added README
final model of StatVerif Example 1 - simple hardware device
better support for unique fact instances

We automatically compute a simple under-approximation to the set of facts with
unique instances. We then exploit this during proof/attack search. We also
implemented some further simplification rules for 'Last'-atoms. This should
make attack extraction complete again.
Wrote a README explaining the repository structure
More complicated version of StatVerif example working again
started adapting the MANUAL to explain the new typing stuff
mark README as markdown
better README
wibbles in README
updated stateful examples
added support functions for terms with bound variables
simplify variable indices as part of prover
solver tweaking: defer looping premises and split node-id equalities
formalized and interactively verified minimal stream protocol
modeled and verified TESLA_Scheme1
formatting wibbles