This archive contains materials (software, lab manuals, slides, solutions) for two practical exercises on use of formal methods in security: * Known Plaintext Attack on a Stream Cipher using a SAT Solver * An Information Flow Control Type System Both practical exercises are available in a short version and a longer, more detailed version. These practical exercises were developed to support the Cyber Security Body Of Knowledge (CyBOK), in particular the Formal Methods in Security knowledge area introduced in CyBOK 1.1.