Formal verification of IFF and NSLPK authentication protocols with CiMPG (S)
Thet Wai · Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering · 2021
Proof scores are programs written in an algebraic specification language, such as CafeOBJ, to conduct formal verification.Thus, the proof score approach to formal verification (PSA2FV) can be regarded as a kind of proving by programming and then flexible.PSA2FV, however, is subject to human errors.To address the issue, a proof assistant called CiMPA was developed for CafeInMaude, the world's second implementation of CafeOBJ.Furthermore, a proof generator called CiMPG was developed to benefit from the strong points of both PSA2FV and CiMPA.Although some case studies have been conducted with CiMPG, it is necessary to do some more.The present paper reports on case studies in which it is formally verified that two authentication protocols enjoy desired properties with CiMPG.