创建具有关系值的签名字段是最佳做法吗？

Question

商店有顾客。每个客户使用其用户ID和密码登录到商店。

我想创建一个Alloy函数（fun），当传递凭据（userID和密码）时，返回拥有这些凭据的客户：

fun customerWithTheseCredentials[userID: UserID, password: Password]: Customer {
    ???
}

我已经说服自己，为了实现这一点，我必须以这种方式声明客户签名：

sig Customer {
    credentials: UserID lone -> lone Password
}

通过这种方式创建签名，我可以这样实现这个功能：

fun customerWithTheseCredentials[userID: UserID, password: Password]: Customer {
    credentials.password.userID
}

如果我以这种方式创建了客户签名：

sig Customer {
    userID: UserID,
    password: Password
}

然后我无法实现该功能。你同意吗？

我坚信，设计具有关系值（例如，credentials: UserID lone -> lone Password）而不是集合（例如，userID: UserID）的签名字段总是更好。你是否也有这种信念？

以下是我的Alloy型号：

sig UserID {}
sig Password {}
sig Customer {
    credentials: UserID lone -> lone Password
} 

fun customerWithTheseCredentials[userID: UserID, password: Password]: Customer {
    credentials.password.userID
}

run {}

fact Every_customer_has_a_different_password_userID {
    // Every customer has a different userID
    no disj c, c': Customer | 
        c.credentials.Password = c'.credentials.Password
    // Every customer has one userID/password pair
    all c: Customer |
        one id: UserID |
            one p: Password |
                c.credentials = id -> p
}

Answer 1

我不同意，您可以使用set comprehension轻松检索具有作为参数给出的id和密码的客户集。

看看这个模型（我冒昧地不假设每个客户都有不同的密码（“password123”只是太常见;-)）。

sig UserID {}
sig Password {}
sig Customer {
    id :disj UserID,
    password: Password
} 

fun customerWithTheseCredentials[userID: UserID, pass: Password]: Customer {
    {c:Customer| c.id=userID and c.password=pass}
}

run {}

Answer 2

好吧，这是我工作的一个区域所以我无法展示一个密码不会被更加小心对待的例子:-)我知道这只是一个例子但人们因为一个不安全的密码模型而死了！ （我喜欢夸张。）作为一个模块化的狂热者，我也认为你应该将认证任务与客户的检索分开，它们本身并不是耦合的，所以应该是分开的。

因此，我的模型是：

sig UserId, PasswordDigest {}
sig Password { digest : disj PasswordDigest }

sig Customer {
    identity : disj UserId
}

one sig Authenticator {
    db : UserId lone -> one PasswordDigest
}

pred authenticate[ id : UserId, password : Password ] {
    password.digest in Authenticator.db[id]
}

fun customerWithTheseCredentials[ userid: UserId, password : Password ] : lone Customer {
    authenticate[ userid, password ] => identity.userid else none
}

run { #Customer = 3 and #Password=3}