Bellare和Rogaway在1993年和1995年分别给出了两个可证明安全性的两方和三方会话密钥分配协议。协议本身很简单，其意义在于首次建立了会话密钥分配协议的形式化安全模型，称为BR安全模型。这是一种现实模型，即协议只定义在现实世界中，而安全性是通过会话密钥与某随机数的计算不可区分性来定义的（基本方法是使会话密钥和一个敌手易于得到的某伪随机数紧密联系）。

协议定义：P=（Π，Ψ，LL），这是一个多项式时间可计算的三元组函数，Π描述诚实方的行为，Ψ描述S的行为，LL描述用户主密钥的初始分布。

协议参与方：I={0，1，2，…，N}（0代表可信中心S），敌手E。协议参与者的所有预言机只能被动地回答攻击者E对它们进行的各种查询（Query），预言机之间并不进行直接的通信。也就是说，模型中至少存在一个良性（Benign）攻击者，它唯一的动作就是忠实地传递预言机之间的协议消息。

E所能发起的攻击形式化为5种Oracle询问：（SendPlayer，i，j，s，x）；（SendS，i，j，s，x）；（Reveal，i，j，s）；（Corrupt，i，K）；（Test，i，j，s）。前4种Oracle询问可以是多项式次，形式化了E所能发动的各种攻击，如窃听、已知会话密钥、重放、收买某合法方等攻击，（Test，i，j，s）则只能询问一次，是为了定义安全性而提供的“测试”Oracle。

•（SendPlayer，i，j，s，x）：E可以向预言机Πsi，j发送消息。该预言机按照协议规范应答一个响应消息。(www.daowen.com)

•（SendS，i，j，s，x）：E可以向预言机ΨSi，j发送消息。该预言机按照协议规范应答一个响应消息。

•（Corrupt，i，K）：此查询要求被询问的协议参与者返回它拥有的长期私钥。相应地，回答过Corrupt查询的实体的状态被称为“已腐化”（Corrupted）。

•（Reveal，i，j，s）：收到此查询的预言机返回它协商得到的会话密钥。如果该预言机的状态还不是“已接受”（Accepted），那么它返回一个符号⊥表示终止。

•（Test，i，j，s）：E可以向一个预言机发出Test查询。E将收到该预言机所拥有的会话密钥或者一个随机值。具体来说，该预言机通过投掷一枚公平硬币b∈R{0，1}来回答此查询。若投币结果为0，那么它返回自己协商获得的会话密钥；否则，它返回会话密钥空间{0，1}k上的一个随机值，这里，k表示会话密钥的比特长度。