Hierarchical and compositional verification of cryptographic protocols