A lost wireless sensor may lead to the leakage of sensitive information. This paper proposes a framework to facilitate the design of self-destructing wireless sensors with assured security and performance properties. This framework includes a cryptographic self-destructing mechanism that enables autonomous self-destruction of a wireless sensor and a caching strategy to reduce the performance overhead that is consequently introduced. Based on Discrete-Time Markov Chains (DTMC), we have designed models to characterize the proposed self-destructing mechanism, the caching strategy, various components in a sensor, the attacker, and the interactions among all these elements. We have also defined security and performance properties in the form of probabilistic computation tree logic (PCTL), which could be rigorously verified using probabilistic model checking. This framework offers unique capabilities on performing quantitative analysis on security and performance of wireless sensors.