An undecidability result for AGh

Stephanie Delaune
Theoretical Computer Science
Volume 368, Issues 1-2 , 5 December 2006, Pages 161-167
http://dx.doi.org/10.1016/j.tcs.2006.08.018

セキュリティに対する論理学的アプローチの論文．
Intruderの行なうことをdeductionとしてモデル化して，証明論を展開する．
頻繁に用いられている公理としてDolev & Yao (1983) のものがあり，それにequational reasoningも付加したものを考えている．
特に，その等式としてアーベル群の公理と準同型性のみを許したものを考えて (これをAGhと呼んでいる)，そのときに与えられたセッションの集合がsecureであるか判定する問題が決定不能であることを証明している．