電子投票や医療に関わる通信などでは，通信プロトコル（通信の仕組み）により匿名性・プライバシなどの安全性が担保される必要がある．また，通信プロトコルの安全性を人手で正確に検査することは困難である．そこで本研究では，通信プロトコルの安全性の高精度自動検証方法を考案した．特に，未解決問題であった一方向関数を用いた通信プロトコルの高精度自動検証を可能にした．