A typed natural deduction calculus to reason about secure trust