Hua Shen

Daijie Sun

Lan Zhao

Mingwu Zhang
email: mzhang@hbut.edu.cn

A Fair (t, n)-threshold Secret Sharing Scheme with Efficient Cheater Identifying

Keywords: Secret sharing, Cheater identification, Fairness, Attack model

The fairness of secret sharing guarantees that, if either participant obtains the secret, other participants obtain too. The fairness can be threatened by cheaters who was hidden in the participants. To efficiently and accurately identify cheaters with guaranteeing fairness, this paper proposes a fair (t, n)-threshold secret sharing scheme with an efficient cheater identifying ability. The scheme consists of three protocols which correspond to the secret distribution phase, secret reconstruction phase, and cheater identification phase respectively. The scheme's secret distribution strategy enables the secret reconstruction protocol to detect the occurrence of cheating and trigger the execution of the cheater identification protocol to accurately locate cheaters. Moreover, we prove that the scheme is fair and secure, and show that the cheater identification algorithm has higher efficiency by comparing with other schemes.

Introduction

In the reconstruction phase of a (t, n)-threshold secret sharing scheme, dishonest participants can reconstruct the real secret because of receiving the valid secret shares. It's unfair for honest participants that they gain the wrong secret because of accepting the invalid secret shares [START_REF] Zhang | Obfuscating EVES algorithm and its application in fair electronic transactions in public cloud systems[END_REF]. To address this issue, many researchers have come up with their solutions. Laih and Lee [START_REF] Laih | V-fairness (t, n) secret sharing scheme[END_REF] proposed a vfair (t, n)-threshold secret sharing scheme, in which all participants do not have to show their secret shares simultaneously to recover the secret with the same probability, even if there are v(< t/2) dishonest participants. [START_REF] Lee | A simple (v, t, n)-fairness secret sharing scheme with one shadow for each participant[END_REF] and [START_REF] Yang | An efficient v-fairness (t, n) threshold secret sharing scheme[END_REF] further improved Laih scheme [START_REF] Laih | V-fairness (t, n) secret sharing scheme[END_REF]. In 2003, Tian [START_REF] Tian | Fair (t, n) threshold secret sharing scheme[END_REF] utilized the consistency of secret shares to detect attackers, and constructed a fair (t, n)-threshold scheme with the help of the schemes of Tompa and Woll [START_REF] Tompa | How to share a secret with cheaters[END_REF]. Harn and Lin [START_REF] Harn | Detection and identification of cheaters in (t, n) secret sharing scheme[END_REF] also used the consistency of secret share to design an algorithm to detect cheating behavior and identify cheaters. In 2014, Harn [START_REF] Harn | Comments on'fair (t, n) threshold secret sharing scheme[END_REF] pointed out that the research on asynchronous attack in scheme [START_REF] Tian | Fair (t, n) threshold secret sharing scheme[END_REF] was incorrect. In 2015, Harn [START_REF] Harn | Fair secret reconstruction in (t, n) secret sharing[END_REF] proposed a scheme that can resist asynchronous attacks of external attackers and internal attackers. In 2016, Liu [START_REF] Liu | Linear (k, n) secret sharing scheme with cheating detection[END_REF] presented a Linear (t, n)-threshold secret sharing scheme in which there is only one honest participant can detect cheaters. Lin [START_REF] Lin | Distributed secret sharing approach with cheater prevention based on qr code[END_REF] constructed a secret sharing scheme which focuses on preventing cheating behavior rather than cheating detection. With the same purpose, in 2018 Liu [START_REF] Liu | k, n) secret image sharing scheme capable of cheating detection[END_REF] proposed a (t, n)-threshold secret image sharing scheme. In order to improve the efficiency of the verifiable secret sharing scheme, Mashhadi [START_REF] Mashhadi | Provably secure verifiable multi-stage secret sharing scheme based on monotone span program[END_REF] and Cafaro [START_REF] Cafaro | Space-efficient verifiable secret sharing using polynomial interpolation[END_REF] put forward their schemes respectively, but none of their schemes are unconditionally safe. In 2018, Liu and Yang [START_REF] Liu | Cheating identifiable secret sharing scheme using symmetric bivariate polynomial[END_REF] proposed a cheating identifiable secret sharing scheme by using the symmetric bivariate polynomial, but the scheme does not achieve fairness requirement of secret sharing.

In order to not only identify deception behavior but also efficiently and accurately locate cheaters, this paper propose a fair (t, n)-threshold secret sharing scheme which realizes the fairness through Distribution protocol and Reconstruction protocol, and achieves the efficiently cheaters identification through Cheater identification protocol. Moreover, the presented scheme is unconditional security because of not depending on any security assumptions, and is fair and secure based on four attack models.

The remainder of this paper is organized as follows. We introduce some preliminaries, in Section 2. In Section 3, we present a fair (t, n)-threshold secret sharing scheme with an efficient cheater identifying algorithm. In Section 4, we describe the fairness and security of the proposed scheme, followed by the performance analysis in Section 5. Finally, we conclude this paper.

Preliminaries

In this section, we briefly recall some fundamental backgrounds which are used in our scheme and then introduce the attack models of our scheme.

Shamir's (t, n)-secret sharing scheme

Shamir's (t, n)-threshold secret sharing scheme [START_REF] Shamir | How to share a secret[END_REF] is based on Lagrange interpolating polynomial, in which there are n participants P={P 1 ,• • • ,P n }, and a mutually trusted dealer D. The scheme consist of two algorithms:

-Distribution algorithm: The dealer D first randomly generates a polynomial:

f (x) = a 0 + a 1 x + a 2 x 2 + • • • + a t-1 x t-1
, in which the secret is s=a 0 and all the other coefficients a 1 , • • • , a t-1 are chosen from a finite field F, and then D computes the secret share s i = f (i) and sends it to the participant P i , where i = 1, 2, • • • , n. -Reconstruction algorithm: In the reconstruction phase, at least t participants submit their secret shares, the secret s can be reconstructed by calculating the Lagrangian interpolation polynomial through these secret shares.

Definitions of Consistency and Fairness

Definition 1. ( consistency): In a (t, n)-threshold secret sharing scheme, suppose there are m (m ≥ t) participants reconstruct the secret. The m shares are consistent if any t shares in them can reconstruct the same secret.

To check whether m shares are consistent or not, we only need to sequentially execute three steps as follows [START_REF] Tian | Fair (t, n) threshold secret sharing scheme[END_REF]. (i) Reconstruct a polynomial g(x) using any t shares of the m secret shares. (ii) Check whether the degree of g(x) is t -1 or not. (iii) Check whether the remainder m -t secret shares satisfy g(x) or not. If (ii) and (iii) are satisfied, we can conclude that the m shares are consistent.

Definition 2. ( fairness): A (t, n)-threshold secret sharing scheme is fair if it can guarantees that either each participant who takes part in reconstructing the secret obtains the same secret, or knows nothing about the mystery.

Not difficult to find if the m secret shares are consistent, the corresponding scheme is fair.

Attack models

The aim of our scheme is holding the fairness and secure under the following four attack models. :

-Non-cooperative attack with synchronisation (NCAS): All participants submit the secret shares simultaneously, and that there are no cooperations between dishonest parties. -Non-cooperative attack with asynchronisation (NCAAS): All participants present secret shares successfully and that there are no cooperations between dishonest parties. -Collusion attack with synchronisation (CAS): The malicious parties modify their secret shares to deceive the honest parties. We assume that all participants submit their secret shares at the same time. Under this assumption, only when the number of malicious parties is more extensive than or equal to the threshold value t, can the malicious parties successfully deceive the honest parties. -Collusion attack with asynchronisation (CAAS): The dishonest parties collaboratively modify their secret shares to deceive the honest parties. The participants asynchronously release their secret shares. The best option for dishonest participants is to submit their accordingly modified secret shares after all honest participants have submitted their secret shares.

Our schemes

In this section, we introduce our fair (t, n)-threshold secret sharing scheme which consists of three algorithms: distribution algorithm, reconstruction algorithm, and cheater identification algorithm.

Distribution

The dealer D wants to share a secret s among n participants

P = {P 1 , • • • , P n }.
D first randomly constructs an identifier sequence {a 1 , a 2 , • • • , a v } from Z q , and q is big prime integer. The sequence must satisfy:

a 1 > a 2 > • • • > a l-1 > a l+1 > • • • > a v > a l where l ∈ [1, v]
is randomly determined by D, and a l is related to finally recover s. And then, based on the sequence, D generates v random polynomials through which D calculates the secret share s i = (s i1 , • • • , s iv ) for the ith participant. The distribution protocol is shown as:

Distribution protocol

Input: the secret s, the parameter v.

Output: the secret shares

s 1 , s 2 , • • • , s n . 1. Randomly pick an integer l ∈ [1, v]; 2. Generate a 1 > a 2 > • • • > a l-1 > a l+1 > • • • > a v > a l ;
3. Construct v polynomials of (t -1)-degree, like as follows:

f k (x) = a k + a k,1 x + a k,2 x 2 + • • • + a k,t-1 x t-1 mod Z q , where k = 1, • • • , v, and a k,1 , • • • , a k,t-1 are randomly picked from Z q ; 4. Calculate d to satisfy: s = a l • d; 5. Generate the secret share of ith (i = 1, • • • , n) participant by computing s i = (s i1 , s i2 , • • • , s iv ) = (f 1 (i), f 2 (i), • • • , f v (i)).

Reconstruction

Suppose that m(≥ t) participants R = {P 1 , • • • , P m } cooperate to reconstruct s. Denoted by P -i = R/P i . The reconstruction protocol is shown below:

Reconstruction protocol Input: m(m ≥ t) secret shares {s 1 , s 2 , • • • , s m }.
Output: the set of cheaters A and the secret s.

1. 1th round: P i sends s i1 to P -i , and then performs Receive share(k).

2. kth (k from 2 to v) round: If P i receives all (k -1)th items of secret shares sent by P -i , then uses {s

1 k-1 , s 2 k-1 , • • • , s m k-1 } to calculate a Lagrange interpolating polynomial f k-1 (x). If f k-1 (x) is t -1 degree
= f k (0). If a k > a k-1
, then D sends d to all participants in P/A, and these participants can calculate s = a k-1 • d, and then the protocol is terminated; otherwise, all participants in P/A send the (k + 1)-th items of secret shares.

Cheater identification

To identify the participants who input fake shares, We use a mark vector represents a kind of choice of selecting t participants from m participants, so there are

u = m t mark vectors, denoted by C 1 , • • • , C u .
Each mark vector consists of m items, of which the value is 0 or 1, denoted by

C j = (c j1 , • • • , c jm ), j = 1, 2, • • • , u.
Therefore, each mark vector includes t 1 s and m -t 0 s.

Cheater identification protocol

Input: m, t, k, {s

1 k , s 2 k , • • • , s m k }.
Output: the set of cheaters A.

All the m reconstruction participants do:

1. Generate u mark vectors C 1 , C 2 , • • • , C u . 2. Based on the mark vector C j (j = 1, 2, • • • , u) (that is, based on S k = {s i k |c j i = 1} (i = 1, 2, • • • , m))
, each participant yields the Lagrange interpolating polynomial f j k (x). Therefor, each participant can obtain

f 1 k (x), f 2 k (x), • • • , f u k (x). 3. According to f 1 k (x), f 2 k (x), • • • , f u k (x), each participant can obtain u val- ues of the identifier a k , that is a 1 k = f 1 k (0), a 2 k = f 2 k (0), • • • , a u k = f u k (0)
. These values might different or the same. Find the most frequently occurring value in them, the value is the value of a k . 4. And then extract the corresponding mark vectors from

{C 1 , • • • , C u }.
Use C succ denote the set of these corresponding mark vectors. 5. Perform Logic Or operation on C succ , the participants corresponding to the items whose values are 0 in the result mark vector are cheaters, and then add these participants to A, finally return A.

Security and correctness analysis

Theorem 1. In our proposed scheme, the probability that each participant successfully guesses the secret s is 1/v.

Proof. The dealer D hides the secret s into the polynomial f l (x), where l ∈ [1, v] is randomly chosen by D, therefore, the participants successfully guess the value of l with the probability 1/v.

P = {P 1 , • • • , P m } (t ≤ m ≤ n
) denotes all participants who take part in the secret reconstruction phase, P I = {P i1 , • • • , P iα } ⊆ P denotes the set of cheaters in P, P -I = P/P I denotes the set of honest participants in P.

Theorem 2. Under non-cooperative attack with synchronisation (NCAS), when m > t, our scheme is secure and fair.

Proof. NCAS assumes that all participants present shares at the same time and that there is no cooperation between cheaters. Suppose that in the k-round reconstruction stage, the cheaters in P I send invalid secret shares. Since there is no cooperation between the cheaters, their invalid secret shares can only be random numbers in Z q . When m > t, these secret shares could not pass the consistency test, and the attack is immediately detected. In order to restore s, the attackers in P I need to guess in which polynomial s is hidden and which honest participants are involved. According to Theorem 1, the maximum successful probability is 1/v. If v is large enough, the probability can be ignored. Therefore, under non-cooperative attack, when m > t, our scheme is secure and fair. Theorem 3. Under non-cooperative attack with asynchronisation (NCAAS), when {(m -α < t -1)∩(m > t)}∪{m -α≥t + 1}, our scheme is secure and fair.

Proof. NCAAS assumes that all participants present shared shares successively without cooperation between attackers. A cheater' ideal attack is to show the secret share at the end, because he can obtain all the shares before others. When m -α ≥ t + 1, that is, there are no less than t + 1 honest participants, who show the secret shares firstly. Therefore, the attackers can reconstruct the correct polynomial f k (x) (suppose in k-round) based on t real secret shares, and then obtain the a k . The attackers can show the real secret shares in the first l rounds and show a fake secret share in (l + 1)th round. However, the fake secret share cannot pass the consistency test, and the attack behavior can be detected, which trigger the execution of cheater identification algorithm. The right identifier a l+1 can be reconstructed based on the m -α real secret shares, because m -α t > 1, the a l+1 is correct identifier which can be used to identify the attackers, therefore, the attackers could not gain d from the dealer to obtain s. When m -α < t + 1, for an attacker, even if he finally shows his secret share, he can only obtain at most t -1 real secret shares, so he can not reconstruct any t -1-degree polynomial, as a result he can not recover s. In order to detect attacks, m should greater than t. In conclusion, when {(m -α < t -1)∩(m > t)}∪{m -α≥t + 1}, the proposed scheme is secure and fair.

Theorem 4. Under collusion attack with synchronisation (CAS), when {(α < t) ∩ (m > t)} ∪ {(α ≥ t) ∩ (m -α > α + t -1)}, our scheme is secure and fair.

Proof. CAS assumes that all participants present secret shares simultaneously and that multiple attackers conspire to attack the scheme. Suppose there are α cheaters in k-round. (i) When α ≥ t, if the number of honest participants is less than t, that is, m -α < t, then cheaters can cooperate to forge a set of invalid secret shares which can pass consistency detection. The specific process is as follows: Cheaters first use their secret shares to recover an interpolation polynomial, then utilize the polynomial to calculate the secret shares held by other honest participants, and then generate their false secret shares based on the secret shares of other honest participants. For example,

α = t, m -α = t -1, m = 2t -1, use {P 1 , • • • , P t-
, • • • , s 2t-1 l+1 }.
Finally, the secret shares shown by all participants as follows:

{s 1 l+1 , s 2 l+1 , • • • , s t-1 l+1 , s t l+1 , s t+1 l+1 , • • • , s 2t-1 l+1 }.
These m secret shares can pass consistency detection when m-α ≥ t. The secret shares forged by the above method in (l +1)th round cannot pass consistency detection. By executing the identification algorithm, m real secret shares can used to reconstruct the correct identifier a l+1 at m -α t times, while t-1 real secret shares and an invalid secret share can be utilized to reconstruct a wrong identifier a l+1 at α + t -1 t times. Therefore, we have

m -α t > α + t -1 t .
That is, m -α > α + t -1, under this condition, the invalid secret shares can be detected, and cheaters cannot obtain d from the dealer and recover s. But the honest participants can gain d and reconstruct s. (ii) If α < t, these α cheaters can not use their real secret shares to forge the invalid secret shares that can pass the consistency detection. When m > t, this attack can not pass the consistency detection. If cheaters want to reconstruct s, they can only guess the value of l, the probability of successfully guessing is only 1/v. From what has been discussed above, when {(α < t) ∩ (m > t)} ∪ {(α ≥ t) ∩ (m -α > α + t -1)}, our scheme is secure and fair.

Theorem 5. Under collusion attack with asynchronisation (CAAS), when mα > α + t -1, our scheme is secure and fair.

Proof. CAAS assumes that all participants present secret shares successively and that multiple cheaters conspire to attack the scheme. For cheaters, the ideal mode of attack is to present the secret shares at the end, so that they can obtain the real secret shares presented by previous honest participants. When m -α ≥ t, there are not less than t honest participants, who first show the secret shares. Attackers use t -1 real secret shares (according to the method of Theorem 4) to forge α invalid secret shares. Because m -α ≥ t, these invalid secret shares cannot pass consistency detection. By executing the identification algorithm, m -α real secret shares can be used to recover the correct identifier a l+1 m -α t times, while t -1 real secret shares and an invalid secret share can be utilized to reconstruct a wrong identifier a l+1 α + t -1 t times. Therefore, we have

m -α t > α + t -1 t .
Concretely, under m -α > α + t -1, these invalid secret shares can be detected, and cheaters cannot gain d from the dealer and reconstruct s. But the honest participants can obtain d and recover s. Therefore, when m -α > α + t -1, the proposed scheme is secure and fair.

Theorem 6. Under the conditions mentioned above, our cheater identification algorithm is correct.

Proof. The key to prove the correctness of the cheater identification protocol is to prove the most frequently occurring value in {a

1 k = f 1 k (0), • • • , a u k = f u k (
0)} is the correct value of a k . In the cheater identification protocol, interpolating polynomials are reconstructed only based on t secret shares, therefore, only when the t secret shares are real can the correct value of a k be recovered. To guarantee the most frequently occurring value in {a

1 k = f 1 k (0), • • • , a u k = f u k (
0)} is the correct value of a k , the following condition must be satisfied:

m -α t > 1 2 m t .
We have,

(m -α)! (m -α -t)!t! > 1 2 • m! (m -t)!t! = 1 2 • (m -α)!α! (m -t)!t! ⇒ (m -α)! (m -α -t)! > 1 2 • (m -α)!α! (m -t)! = 1 2 • (m -α)! (m -α -t)!
Since the inequality is always true, our cheater identification algorithm is correct.

Performance

The following two examples are given to respectively calculate the maximum number of attackers α max under the four types of attack models. Taking (7, n) threshold scheme as an example, assuming m = 9 and m = 11, where m is the number of participants who take part in the secret reconstruction phase. Under NCAS, according to Theorem 2, when m > t our scheme is secure and fair, so α max = 9. Similarly, under NCAAS, according to Theorem 3, when {(m -α < t -1)∩(m > t)}∪{m -α≥t + 1} our scheme is secure and fair, which means α max = 9. From the analysis of Theorem 4, Under CAS, when {(α < t) ∩ (m > t)} ∪ {(α ≥ t) ∩ (m -α > α + t -1)} the proposed scheme is safe and fair, so α max = 6. According to the analysis of Theorem 5, Under CAAS, our scheme can defend at most 1 cheaters, as shown Table 1. Based on a similar analysis process, when m = 11, the values of α max are shown as in Table 1. Different from Tian and Peng's [START_REF] Tian | A practical publicly verifiable secret sharing scheme based on bilinear pairing[END_REF] scheme, our scheme does not depend on any security assumptions, it is a unconditional security scheme. Compared to Tian's [START_REF] Tian | Fair (t, n) threshold secret sharing scheme[END_REF], Harn's [START_REF] Harn | Comments on'fair (t, n) threshold secret sharing scheme[END_REF], Harn-Lin's [START_REF] Harn | Detection and identification of cheaters in (t, n) secret sharing scheme[END_REF] and Liu-Yang's [START_REF] Liu | Cheating identifiable secret sharing scheme using symmetric bivariate polynomial[END_REF] secret sharing schemes, our scheme achieves fairness but they do not have, as shown in Table 2.

In [START_REF] Harn | Detection and identification of cheaters in (t, n) secret sharing scheme[END_REF], Harn and Lin proposed a secret sharing scheme that can identify cheaters. In their scheme, the correct secret needs to be confirmed and the secret share of each participant needs to be verified. In our scheme, we removed the process of validating each participant's secret share but achieves the same function of [START_REF] Harn | Detection and identification of cheaters in (t, n) secret sharing scheme[END_REF]. Therefore, our scheme has higher operating efficiency than [START_REF] Harn | Detection and identification of cheaters in (t, n) secret sharing scheme[END_REF].

Conclusion

In this paper, we study the cheater identification issue and the fairness problem in the reconstruction phase of secret sharing, and propose a fair (t, n) secret sharing scheme including a efficient cheater identification algorithm. By comparing with the existing verifiable secret sharing schemes, it can be found that our scheme achieves fairness. Compared with the fair secret sharing scheme, our cheater identification algorithm has a lower computational complexity. Moreover, we analyzed the security of our proposed scheme under four different attack models.

  , then all participants send the kth items of their secret shares and then perform Receive share(k). Otherwise, all participants utilize the cheater identification protocol and obtain the set A. If |P/A| ≥ t, then all participants ∈ P/A send the kth items of their secret shares and performs Receive share(k); otherwise, protocol is terminated.Procedure Receive share(k): Receiving the kth item of secret share 1. When P i has received all kth items of secret shares sent by P -i , he utilizes all these items {s 1 k , s 2 k , • • • , s m k } to compute the Lagrange interpolating polynomial f k (x). If the degree of f k (x) is t -1, then P i performs step (b). Otherwise, all participants invoke the cheater identification protocol to identify the cheaters, and put them into the cheaters' set A. If |P/A| ≥ t, then the protocol turns to step b; otherwise, it is terminated. 2. Calculate the identifier by using the secret share sent by all participants in P/A, a k

  1 } denote honest participants, use {P t , P t+1 , • • • , P 2t-1 } denote cheaters. Cheaters can use their true secret share {s t k , s t+1 k , • • • , s 2t-1 k } to calculate the interpolation polynomial f k (x), so they can show the true secret shares in the first l rounds, and in (l + 1)th round, they can use f l+1 (x) to obtain other honest participants' secret shares {s 1 l+1 , • • • , s t-1 l+1 }, and calculate another (t-1)-degree polynomial f l+1 (x) by using secret shares {s 1 l+1 , s 2 l+1 , • • • , s t-1 l+1 } and a random value s t l+1 . And then, cheaters use f l+1 (x) to calculate t-1 invalid secret shares {s t l+1 , s t+1 l+1

Table 1 .

 1 (7,n)-threshold scheme, m = 9 or m = 11

	Attack model	Conditions	αmax	αmax
			(m = 9) (m = 11)
	NCAS	m > t	9	11
	NCAAS	{(m -α < t -1)∩(m > t)}∪{m -α≥t + 1}	9	11
	CAS	{(α < t) ∩ (m > t)} ∪ {(α ≥ t) ∩ (m -α > α + t -1)}	6	6
	CAAS	m -α > α + t -1	1	2

Supported by the National Natural Science Foundation of China (61702168, 61672010), Hubei Provincial Department of Education Key Project (D20181402), the open research project of Hubei Key Laboratory of Intelligent Geo-Information Processing (KLIGIP-2017A11).

Table 2. Security comparison Scheme Tian[6] Harn-Lin[8] Liu-Yang[17] Tian-Peng[18] ours Security assumption no no no ECDLP no Fairness no no no no yes


Sebastian Mödersheim

Anders Schlichtkrull

Georg Wagner
email: gwagner@iaik.tugraz.at

Stefan More
email: smore@iaik.tugraz.at

Lukas Alber
email: lalber@iaik.tugraz.at

TPL: A Trust Policy Language

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

We introduce TPL -not only a Trust Policy Language but also a trust management system geared to support and integrate today's existing trust schemes to create a trust infrastructure. A trust management system is a system that helps companies and organizations to automatically process trust decisions about electronic transactions they receive. TPL helps to specify and automatically implement a company's business policy for trust decisions.

TPL is designed in the context of the LIGHT est project that aims to create a Lightweight Infrastructure for Global Heterogeneous Trust management in support of an open Ecosystem of Stakeholders and Trust schemes. The idea is that there are a number of trust schemes like the European eIDAS, but no scheme on which the whole world agrees on. To achieve this TPL supports different formats of electronic documents and transactions. It also allows authorities behind a trust scheme to define translations from other schemes. Translations can be automatically processed, but are only "recommendations": a policy designer can decide whether to accept trust translations. TPL also supports trust delegations.

TPL has simple, clear and precise semantics as first-order clauses interpreted with respect to an environment representing TPL's interaction with the outside world. Despite the simplicity, the ATV's implementation -the Automated Trust Verifier connecting parsers and server lookups with logical evaluation -is complex. A concern is the reliability of trust decisions, i.e., that bugs in a component cannot lead to false positives. Thus TPL's architecture allows for boiling down this problem to the correctness of isolated components. For the logical decision of whether a decision follows from a policy, we offer a reliable logical verification: we feed the decision and policy, together with a logical representation of all documents and which signatures have been verified with respect to which keys, into the automatic theorem prover RP X [START_REF] Schlichtkrull | A verified prover based on ordered resolution[END_REF][START_REF] Schlichtkrull | A verified functional implementation of Bachmair and Ganzinger's ordered resolution prover[END_REF][START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's ordered resolution prover[END_REF][START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's ordered resolution prover[END_REF] to check that the given decision logically follows from the policy and the given documents. This is a double check by a very special "extra pair of eyes": the correctness of RP X was formally proven using the theorem prover Isabelle. When a positive policy decision of the ATV is verified by RP X , we believe, it is virtually impossible that it could be due to a flawed implementation of TPL's semantics.

In TPL's design we focused on three key qualities. The first is modularity in order to support arbitrary attribute-value based data formats. To connect a new data format to the ATV infrastructure, one only needs to write a parser from the concrete format to an abstract syntax representation. Thus there is no need to "adjust the world" -our system easily fits with existing schemes.

The second quality is declarativity and expressive power. TPL is inspired by Prolog (without the cut operator and negation) and thus policies are always formulated positively, i.e., under which conditions the policy is fulfilled. Nonetheless, TPL is Turing complete, i.e., every computable policy can be expressed; this programming aspect, in particular, allows generating templates for the most common kinds of policies. LIGHT est has also produced graphical interfaces to TPL for users with different degrees of experience with policy specification [START_REF] Mödersheim | GTPL: A Graphical Trust Policy Language[END_REF][START_REF] Weinhardt | Usability of policy authoring tools: A layered approach[END_REF].

The third quality is formal precision and accountability. Since we expect to deal with transactions of substantial value, it is crucial that there are no undefined corner cases or bugs in the implementation. It should be possible for an independent third party to easily review a decision. An example of such a review is the mentioned verification with RP X . Another example could be the review in case of a legal dispute.

Parts of this paper are adapted from our technical report [START_REF] Mödersheim | The LIGHTest foundation[END_REF].

TPL by Example

We present TPL using the example of an online platform for auction houses. We do not consider peer-to-peer auction houses like eBay, but focus on platforms connecting traditional auction houses to the digital world. The auctions in question may easily range up to thousands of Euros for a single item, leading to the problem of ensuring that the successful bidder indeed pays the sum they have bid. The auction house wants no entrance barrier for new customers who just "stumbled" upon an item by an Internet search. On the other hand, they want to avoid manipulations such as shill bidding (somebody anonymously bids on an item to push the price) and payment defaults.

In the analog world, the solution is that one has to bring references from other auction houses or a bank statement or be present at the auction, proving one's identity. We show how to transfer these aspects to the digital world using LIGHT est in a way where one can benefit from the digital world's potential without losing the security and trust guarantees of analog auction houses.

The first step of digitalization is the creation of online catalogs, where a user can click on items they want to bid on and enter a maximum amount. This is basically an electronic version of the classical paper bidding form. After filling out this form, the user sends it as an HTTPS transaction to the auction house.

This paper introduces a number of example policies defining which forms the auction house accepts. One example policy in natural-language is the following:

Example Policy Rule 1 The auction house accepts any form which is of the "Auction house 2019" format and contains a bid up to 100 Euro.

As the first example of a TPL policy, let us consider how to write the above mentioned Example Policy Rule 1 in TPL:

Policy Rule Specification 1 accept(Form) :extract(Form, format, theAuctionHouse2019Format), extract(Form, bid, Bid), Bid <= 100.

In this example, the variable Form is the transaction, here a bidding form in question in some concrete data format. extract is a predicate that can extract the attributes from the form: this is the interface to the parser for the respective data format. The first extraction generally is the check for the expected type of format, here the format used by the concrete auction house, identified by the constant theAuctionHouse2019Format. Next, we extract the bid field, which is bound to the variable Bid, and finally, we check that the value is below 100.

Semantically, the policy can be seen in two ways: (1) As a formal specification in first-order logic of Example Policy Rule 1. (2) As a program that can check if a form lives up to Example Policy Rule 1. In the following section, we will go in to detail with forms, formats and these semantics.

Syntax & Semantics

Formal Definition

The language of TPL mainly consists of definite horn clauses. Its syntax is based on that of first-order logic and Prolog.

We define four disjoint sets of symbols: (1) Variable symbols -starting with upper-case letters. (2) Function symbols -starting with lower-case letters and With this in place, we use a grammar to define the syntax of TPL specifications, as shown in Figure 1.

Semantics

We here briefly sketch two ways to formally define the semantics of TPL.

Logical Semantics A logical view of the semantics can be obtained if we consider the Horn clauses as logical formulas of first-order logic, where :is ← (logical implication from right to left), the comma is logical conjunction and all variables of every Horn clause are universally quantified, e.g., p(X, Y) :-q(X), r(Y, X) becomes ∀X, Y. p(X, Y) ← q(X) ∧ r(Y, X).

Special care must be taken for built-in predicates, i.e. the interface to the environment, in particular, such as extract that is the interface to the concrete formats and their parsers, as well as lookup that is the interface for looking up information on a server. For the semantics, we fix the meaning of these builtin predicates to an (arbitrary) snapshot of the world; in particular, we assume that during the checking of the policy, the state of the world does not change. 3One may also evaluate logically a historical policy decision by specifying the environment as it was at some point in the past in order to answer the question of whether a given document was within the policy at a previous point in time.

More formally, given a set of Horn clauses H and a query q 1 , . . . , q n , the solutions are those substitutions σ of the variables in the q i such that it holds that H |= σ(q 1 ) ∧ . . . ∧ σ(q n ) where |= is the semantics of first-order logic as defined in any standard textbook. A policy might use built-in predicates which go beyond logical reasoning such as lookup which performs a call to a server. To define the semantics of the solutions in this case we, for a specific policy, allow the inclusion of a formula f that partially specifies this external environment. Such an f could be a trace of the interactions that happened in an execution of the policy. This f simply consists of a number of clauses. As such the semantics is defined as

H ∧ f |= σ(q 1 ) ∧ . . . ∧ σ(q n ).
Executable Semantics TPL is similar to Prolog, but does not include the ! operator or negation as failure. Such "counter-logical" elements would forbid interpretation as logical formulas and the resulting clear and simple semantics. Policies are lists of definite Horn clauses and TPL also shares most of Prolog's syntax.

TPL's executable semantics is the same as that of Prolog except that in TPL our unification always includes the occurs check. The semantics of Prolog can be described as an interpreter -see e.g. Deransart, Ed-Dbali and Cervoni's textbook [START_REF] Deransart | Prolog -The Standard: Reference Manual[END_REF], in particular, in Section 4.2. TPL's built-in predicates (such as extract, lookup, <=) are not part of TPL's core language but are defined outside it.

Forms and Formats

Policies work on forms represented by a variety of concrete data formats, from X.509 certificates and DNS resource records to custom data formats for electronic forms. TPL supports all of these in a flexible way without cluttering the policies with low-level details like parsing. We consider an abstract notion of formats, similar to abstract syntax, namely like a paper form with fields to fill in and each field having a unique identifier. This abstracts from concrete measures (like XML) to structure this information, and any concrete format can be connected to TPL by providing a parser and pretty-printer for it, i.e. the transformation between actual byte strings and abstract syntax. Let us consider a form for the auction house example. Abstractly, it is a set of attribute-value pairs: {(format, the_auction_house_2019), (bidder_name, "John Doe"), (street, "Dartmouth St"), (city, "Midfarthington"), (country, "England"), (lot_number, 54678), (bid, 60), (signature, ...), (certificate, ...)} conditions" are relevant, this must be solved by a kind of locking of databases for the duration of the policy checking. We believe this kind of scenario is extremely atypical for trust policies and not practically relevant.

The actual transaction on the string level could be an XML representation: <?xml version="1.0" encoding="UTF-8"?> <format name="the_auction_house_2019" /> <person> <name>John Doe</name> <street>Dartmouth St.</street> <city>Midfarthington</city> <country>England</country> </person> <lot_number>54678</lot_number> <bid>60</bid> <signature> ... </signature> <certificate> ..

. </certificate>

The idea is that abstract symbols like bidder_name should be a sound abstraction of their concrete byte-level format [START_REF] Mödersheim | A sound abstraction of the parsing problem[END_REF]. Notice that the XML representation's tree structure and the attribute value pair set representation are not the same: it is often nice to have a layer on top of an XML format, so one does not have to browse the XML parse tree but has an immediate representation of the data suitable for one's purposes. TPL provides a built-in predicate extract connecting the interpreter with the appropriate parser so that attributes can be extracted from the format as specified by the attribute value pair representation.

Implementation

For the LIGHT est project, we implemented the Automated Trust Verifier (ATV), at the core of which is a TPL interpreter. The ATV is implemented in Java, using the ANTLR parser generator to implement the grammar from Figure 1.

Besides the interpreter core, the ATV implements the built-in predicates like extract whose truth value depends on extra-logical facts and actions. These predicates are implemented as external functions that are invoked by the native Java code. For this, it is necessary to partition the parameters of built-in predicates into inputs and outputs; e.g. for extract, the first two arguments (the form and the attribute) are inputs, and the resulting value is the output. It is required that all the input arguments must be ground terms (containing no variables) when the interpreter reaches them. After finishing an external call like a server lookup, the control is given back to the interpreter.

Built-In Predicates

This section describes the built-in predicates of TPL in more detail, as they are currently found in our reference implementation ATV.

Built-in Predicate 1 (extract)

The extract predicate is used to extract information from a document (e.g. a transaction, certificate, or trust list entry). This predicate gives a uniform interface to all kinds of data formats; the interpreter is designed modular so that new data formats can easily be integrated by providing a parser for the respective data structure. For a call extract(From, What, Out)

we have that Form is an input document, What is a field of the document, and Out is the output, i.e., the value of that field.

The set of fields that are available depends on the format. Thus, when trying to extract a field that does not exist in the present format, the predicate fails. For every format at least one field is defined, namely format which returns the unique identifier for the document's format.

Built-in Predicate 2 (lookup and trustlist) The lookup predicate allows to perform lookups at DNS name servers and HTTP queries authenticated using DANE. The input parameter Domain defines the DNS domain to query, while the output parameter Entry contains the desired document. In a similar manner, the trustlist predicate is a more specific case, which is used to retrieve a single entry, identified by the parameter Certificate, from a trust list. the TPL interpreter will use the appropriate signature verification function for the format of FORM and succeeds if and only if the form was properly signed using the given key.

Built-in Predicate 5 (verify_hash) The verify_hash predicate checks if an object evaluates to the correct hash value. So for a call verify_hash(Form, Hash) the TPL interpreter will use the appropriate hash function for the format of FORM and succeed if and only if the parameter Form has the same hash as passed by the parameter Hash.

In addition, our implementation comes with additional built-in predicates to support encoding of domains and concatenation of strings.

4 Using TPL So far, our example auction house only accepts bids up to a certain number but puts no constraints on who may place a bid. For large bids the auction house needs to know who they are and that they can be trusted. This is achieved by issuing certificates to users, and publishing a list of trusted authorities who may issue certificates. Such a list is a trust list and is for example published by the European Union in the eIDAS framework. Therefore, we extend our example:

Example Policy Rule 2 The auction house accepts any bid up to 1500 Euro, if it is signed by an eIDAS qualified signature.

Thus, we need to perform the following checks: (1) Is the bid amount smaller than 1500 Euro? (2) Has the bidder's certificate been issued by an eIDAS qualified authority? (3) Did the bidder actually sign the bid?

Signatures and Signable Formats To verify signatures we use the built-in predicate verify_signature and signable formats: A signable format is a format for which a signature verification function is specified. For a form of the specified format and a public key, we can verify if the form is properly signed.

Trust Scheme lookups We need to verify the trust scheme membership of the bidder's issuer and thus have to obtain the associated trust list. Trust lists are discovered using a trust scheme claim which is inside the bidder's or issuer's certificate. In LIGHT est this claim is represented by a domain name [START_REF] Wagner | DNS-based Trust Scheme Publication and Discovery[END_REF], e.g. the (fictional) URL qualified.trust.ec.eu for the trust scheme of qualified eIDAS authorities.

The trustlist built-in predicate (see Section 3.5) triggers a server lookup. It will succeed if a certain trust scheme exists, the trust list is available, and the desired certificate is on that list. It fails otherwise. It, therefore, acts as a requirement in a policy that the given certificate is on the claimed trust list.

To claim a trust scheme membership, a certificate includes a field trustScheme that states the trust scheme (represented as a domain) it claims to be in. In order to ensure that the domain actually belongs to our desired trust scheme, we use the built-in predicate trustscheme (see Sec.3.5). When this is added to a TPL specification containing Policy Rule Specification 1, then any form that lives up to the requirements of either rule is accepted. Policy Rule Specification 2 requires that the format of the form is the auction house format, and extracts the bid to check that it is at most 1500. After that it extracts the bidder's certificate. This a form, and the policy extracts the public key of the bearer, given in the pubKey field. Then the verification of the signature of the form is done with respect to the public key using the verify_signature predicate. Afterward, the policy checks that the certificate is eIDAS qualified. This is done in a separate predicate. From the bidder's certificate, it extracts the issuer's certificate, given in IssuerCertificate. From the IssuerCertificate it then extracts the TrustSchemeClaim, which is a domain name used to address the trust scheme and to verify the issuer's trust scheme claim. The policy checks that the trust membership claim is really eIDAS qualified. This is done using the trustscheme predicate. A lookup is then done using the trustlist predicate, which discovers and retrieves the trust list and verifies that the IssuerCertificate is on the list. Lastly, the issuer's public key is extracted from the trust list entry and then used with verify_signature to verify the signature on the bidder's certificate. The TrustListEntry must contain at least the public key of the issuer, such that it can be verified to be the same as the issuer key recorded in the certificate.

Specifying the policy

This shows that policies can be specified on an abstract level avoiding specifying the whole interaction with the Internet and the checks that need to be performed on the response to authenticate it.

Allowing Trust Translation

Trust schemes can define translations, i.e. they might consider other schemes equivalent to them. We extend our example policy accordingly:

Example Policy Rule 3 The auction house accepts any bid of at most 1000 Euro with a signature from a scheme outside eIDAS if the scheme is deemed equivalent to eIDAS via a translation scheme of eIDAS.

We introduce the notation of equivalence modulo a translation relying on the trust translation schemes provided by the authority of the target scheme.

The used example policy is similar to Policy 2, but the trustscheme predicate is changed to trustschemeX which allows trust translation and is defined explicitly in TPL: trustschemeX checks that a trust scheme membership claim belongs either directly to the scheme we are trusting, or belongs to an equivalent scheme: For a claim for a foreign scheme and the name of a trusted scheme, the built-in predicate encodeX generates a domain for the trust translation scheme. Suppose Claim is a (hypothetical) Swiss scheme located at example.admin.ch and the TrustedScheme is eIDAS_qualified. Then the URL should point to e.g. admin.ch._translation.qualified.trust.ec.eu (i.e. it should escape the domain of the original scheme, and select the corresponding Translation scheme of eIDAS qualified). This domain should refer to the entry about the Swiss scheme at eIDAS. The entry is then used to discover information which can be used to verify equivalence. In the example case, we check if the translation field is set to equivalent.

Delegation

An important concept is delegation: A mandator can delegate rights to a proxy, who then acts on behalf of the mandator. This allows us to extend the auction house service even further:

Example Policy Rule 4 The auction house accepts any bid of at most 1000 with a signature from a proxy. The proxy must be within the eIDAS trust scheme.

Within the delegation we have several fields where the mandator can define what the proxy is allowed to do [START_REF] Wagner | Harmonizing Delegation Data Formats[END_REF]. In this case, the mandator must allow the proxy to place bids. Put in practice, the mandator could also set a maximum amount up to which the proxy is allowed to place bids. Thus the fields must be verified in order to place bids. Further, for the public key, it is checked that it is within the eIDAS trust scheme. Lastly, the policy checks at the delegation provider that the delegation is still valid and that nobody tampered with the delegation. This leads us to the specification of the delegation in Policy Rule Specification 3.

Policy

Verification

Jim [START_REF] Jim | SD3: A trust management system with certified evaluation[END_REF] introduced the trust management system SD3 with certified evaluation. When SD3's evaluator decides whether a transaction lives up to a policy, it provides a proof of this. A separate proof checker can then check the proof's correctness. The proof checker is a very simple program, and thus it is easy to inspect and understand its code -making it highly trustworthy. TPL also allows certified evaluation, with the crucial difference that the trustworthiness of the proof checker does not come from a claim that its code is simple. Instead, we base our proof checker on the prover RP x [START_REF] Schlichtkrull | A verified prover based on ordered resolution[END_REF][START_REF] Schlichtkrull | A verified functional implementation of Bachmair and Ganzinger's ordered resolution prover[END_REF][START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's ordered resolution prover[END_REF][START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's ordered resolution prover[END_REF] which is, with exception of its parser, verified in Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL -A Proof Assistant for Higher-Order Logic[END_REF]. Isabelle is a proof assistant i.e. a computer program that allows its user to prove theorems in e.g. computer science. The idea is that Isabelle ensures the proofs' correctness because RP x is proved in Isabelle/HOL to be sound and complete for first-order clausal logic.

For successful queries the interpreter can construct a proof certificate as a triple (p, (q 1 , ..., q n ), b) where p is the policy, q 1 , ..., q n is the query and b is a record of the results from all calls to the built-in predicates that happened during execution including server-lookups, extractions from forms, signature verification and comparisons of e.g. numbers. The proof checker works as follows:

1. Let c be p ∧ (¬q q ∨ • • • ∨ ¬q n ) ∧ b encoded in the input format of RP x .
2. Run RP x on c. 3. If RP x is successful in proving the formula unsatisfiable, then the proof check was successful.

The idea is that we want prove p ∧ b |= q 1 ∧ ... ∧ q n . This is equivalent to proving that p ∧ (¬q q ∨ • • • ∨ ¬q n ) ∧ b is unsatisfiable, and RP x can do that for any correct positive decision thanks to its soundness and completeness. Our integration of RP x in TPL is currently in the state of an early prototype. We have written a program that can encode a triple (p, (q 1 , ..., q n ), b) in RP x 's input format. Using this program, we have run RP x on a number of such triples and seen that it gives the correct result. One could argue that this is not necessary since RP x is formally verified, however, one should, as e.g. Paulson [START_REF] Paulson | Computational logic: its origins and applications[END_REF] recently pointed out, not see formal verification as a replacement for testing. Indeed we have run RP x on a number of encoded triples but more systematic testing would be needed to ensure a production quality certifier. Notice also that while the core of RP x is verified, the encoding of the formula p ∧ (¬q q ∨ • • • ∨ ¬q n ) ∧ b in RP x s input format is still left unverified and so is the parser of RP x . Notice also that the verification of RP x 's soundness and completeness is only with respect to unsatisfiability in Herbrand models. This is not a problem though since it implies its soundness and completeness with respect to arbitrary models, but this has yet to be formally proven for RP x .

6 Discussion and Related work Blaze et al. [START_REF] Blaze | Decentralized trust management[END_REF] coined the term trust management system and introduced Policy Maker, one of the first such systems. PolicyMaker was refined to create KeyNote [START_REF] Blaze | Keynote: Trust management for public-key infrastructures (position paper)[END_REF][START_REF] Blaze | The keynote trustmanagement system version 2[END_REF]. The relation between access control policies and trust policies was early recognized. Herzberg et al. [START_REF] Herzberg | Access control meets public key infrastructure, or: Assigning roles to strangers[END_REF] sees trust policy languages as an extension of access control mechanisms, thereby, as Li et al. [START_REF] Li | A logic-based knowledge representation for authorization with delegation[END_REF] point out, generalizing authorization. Due to the similarity, a popular idea used in access control languages is often used for trust policy languages, namely logic programming.

For a large number of works, including ours, policies are always formulated positively: every policy rule describes under which conditions one is trusted and the decision is negative when no policy rule is fulfilled. This makes it a lot simpler than languages including negative rules such as Dong and Dulay's [START_REF] Dong | Shinren: Non-monotonic trust management for distributed systems[END_REF] Shinren: While it is convenient to also formulate negative constraints, the integration into the reasoning process results in a rather complicated semantics with a ninevalued logic and requires policy rules to be annotated with priorities. We believe that it is enough to limit the use of negation to black listing, i.e. checking that an entity is not on a black list which can be part of a server lookup with a builtin predicate. Note also that pure Horn clauses are Turing complete, i.e. every computable trust policy decision can be expressed in TPL.

Several of these languages borrow from logics of knowledge and belief such as Li et al.'s DL [START_REF] Li | A logic-based knowledge representation for authorization with delegation[END_REF], Becker et al.'s SecPAL [START_REF] Becker | SecPAL: Design and semantics of a decentralized authorization language[END_REF] as well as Gurevich and Neeman's DKAL [START_REF] Gurevich | DKAL: Distributed-Knowledge Authorization Language[END_REF]. In particular, they contain a modal operator, says, so that the fact that an agent stated a formula is itself a formula. This allows for easily relating the reasoning of participants but leaves the area of classical logic due to modal interpretation in different worlds. Basing a policy language on logic also allows us to achieve proof certification, i.e. checking that a policy decision indeed follows logically from a policy, reducing the chance of a false policy decision due to an implementation error. Jim [START_REF] Jim | SD3: A trust management system with certified evaluation[END_REF] used this idea to allow for a simple proof checker to check the policy decisions made by a more complicated program. Jim's unverified proof checker's trustworthiness came from simplicity rather than being verified.

Conclusion

We have presented TPL, a trust policy language and trust management system. We have shown the language's syntax and semantics as well as the idea of using formats to represent transactions abstractly. We also showed how the language supports signatures, translation and delegation. By basing the semantics on firstorder logic, we have also achieved a way to verify policy decisions, by way of a prover that is formalized sound and complete in the Isabelle proof assistant.

We argued that TPL has the qualities of "modularity", "declarativity and expressive power" and "formal precision and accountability". By being modular TPL allows for heterogeneity. By providing declarativity and expressive power, TPL ensures that it has the expressibility needed to write the policies needed by users. By providing formal precision and accountability, TPL ensures that businesses and organizations can feel safe about the correctness of the automatic trust decisions. TPL is a central component of LIGHT est and with the above qualities we believe that TPL can help LIGHT est achieve its goal of providing a lightweight infrastructure for global heterogeneous trust management in support of an open ecosystem of stakeholders and trust schemes. We hope that this will provide a step towards wider adoption of TPL and trust management systems.

Fig. 1 .

 1 Fig. 1. Syntax in TPL specified by a grammar.

  lookup(Domain, Entry) trustlist(Domain, Certificate, TrustListEntry) Built-in Predicate 3 (trustscheme) The trustscheme predicate checks if a trust scheme claim (a domain name) represents a trusted scheme. Both parameters are input parameters. A call trustscheme(TrustSchemeClaim, eIDAS_qualified) is true if and only if the trust scheme claim is a claim for an eIDAS membership. Built-in Predicate 4 (verify_signature) The verify_signature predicate has two input parameters. For a call verify_signature(Form, PubK)

  trustschemeX(Claim, TrustedScheme) :trustscheme(Claim, TrustedScheme). trustschemeX(Claim, TrustedScheme) :-encodeX(Claim, TrustedScheme, Domain), lookup(Domain, Entry), extract(Entry, translation, equivalent).

  We translate Example Policy Rule 2 into a TPL rule:

	check_eIDAS_qualified(Certificate).
	check_eIDAS_qualified(Certificate) :-
	extract(Certificate, format, eIDAS_qualified_certificate),
	extract(Certificate, issuer, IssuerCertificate),
	extract(IssuerCertificate, trustScheme, TrustSchemeClaim),
	trustscheme(TrustSchemeClaim, eIDAS_qualified),
	trustlist(TrustSchemeClaim, IssuerCertificate, TrustListEntry),
	extract(TrustListEntry, pubKey, PkIss),
	verify_signature(Certificate, PkIss).
	Policy Rule Specification 2
	accept(Form) :-
	extract(Form, format, theAuctionHouse2019format),
	extract(Form, bid, Bid), Bid <= 1500,
	extract(Form, certificate, Certificate),
	extract(Certificate, pubKey, PK),
	verify_signature(Form, PK),

With respect to the assumption that the world does not change during policy evaluation, consider the following example. A policy could ask that a transaction is only accepted if approved by officials in two distinct sections, A and B, of a company, where the policy designer (unspokenly) relied on the fact that by company policy, no employee works in both sections. Then it is conceivable that an employee approved the transaction, who happens to move from section A to section B -with the corresponding trust list entries being updated just while some transaction is checked against the policy. It could thus happen that the policy is "accidentally" fulfilled by the single employee's approval, even though the trust list never actually showed any employee as members of two sections at the same time. Indeed if such "race

Acknowledgement. Andreas Viktor Hess suggested many improvements.

This work was supported by the LIGHT est project, which is partially funded by the European Commission as an Innovation Act as part of the Horizon2020 program under grant agreement number 700321.