问在Bellare模型中，不提供前向保密的具有相互认证的密钥交换协议是否可以被证明是安全的？

EN

这取决于你所说的Bellare-Rogway模型是什么意思？你是说

• BR93：贝拉雷和罗格威最初的AKE模型？
• BR95：他们的后续AKE模式，其中包括三方案件(和其他事情)？
• BPR00：他们的第三个AKE模型(连同Pointcheval)，它还处理基于密码的身份验证的情况？
• 或者是以各种方式扩展或更新上述模型的许多衍生模型中的任何一种，但通常仍被称为"BR-like“模型家族？

如果您的问题中的BR-模型被具体解释为上述前三种模型中的任何一种，那么答案是：

• BR93:前向保密是不需要的。这是因为模型没有给对手任何获得长期密钥的手段。
• BR95:前向保密是必需的。这是因为BR95提供了一个损坏的查询，使对手能够访问用户的内部状态(包括其长期密钥)。
• BPR00:前向保密是必需的。同样，在此模型中，向对手提供了一个查询，使其能够获得用户的长期密钥。

然而，如果你的问题更多的是关于BR-模型作为一个模型家族的想法，所有围绕一些核心建模概念，那么答案是:这取决于。我的意思是BR-模型可以被修改，以适应前向安全协议和非转发安全协议。若要建立前向安全协议的模型，请包括一个损坏的查询(或类似的内容)，该查询允许对手获取长期密钥。若要对非转发安全协议进行建模，请省略此查询(或至少对测试会话进行限制)。

关于您关于新鲜度的问题，这实际上不是关于协议本身，而是一个建模工件。也就是说，根据BR-模型中提供给对手的查询和功能(无论您想要什么样的风格)，总会有一些方法让对手破坏任何协议。这与协议的实际安全性无关，因为这些琐碎的攻击是模型固有的，不对应于任何真实的攻击。因此，引入新鲜度的概念是为了纠正这些琐碎的攻击，说只有“允许”对手进行不被认为是微不足道的攻击。然而，我应该指出，真正弄清楚这些琐碎的攻击是什么，有时可能有点棘手。