​​論理指向セキュリティ分析
​​Logic Oriented Security Analysis
​​
​​

​​なぜやるのか

​​民主主義という構造体は極めて複雑で、要素を把握しにくい。その性質が原因で課題が放置され、悪意ある攻撃者につけいる隙を与えてきた。
​​
​​民主主義を状態機械とみなし、その健全性に関するsafety(安全性)とliveness(活性)を形式的に記述する。加えて、ある与えられた民主主義に関して、いまそれがどのように安全性がないのかを分析し、どのように活性を確保すれば民主主義の健全性を回復するのかの道筋を示すための方法論を詳述する。
​​
​​

​​どうやるのか

​​​+民主主義の形式的記述​ にある形式記法をもとに、Attack(攻撃)やGriefing(嫌がらせ)が起きたあとの状態機械を想像する。その状態機械に対して「どう安全でないのか」「どうすれば健全な状態に戻るのか」という「処方箋」を思考実験する。
​​
​​

​​なにをやるのか

​​

​​衆愚政治への処方箋

​​
​​■ 症状
​​衆愚政治を根拠にしたDAO4N批判はすべて
​​
​​isFacilitatorsUnsafe か isEducationUnsafe か isMediaUnsafe ということになる。
​​
​​■ 処方箋
​​isEducationLive := 
​​( isDismissible(self) and noStrongAdversary )
​​    or isMonopolized
​​    or isPoliceLive
​​    or isJurisdictionLive
​​
​​isMediaLive := 
​​(
​​    ( isDismissible(self) and  noStrongAdversary )
​​    or isMonopolized
​​    or isPoliceLive
​​    or isJurisdictionLive
​​) and isSurveillanceLive 
​​
​​を満たせば、いずれ回復する。
​​
​​isFacilitatorsUnsafe propositionをもたらす状況にLivenessを与える方法については、ファシリテーターが裁判官のような独立性の高い役職であるために長い任期と高い給与を与えており、なおかつファシリテーターはランダムに審議に登用されるために、「大多数のファシリテーターが不適格である」という状態からいかに復帰するかという設問に対して解を探せばよいと考えられる。この場合、isEducationLiveおよびisMediaLiveな状態を作り出して一定時間民意が健全になるのを待たねばファシリテーターを新規登用できないので、時間のかかる処理と言える。
​​
​​

​​言論統制への処方箋

​​
​​■ 症状
​​
​​言論統制で民主主義が不健全なときは
​​
​​isSurveillanceUnsafe() := isCorrupted(self) or isCoercedByMediumAdversary(self)