xDECAF 😆☕

Appearance

📊 Model: (InformationFlow-PrivateTaxi-no-violation) ​

Available Online

This model is available to view using the online editor!

Open In Online Editor

🔗 Link to Original Paper/Article ​

View SourceOpen Example Model in Example Models Bundle

📝 Short Description ​

The case is about a private taxi service that connects riders and drivers.

🔤 Abbreviations ​

  • CalcDistanceService: Service for calculating distance.

📖 Extensive Description ​

Riders and Drivers have user accounts at the PrivateTaxiService. Riders and Drivers calculate routes to their destinations based on their locations. They encrypt their route for a CalcDistanceService and send it to the PrivateTaxiService. The PrivateTaxiService uses the CalcDistanceService to determine the proximity of routes (calc_proximity). The Rider selects one of the matches (find_match and select_match) and encrypts the route for the Driver. Drivers decrypt the route (decrypt_route) to navigate to the Rider and bring him/her to the destination.

🏷️ Label Description ​

🗂️ Data Labels: ​

  • PublicKeyOf: This characteristic type describes that the data flow contains a public key of an Entity.
  • PrivateKeyOf: This characteristic type describes that the data flow contains a private key of an Entity.
  • DecryptableBy: This characteristic type describes that a data item can be decrypted with any of the private keys of the specified entities.
  • CriticalDataType: This characteristic type marks whether a flow contains the critical data type RouteDataType or ContactInformation.
  • EncryptedContent: This characteristic type marks that an encrypted flow contains either the critical data RouteDataType or ContactInformation.

🏷️ Node Labels: ​

  • Entity: This designates a node to be part of an Entity. These are: Driver, Rider, CalcDistanceService or PrivateTaxiService.

⚠️ Constraints ​

NeverKnowRoutes ​

The Private Taxi Service must never get to know the routes of drivers or riders:

  • NeverKnowRoutes: CriticalDataType.RouteDataType neverFlows vertex Entity.PrivateTaxi

NeverKnowContactInfo ​

The Distance Calculation Service must never get to know contact information of drivers or riders:

  • NeverKnowContactInfo: CriticalDataType.ContactInformation neverFlows vertex Entity.CalcDistanceService

🚨 Violations ​

None.