A Coloured Petri Nets Model of the 5G Authentication and Key Agreement Protocol (Revista Brasileira de Computação Aplicada, 2025)
Background: A segurança nas redes 5G deve proteger as funções de rede e outros componentes responsáveis pelas comunicações ponta a ponta, visando garantir confidencialidade, integridade, disponibilidade, autenticidade e não-repúdio. Algumas funções de segurança que protegem as redes 5G fazem parte de protocolos relevantes, como o 5G Authentication and Key Agreement (5G-AKA). No entanto, o protocolo 5G-AKA apresenta algumas limitações, tornando-se suscetível a ataques, como os de repetição e man-in-the-middle. Resultados: Com o objetivo de analisar o protocolo 5G-AKA em relação às propriedades de segurança e ajudar a identificar possíveis vulnerabilidades e ameaças, redes de Petri coloridas foram usadas para modelar os componentes do protocolo, suas interações e um exemplo de cenário de ataque. O model foi validado por meio de simulações e a técnica de verificação automática de modelos. Conclusões: O modelo pode contribuir para melhorar a segurança das redes 5G ao validar propriedades e comportamentos por meio de simulações e verificação formal. O modelo proposto do 5G-AKA pode ser uma ferramenta relevante para identificar vulnerabilidades e propor medidas de mitigação em diferentes topologias de 5G.