Security and Privacy in Smart Grid Systems: Countermeasure and Formal Verification

在许多分布式计算环境中，需要两个相互不信任的方进行联合计算，通常不会从一方或双方向另一方公开未处理的数据。有时候，“可信第三方”被用于此目的-但立即验证该方的可信度成为一个挑战。密码学世界已经通过安全多方计算的范例解决了这个问题，并通过各种同态加密方案解决了不可信处理器的相关问题。这些在许多情况下是成功的，但意味着一定的管理费用和复杂性。我们提出了一个不同的模型，其中的可信计算技术被用来创建一个有保证的值得信赖的远程实体（TRE）：这也使我们能够开发双工通信，这是很少考虑在上述方法。该项目的主要部分是致力于开发和验证一个基于TRE的解决方案，以应对智能电网中安全和隐私方面的重大而深远的挑战：在该项目的后期，我们考虑将该方法推广到其他类似问题，例如基于动态位置的道路定价。“大想法”是用户可以注册TRE，并且对他们的数据有很高的信心（例如，关于目前用电量的信息）不会落入可能利用它来对付他们的人手中。（例如，计算出房屋何时无人居住）-但是电力公司也可以从他们的角度确信他们接收的数据来自他们的客户之一。如果他们需要减少需求--在极端的情况下，比如远程关闭某人的空调一段时间--他们可以发送一个信号回来，确信它会到达正确的用户，而不知道是哪个客户。这种方法可以推广到许多其他情况：例如，TRE可以帮助计算你在特定时间在特定道路上驾驶的价格，而无需向运输当局透露你的动向。它还可以传递回个性化（但匿名）的指示，说明如何找到一个更好的路线。

In many distributed computing contexts, a need arises for two mutually-distrusting parties to undertake a joint calculation, often without the disclosure of the unprocessed data from one or both sides to the other. Sometimes a 'trusted third party' is used for this purpose - but immediately the verification of the trustworthiness of that party becomes a challenge. The cryptographic world has addressed this through the paradigm of secure multi-party computation - and the related problem of an untrusted processor through various schemes of homomorphic encryption. These are successful in many contexts, but imply certain overheads and complexities. We propose a different model, wherein the technologies of Trusted Computing are used to create an assured Trustworthy Remote Entity (TRE): this also enables us to develop duplex communications, which are seldom considered in the approaches described above. The main part of this project is devoted to developing and verifying a TRE-based solution for the substantial and far-reaching challenges of security and privacy in smart power grids: later in the project we consider the generalization of the approach to other similar problems, such as those in dynamic location-based road pricing. The 'big idea' is that the user can be signed up with a TRE, and have a high degree of confidence that their data (e.g. the information on how much electricity is being used right now) is not going to get in to the hands of someone who might use it against them (e.g. to work out when the home is unoccupied) - but the power company can also have from their side confidence that the data they receive is coming from one of their customers. If they need to reduce demand - in the extreme case by, say, remotely switching off somone's air conditioning unit fora time - they can send a signal back, confident that it will go to the right user, without knowing which customer that is.This approach can be generalised to many other situations: for example, the TRE could help to calculate a price for you to drive on a particular road at a particular time, without disclosing your movements to the transport authority. It could also pass back personalized (but anonymous) instructions on how to find a better route at the time.