本研究では，ガロア体上の算術演算として記述される攻撃対策を施した耐タンパー性暗号プロセッサの形式的設計技術の確立を目指し，その形式的記述・検証手法を開発した．また，その応用として高効率な耐タンパー性暗号プロセッサの設計・開発を行った．特に，近年暗号プロセッサに物理的に直接アクセスして秘密情報を奪うサイドチャネル攻撃の脅威が急速に高まっていることから，サイドチャネル攻撃対策に着目し，同対策を施した暗号プロセッサの形式的設計・検証手法の開発および同対策を施した暗号プロセッサの試作・評価を推進した．