CODEWITHSUNDEEP
formal-languagesformal-verificationmodel-checkingformal-methodsfdr
Tool Ply
Tool Ply

Reputation: 31

How to declare a data-contructor with same name but different type in CSPm(Communication Sequential Process)

I am learning to model check the security protocol by using CSPm and FDR

I start it from implementing an early paper: Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, Gavin Lowe, TACAS 1996

This is my code snippet:

-- 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)

The error prompt by FDR are:

/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

So how to declare a data-constructor with the name 'Encrypt' but two different types: Int.Int.Int and Int.Int?

Upvotes: 1

Views: 33

Answers (0)

Related Questions