The ro-spi Calculus at Work: Authentication Case Studies