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

Question

一家商店有顾客。每个客户都使用他们的用户 ID 和密码登录商店。

我想创建一个 Alloy 函数 (fun)，当传递凭据（用户 ID 和密码）时，returns 拥有这些凭据的客户：

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

我不同意，您可以使用集合理解来轻松检索具有给定 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}

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

Is it best practice to create signature fields with relation values?

alloy