-
Notifications
You must be signed in to change notification settings - Fork 3
/
prover_tests.txt
10 lines (10 loc) · 1.33 KB
/
prover_tests.txt
1
2
3
4
5
6
7
8
9
10
open(#a, <shared.txt>) |- #root says open(#a, <shared.txt>)
#root says open(#a, <shared.txt>) |- #root says open(#a, <shared.txt>)
#root says (open(#b, <shared.txt>) -> open(#a, <shared.txt>)), open(#b, <shared.txt>) |- #root says open(#a, <shared.txt>)
#root says (open(#b, <shared.txt>) -> open(#a, <shared.txt>)), #root says open(#b, <shared.txt>) |- #root says open(#a, <shared.txt>)
#root says (@A . (open(#b, <shared.txt>) -> open(A, <shared.txt>))), #root says open(#b, <shared.txt>) |- #root says open(#a, <shared.txt>)
#root says (@A . (@R . (open(A, R) -> (@B . ((A says open(B, R)) -> open(B, R)))))), #root says open(#b, <secret.txt>), #b says open(#a, <secret.txt>) |- #root says open(#a, <secret.txt>)
#root says (@A . (@R . (open(A, R) -> (@B . ((A says open(B, R)) -> open(B, R)))))), #root says open(#c, <secret.txt>), #c says open(#b, <secret.txt>), #b says open(#a, <secret.txt>) |- #root says open(#a, <secret.txt>)
iskey(#root, [root]), sign(open(#a, <shared.txt>), [root]) |- #root says open(#a, <shared.txt>)
ca(#ca), iskey(#ca, [ca]), sign(iskey(#root, [root]), [ca]), sign(open(#a, <shared.txt>), [root]) |- #root says open(#a, <shared.txt>)
ca(#ca), iskey(#ca, [ca]), sign(iskey(#root, [root]), [ca]), sign(open(#b, <shared.txt>) -> open(#a, <shared.txt>), [root]), sign(open(#b, <shared.txt>), [root]) |- #root says open(#a, <shared.txt>)