Modeling Customer Knowledge and Unauthorized Access in Online Stores
The content discusses how to model a scenario where a malicious customer, Eve, gains unauthorized access to another customer's account by knowing their password. It suggests adding an additional field to represent the knowledge customers have about other customers' passwords. The relationship and implications of such a scenario are explored, highlighting the importance of secure customer data management in online stores.
Uploaded on Sep 24, 2024 | 1 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Eve knows Alices password Roger L. Costello March 24, 2018
Alice and Eve are customers of an online store abstractsig Customer { userId: disj UserId, password: disj Password, token: lone Token } onesig Alice extends Customer {} onesig Eve extends Customer {}
This means each customer has a different user id. Ditto for passwords. abstractsig Customer { userId: disj UserId, password: disj Password, token: lone Token } onesig Alice extends Customer {} onesig Eve extends Customer {}
The store keeps a record of each customer sig StoreRecord { customer: disj Customer, userId: disj UserId, password: disj Password, token: disj Token } { (userId = customer.userId) and (password = customer.password) } fact A_StoreRecord_for_each_customer { all c: Customer | one s: StoreRecord | s.customer = c }
The store provides, among other things, a login function Customers log in with their user id and password and the login function returns a token: fun Login [customerUserId: UserId, customerPassword: Password]: Token { {storeRecord: StoreRecord | (storeRecord.userId = customerUserId) and (storeRecord.password = customerPassword)}.token } The customer uses the token for continued interaction with the store.
Eve is malicious Eve obtains Alice s password and then logs on using Alice s password. How to model this? How to model Eve knowing Alice s password? Answer: add an extra field to Customer to represent the knowledge that a customer has about other customers' passwords: (Acknowledgement: Thanks to Eunsuk Kang for this idea) abstractsig Customer { userId: disj UserId, password: disj Password, token: lone Token, knows: set Password Add this field }
The knowledge that Eve has about passwords is modeled as: Eve.knows = Eve.password + Alice.password
Model one customer logging on as another To model one customer logging on as another, create a predicate (pred), pass it two customers, it logs the first customer on as the second: pred logsOnAs[c1, c2 : Customer] { some p : Password | some Login[c2.userId, p] and p in c1.knows }
Run the model, where Eve knows Alices password run EveLogsOn1 { // Eve knows Alice's password Eve.knows = Eve.password + Alice.password Eve.logsOnAs[Alice] } The Alloy Analyzer generates an instance; Eve successfully logs in as Alice!
run EveLogsOn1 { // Eve knows Alice's password Eve.knows = Eve.password + Alice.password Eve.logsOnAs[Alice] } Equivalent run EveLogsOn1 { // Eve knows Alice's password Eve.knows = Eve.password + Alice.password logsOnAs[Eve, Alice] }
These are also equivalent run EveLogsOn1 { // Eve knows Alice's password Eve.knows = Eve.password + Alice.password Eve.logsOnAs[Alice] } pred EveLogsOn1 { // Eve knows Alice's password Eve.knows = Eve.password + Alice.password Eve.logsOnAs[Alice] } run EveLogsOn1
Run the model, where Eve does not know Alice s password run EveLogsOn2 { // Eve only knows its own password Eve.knows = Eve.password Eve.logsOnAs[Alice] } The Alloy Analyzer does not generate an instance; Eve cannot log in as Alice.
// The store keeps a record for each customer. sig StoreRecord { customer: disj Customer, userId: disj UserId, password: disj Password, token: disj Token } { (userId = customer.userId) and (password = customer.password) } fact A_StoreRecord_for_each_customer { all c: Customer | one s: StoreRecord | s.customer = c } sig UserId, Password, Token {} abstractsig Customer { userId: disj UserId, password: disj Password, token: lone Token, knows: set Password } onesig Alice extends Customer {} onesig Eve extends Customer {} fun Login [customerUserId: UserId, customerPassword: Password]: Token { {storeRecord: StoreRecord | (storeRecord.userId = customerUserId) and (storeRecord.password = customerPassword)}.token } pred logsOnAs[c1, c2 : Customer] { some p : Password | some Login[c2.userId, p] and p in c1.knows } run EveLogsOn1 { // Eve knows Alice's password Eve.knows = Eve.password + Alice.password Eve.logsOnAs[Alice] }