Formal proof of security algorithms based on reachability reduction. - Mohamed Bouziane; Sophie Gire; François Monin; Laurent Nana (MEDES, 2016)