Currently the intro part is focused on protocol verification. Maybe this should be renamed to proto-intro.
Then a similar intro aimed at formal verification of programs can be written, e.g. sw-intro. This would be nice to have for the software security later.