纳迪姆·科贝西：礼仪分析中的恐惧与厌恶
在Symbol Software博客上，我最近发表了一篇文章庆祝Verifpal成立一周年，并详细讨论了Verifpal在过去一年中在三个方面取得的成就：可用性、特性和可靠性。我还讨论了我如何看待Verifpal在协议分析领域的定位，以及它的未来目标，以便人们了解Verifpal的目标是什么(更重要的是，它不打算做什么)。
我在那篇帖子中没有提到的是我在Verifpal工作的第一年有一些相当黑暗的经历。在我生命的早期，有人告诉我，当我所在领域的人对我自己或我所做的工作有偏见或不公平时，我要保持沉默，否则我只会让问题变得更糟。据我所知，这通常只意味着用短期的救济换取确定的长期灾难，因为那些确实逃脱了胡说八道的人只会觉得我的沉默进一步证明了他们的清白，赋予了他们权力，并给了我更大的喘息空间，以便按照他们自己的方式定义我的工作，甚至我自己。
在这篇文章中，我将简要总结一下我在过去一年中使用Verifpal时的一些糟糕经历。把它当作Symbol Software博客上另一篇文章的阴暗面吧，如果你纯粹对更专业的细节感兴趣，这是你应该阅读的。我不认为我应该保持沉默，因为我经常处理来自我的领域的如此多的废话，不断地被那些从未接近被追究责任的人游说。
私营部门：当我要求传票时，Zoom使用Verifpal并公开辱骂。
今年5月，来自Zoom(前身为Keybase)的Max Krohn伸出援手，请求帮助使用Verifpal分析Zoom的新协议。这是我们所有推特DM的PDF文档。在一周的时间里，我帮助麦克斯看了八个Verifpal模型。在一个例子中，为了讨论Verifpal发现的一个缺陷，Max的团队无法理解如何发现和修复，我们进行了一个信号通话(我希望我已经录下了)。这个漏洞是真实的，不明显的，并导致了对协议的攻击。因为Verifpal，Zoom的团队发现并修复了它。
Zoom发表了他们的白皮书，没有提到Verifpal的工作，也没有引用Verifpal，这与Max Krohn在电话中向我承诺的直接相反。另一名Zoom团队成员也证实了这一点：
我与麦克斯进行了第二次信号通话，他再次承诺，一旦麦克斯的一些反馈得到实施，就会引用Verifpal。当然，从那以后，我就再也没有收到过麦克斯或他的团队的回复；不过，我确实收到了利·基斯纳的回复，她当时是Zoom的端到端加密工作的联合负责人，最近受雇于苹果公司，当我问到有关Zoom的端到端加密的问题时，她试图在Twitter上诋毁我的角色：
@kaepora，在你承认并弥补你造成的伤害之前，我不会作为这个社区的一员与你接触。
&；mdash；Lea Kissner(@LeaKissner)2020年6月4日。
Zoom(最大等)中没有其他人。在这一点上有什么要补充的吗。尽管与他们合作了一周多，召开了两次电话会议，研究了八个模型，并使用Verifpal识别了一次实际的非明显攻击，但我从Zoom得到的只是含蓄的威胁，他们发表的任何作品中都没有引用或归功于Verifpal。
最终，过去一年为Verifpal研究提供了非常善意资助的NLnet组织发布了一篇帖子，讨论了Verifpal对Zoom的贡献-我没有从Zoom那里获得任何关于该帖子的意见，而是担心我们会一直收到他们律师的意见。
学术界：该领域的研究人员在评估Verifpal时公开表现出个人偏见，并受到其他研究人员的辩护。
几周前，我在一个致力于正式验证研究的邮件列表上发了一封电子邮件，以一种滑稽的方式兜售Verifpal，并分享了我们在第一年取得的成就。最古老的协议分析工具之一的首席开发人员(有20多年的历史)以以下方式回应：
研究人员给Verifpal的分析提供了一个错误的、不起作用的“反例”(即，一个应该显示不正确的Verifpal分析的模型，但没有)，这证明他们从未读过我们的论文或手册，因为我们的论文中提到的那个特定的反例是Verifpal没有解决的。我准确地引用了Verifpal论文中的哪个章节讨论了这一点。
研究人员毫无根据地指责Verifpal项目将他们的名字用于本质上的营销目的，并把话塞进他们的嘴里，以出售Verifpal，
研究人员谴责我的开发方法，同时宣扬他们的方法是唯一客观正确的方法。(我后来指出，他们的方法在比Verifpal长五倍的开发周期内产生了比Verifpal更令人讨厌的软件。)
研究人员没有看过我们最近的Coq形式语义和被动攻击者分析工作(从他们对工作含义的反复曲解就可以证明)，
最后，这位研究人员将所有这些都建立在自己的基础上，以便公开宣布他们对我甚至允许自己成为协议分析社区的一员感到失望(我在这里转述是为了不透露这位研究人员的身份，因为他们最初的措辞会)。要澄清的是：研究人员利用他们几十年的经验，基于对我在Verifpal上的工作的一系列完全误解和故意无知，本质上试图将我赶出这个领域。一年后。
当我指出“反例”不是反例，而且这位研究人员毫无根据地宣扬他们的方法是唯一正确的方法，并且为了攻击我个人而忽略了我们最近所有的可靠性/可靠性工作时，我确保将这位研究人员所说的话称为“胡说八道”，因为，嗯，它是，我觉得他们需要听到它。
然后，他们的两名合作研究人员私下给我发了一封电子邮件，语气中带着惊慌失措的紧迫感，向我解释了以下几点：
第一个声称我这样做是因为我是黎巴嫩移民，由于我一定在黎巴嫩经历过创伤，甚至没有谈到研究讨论的实质内容。我希望我是在开玩笑。这是最低级的种族主义，我也永远不会得到道歉。
第二个人声称已经与研究人员进行了讨论，但他们似乎“太紧张”，无法收回他们所做的任何虚假声明，严重暗示我应该收拾行李离开，因为我不会得到任何形式的撤回或道歉。
这两位合作研究人员都大声宣布效忠最初的研究人员，并对我选择指出最初研究人员写的所有废话的方式表示极大的震惊和怀疑。不要紧的是，他们已经清楚地表明，他们对我的工作抱有偏见，没有对其进行评估就得出了结论。没关系，他们的同事们正在诉诸种族主义的比喻来为他们辩护。根据该组织的说法，最令人震惊的问题是，我敢在一封电子邮件中称所有这些都是“胡说八道”，否则这就是对研究人员错误的批评的完全正确的逐点抨击，并为我的工作辩护。这三位研究人员都没有对我为自己的工作辩护或对任何不公平的批评置若罔闻。
所以，我收拾好行李离开了。编辑：一些读者想知道为什么我要在这里匿名，不像我写这篇文章的Zoom部分的方式。原因是这些研究人员中有一些是我知道的有焦虑问题的人，我不想在公共场合不必要地点名给他们带来麻烦。
可悲的是，这位研究人员之前在Verifpal中发现了有效的错误，而我已经修复了这些错误。有趣的是，了解到我本以为是出于善意发现的错误，结果很可能是我出于愤怒而被派来的错误，最有可能的是一种阻碍我在该领域进一步工作的方法。
在另一个单独的例子中，在我在Twitter上错误地声称Verifpal可能是第一个完成多线程分析的协议分析工具后，一名研究人员公开指责我，他正在开发另一个无关的协议分析工具。事实证明那不是真的，我匆忙改正错误并道歉。后来我发现，这位研究人员除了在Twitter上礼貌地向我指出这一点外，还花了几个小时的时间在一个私人的Slake频道上贬低Verifpal，侮辱我个人，考虑到我完全愿意去公开纠正，这很奇怪。
上面提到的所有研究人员都是我在工作中大量引用、感谢并列举为灵感来源的人。我把它作为一个练习留给读者去弄清楚，为什么他们觉得最终应该吐露自己的肚子，揭露他们隐瞒了这么长时间的所有隐藏的偏见。
在以前的项目和工作中没有这样做之后，我决定在Verifpal中开始公开记录类似的情况。我后悔没有这样做，因为这似乎鼓励人们辱骂和利用他们所在领域中资历较低、声誉较差的人。
我不期待未来出现任何虐待事件，但如果出现这种情况，我确实期待在类似的帖子中记录这些事件。