量子暗号は，光子（光の粒子）の一つ一つに情報を載せる暗号方式です．盗聴者への情報漏洩をゼロにできる画期的な暗号で，究極の暗号とも呼ばれています．このように，量子物理の応用により従来不可能と思われていたことが実現できるようになりました．その一方で，安全性の証明はますます複雑化しています．私たちは，古典暗号の安全性証明で用いられるフォーマルメソッドの手法を量子暗号に応用し，量子暗号の安全性を世界で初めてコンピュータで証明しました．量子暗号の安全性がコンピュータで確認されたことにより，量子暗号の普及促進への貢献が期待できます．