本文针对串空间模型的一些计算性质作了详细的分析，证明了串空间模型中保密性问题的不可判定性，以及认证问题的不可判定性。关于保密性问题的不可判定性，有一些研究者在其他一些模型之下给出过证明。尽管串空间模型和其他这些模型有许多不同之处，但是他们在直观背景上仍旧是相似的，所以本文借鉴了这些结果，在串空间模型中，通过一个从Post字对应问题的归约，证明了保密性问题的不可判定性。 相比之下，现有针对认证问题的讨论就要少很多。虽然保密性问题和认证问题在定义上相差甚远，但仍旧能通过一个从Post字对应问题的归约，来证明认证问题的不可判定性。这也从一个侧面验证了：保密性和认证性在很多协议中是相互关联的。 另外，本文还就一种保密性不可判定性的证明进行了讨论，指出了其中的问题，并提出了一种简单而有效的修正方法。尽管该证明是在另一个安全协议的形式化模型下作出的，但是由于所使用的归约方法和被归约的对象和我们的工作比较相似，对串空间中的形式化模型的研究也有相当的借鉴意义。 本文考察了串空间模型与BAN类逻辑理想化过程的联系，提出的BAN类逻辑理想化规则赋予了一种串空间的语义，证明了这些规则的合理性。