1

我正在学习使用CSPm和FDR对安全协议进行模型检查

我从实现早期论文开始：Breaking and fix the Needham-Schroeder Public-Key Protocol using FDR , Gavin Lowe, TACAS 1996

这是我的代码片段：

-- NSPK Protocol：
-- Msg1 A→B: {Na,A}Pkb
-- Msg2 B→A: {Na,Nb}Pka
-- Msg3 A→B: {Nb}Pkb

-- declare variables：

Initiator = {1..2}    
Responder = {1..2}     
Key = {11..12}          
Nonce = {100..110}     


-- How to declare a data-constructor with the name 'Encrypt' but two different types: Int.Int.Int and Int.Int
channel Msg1, Msg2, Msg3 : Int.Int.Encrypt


-- declare message
MSG1 = {Msg1.a.b.Encrypt.kb.na.a | a <- Initiator, b <- Responder, kb <- Key, na <- Nonce}
MSG2 = {Msg2.b.a.Encrypt.ka.na.nb| a <- Initiator, b <- Responder, ka <- Key, na <- Nonce, nb <- Nonce}
MSG3 = {Msg3.a.b.Encrypt.kb.nb| a <- Initiator, b <- Responder, kb <- Key, nb <- Nonce}
MSG = Union(MSG1, MSG2, MSG3)

FDR 的错误提示是：

/Users/ren/Desktop/Research/Verification/csp_model/nspk.csp:21:36-43:
    Encrypt is not in scope
/Users/ren/Desktop/Research/Verification/csp_model/nspk.csp:25:18-25:
    Encrypt is not in scope
/Users/ren/Desktop/Research/Verification/csp_model/nspk.csp:26:18-25:
    Encrypt is not in scope
/Users/ren/Desktop/Research/Verification/csp_model/nspk.csp:27:18-25:
    Encrypt is not in scope

那么如何声明一个名为“Encrypt”但有两种不同类型的数据构造函数：Int.Int.Int 和 Int.Int？

4

0 回答 0