Automatos temporizados como ferramenta de verificacao de protocolos de seguranca

Os autmatos temporizados so uma extenso da abordagem terico-automtica da modelao de sistemas em tempo real que introduz o tempo nos autmatos clssicos. Desde que foi proposto pela primeira vez no incio dos anos noventa, tornou-se uma importante rea de investigao e foi amplamente estudado tanto no contexto das lnguas formais como na modelao e verificao de sistemas em tempo real. Os autmatos temporizados utilizam a modelao densa do tempo, permitindo a verificao eficiente de modelos de sistemas sensveis ao tempo cujo correcto funcionamento depende das propriedades do tempo. Uma destas reas de aplicao a verificao dos protocolos de segurana. Este livro centra-se no modelo de autmatos temporizados e utiliza-o como uma ferramenta de verificao de protocolos de segurana. Como estudo de caso, o Neuman-Stubblebine Repeated Authentication Protocol modelado e verificado empregando as propriedades sensveis ao tempo no modelo. As falhas do protocolo so analisadas e comentado sobre os benefcios e desafios do modelo.