Vamos ver se eu consigo explicar agora o que eu vou fazer:
Eu estudei as lógicas certo?* E vi a provabilidade delas e as propriedades de cada uma e como uma estende as outras. Agora, a gente pode usar esse artefato para provar a corretude de sistemas. Mas como? Essa era minha pergunta até hoje. Vamos pegar um protocolo de autenticação que foi o que estudei. Suponha que A queira comunicar-se com B. Temos como predicados as ações de envio e recebimento de mensagens, geração de nonces e uma combinação destes que afirma se a entidade é quem inicia a comunicação ou se é quem responde (isso são dois predicados separados, lógico). Então as minhas premissas são as mensagens que B enviou e recebeu e os nonces gerados e o fato de que B é quem responde e A é quem inicia a comunicação. A partir disso, temos que ser capazes de derivar toda a sequencia de trocas das mensagens na ordem correta (ainda não entendi muito bem como se coloca na lógica essa restrição da ordem das fórmulas). O mais mais mais legal é que, quando não conseguimos chegar numa prova, conseguimos ver qual é a vulnerabilidade do protocolo e de que modo pode ser feito um ataque! Incrível hehe
Quando eu estiver entendendo isso direitinho meeesmo, vou escrever um documento explicando (que na verdade deveria ser meu POC… mas eu não sei qual o deadline da documentação ainda).
*A única coisa que eu não consegui me acostumar ainda foi esse ponto de interrogação esquisito junto com a letra ‘w’.