While the design of block ciphers that are provably secure against all attacks, still eludes us, it is possible to make designs that resist differential and linear cryptanalysis, which are two very important general methods of cryptanalysis on symmetric algorithms. The Wide Trail design strategy allows to construct ciphers for which it is very easy to prove security against differential cryptanalysis. This is possible by choosing linear maps for which it is easy to show lower bounds on the number of active S-boxes. These linear maps can be derived from MDS codes in order to obtain the best possible diffusion. The same methods can be used to obtain provable security against linear cryptanalysis, in particular when linear cryptanalysis is defined in terms of the trace map.