暗号および暗号に基づく情報セキュリティ技術は，現代のネット社会では必須機能となっており，その利用は拡大する一方である．このようなシステムに安全上の問題が生じた場合その社会的な損失は甚大であり，そこで用いられる暗号および暗号応用システムの安全性を検証することは実用上大変重要である．
現在，暗号および暗号応用システムの安全性を検証する方法としては，計算量理論に基づく安全性証明手法（計算論的証明手法）が標準的手法として暗号理論において確立している．一方，それら安全性を数理的技法（記号論理的証明手法）の立場から捉えた研究も活発に行なわれてきた．しかし，従来これら二つの手法の相互関係についてはほとんど研究されていなかった．
最近，この二つの手法の相互関係についての研究が始められるようになり，計算論的証明手法の進展（汎用的結合可能性，ゲーム列による証明手法など）ともあいまって，研究が活性化しつつある．例えば，標準的安全性証明（計算論的証明）に対する数理的技法の有効性（健全性／完全性）などが研究され始めた．これにより，数理的技法が，計算論的証明手法の簡明化・機械化に有効であることが明らかになりつつある．数理的技法の優れている点は，証明生成・検証（の一部）を機械化することで，証明のモジュール化や透明性が高まることであり，今後さらに増大すると思われるより複雑な暗号応用システム・プロトコルの安全性証明の簡明化に貢献することが期待される．
本研究部会は，このような最新動向を踏まえて，数理的技法による暗号や暗号応用／情報セキュリティシステムの安全性証明についての研究発表／意見交換を行なう場として設立するものである．とくに，従来あまり交流することのなかった暗号研究者と数理的技法（フォーマルメソッド）研究者が交流／共同研究する場としての役割を期待するものである．